achoi@cory.Berkeley.EDU (Andrew Choi) (11/16/90)
Hi everyone. I was convinced that Prolog can handle only Horn's Clauses until a friend of mine brought me this example: Let's say we want to say: a ; b :- c. (c -> (a or b)) /* Illegal in Prolog */ According to rules of Boolean Algebra, we can re-express proposition as: c -> (a or b) (not c) or (a or b) ((not c) or b) or a (not (c and (not b))) or a (c and (not b)) -> a a :- c, not(b). /* Legal in Prolog */ It seems like one can apply this procedure to all non-Horn's clauses to make them Horn's Clauses. Is this right? Is there some mistakes I don't see here? Thanks for the help. Name: Andrew Choi Internet Address: achoi@cory.berkeley.edu Tel: (415)848-5658 #include <standard/disclaimer.h>
ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) (11/16/90)
In article <8956@pasteur.Berkeley.EDU>, achoi@cory.Berkeley.EDU (Andrew Choi) writes: > Let's say we want to say: > a ; b :- c. (c -> (a or b)) /* Illegal in Prolog */ Prolog syntax is a variant of "Kowalski form". In Kowalski form, n1, n2, ..., ni -> p1, p2, ..., pk stands for the clause pk or ... or p2 or p1 or not ni or ... or not n2 or not n1 Prolog syntax just reverses the sense of the arrow. So *if* Prolog had a syntax for non-Horn clauses, it ought to be a, b :- c % a OR b OR not(c) Remember, the two sides of an implication have different polarities. > According to rules of Boolean Algebra, we can re-express > [c -> (a or b)) as: > (c and (not b)) -> a > a :- c, not(b). /* Legal in Prolog */ > It seems like one can apply this procedure to all non-Horn clauses > to make them Horn Clauses. Is this right? No. Whether something is a Horn clause or not doesn't depend on the syntax you use for it, but whether when it is written out in canonical form it has at most one positive literal. Let's take your example: a :- c, not(b) That's syntax for a | not(c) | not(not(b)) WHICH IS NOT A CLAUSE YET. When we simplify away ~not, we get a | b | ~c which has two positive literals, which means that it is not a Horn clause. A Prolog rule which contains a negated goal in its body is NOT a Horn clause! > Is there some mistakes I don't see here? The basic mistake here is that the operation *some* Prologs deceptively call not(_) is not logical negation (which is why careful programmers spell that operation \+(X), read "X does not succeed"), and that even the operation *some* Prologs honestly call not(_) is not a *complete* implementation of negation, sound though it is. The basic execution method of Prolog comes from a theorem proving strategy which was designed for Horn clauses. If you need non-Horn clauses, you need a different method. (See Mark Stickel's papers on his "Prolog Technology Theorem Prover" for one approach.) -- The problem about real life is that moving one's knight to QB3 may always be replied to with a lob across the net. --Alasdair Macintyre.