7

I have been trying to acclimate to Prolog and Horn clauses, but the transition from formal logic still feels awkward and forced. I understand there are advantages to having everything in a standard form, but:

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

truth table

Also, what exactly are the non-obvious advantages of Horn clauses?

Community
  • 1
  • 1
QuietThud
  • 351
  • 1
  • 12

1 Answers1

3

What is the best way to define the material conditional operator --> in Prolog

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

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

But in general, there is no best way because Prolog doesn't offer proper negation, only negation as failure, which is non-monotonic. The closest you can come with actual propositions A and B is often

(\+ A ; B)

which tries to prove A, then goes on to B if A cannot be proven (which does not mean that it is false due to the closed-world assumption).

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

Also, what exactly are the non-obvious advantages of Horn clauses?

That they have a straightforward procedural reading. Prolog is a programming language, not a theorem prover. It's possible to write programs that have a clear logical meaning, but they're still programs.

To see the difference, consider the classical problem of sorting. 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 it means for S to contain the elements of L in sorted order. However, it also has a procedural meaning, which is: try all the permutations of L until you have one that it sorted. This procedure, in the worst case, runs through all n! permutations, even though sorting can be done in O(n lg n) time, making it a very poor sorting program.

See also this question.

Community
  • 1
  • 1
Fred Foo
  • 355,277
  • 75
  • 744
  • 836
  • Not sure I agree with your theorem prover vs. programming language view. And for sorting, please [look at this program](http://stackoverflow.com/a/6218051/772868) – false Nov 26 '12 at 20:23
  • But I agree with the rest of your answer! – false Nov 26 '12 at 20:25
  • Thank you, larsmans, for taking the time to write a thorough and clear answer that anticipated my related concerns. – QuietThud Nov 26 '12 at 20:43
  • @false Can you please elaborate on why you may disagree? Or point me to some reading material? – QuietThud Nov 26 '12 at 20:44
  • @false: your sorting example proves my point exactly; by reordering the clauses, you can largely retain the logical meaning but get a completely different program (largely because you use the metalogical `nonvar`). – Fred Foo Nov 26 '12 at 21:01
  • @larsmans: but the when-annotation cannot change the meaning of a program (in contrast to simple `nonvar/1` directly in a program)! And you also need performance-tweaks in theorem provers. – false Nov 26 '12 at 21:24
  • @QuietThud: Will do, but probably not 2day. – false Nov 26 '12 at 21:25