Defining a conditional condition in Prolog

Question

I tried to acclimatize in Prolog and Horn's sentences, but the transition from formal logic still seems uncomfortable and forced. I understand that there are advantages to having everything in a standard form, but:

What is the best way to define a conditional material operator --> in Prolog, where A --> B succeeds when either A = true and B = true OR B = false ? That is, an if->then that does not fail when if is false without else .

In addition, what are the unobvious benefits of Horn's offerings?

Answer 1

What is the best way to define a conditional material operator → in Prolog

When A and B are just variables that should be bound to true and false atoms, this is easy:

 cond(false, _). cond(_, true). 

But overall there is no better way, because Prolog does not offer the correct negation, only negation as failure is monotonous. The closest you can come with actual sentences A and B often

 (\+ A ; B) 

who tries to prove A , then goes to B if A cannot be proved (this does not mean that it is incorrect due to a closed world assumption ).

Negation, however, should be used with caution in Prolog.

In addition, what are the unobvious benefits of Horn's offerings?

They have direct procedural reading. Prolog is a programming language, not a proof of a theorem. It is possible to write programs that have a clear logical meaning, but they are still programs.

To see the difference, consider the classic sorting problem. If L is a list of numbers without duplicates, then

 sort(L, S) :- permutation(L, S), sorted(S). sorted([]). sorted([_]). sorted([X,Y|L]) :- X < Y, sorted([Y|L]). 

is a logical specification of what means that S contains elements of L in sorted order. However, it also has a procedural value, namely: try all permutations of L until it is sorted. This procedure, in the worst case, goes through all n! permutations, although sorting can be done in O (n lg n), which makes it a very poor sorting program.

See also this question .