On Jun 17, 11:16 pm, Jan Burse <janbu...@fastmail.fm> wrote: > Hi, > > Here is the challenge. Generalized Horn resolution. It > would allow logic programming to climbe the ladder > of evolution as follows: > > Homo Ergaster: > Backward chaining without variable sharing. > Typically found in Prolog system. > > Homo Antecessor: > Backward chaining with variable sharing. > Status: found in Lambda-Prolog, > found in Jekejeke Prolog, t.b.d. > > Homo Rhodesiensis: > Forward chaining without variable sharing. > Basic mechanism of some systems, i.e. CLIPS. > Status: Some integration with backward > chaining found in Jekejeke Prolog, t.b.d. > > Homo Sapiens: > Forward chaining with variable sharing. > Status: t.b.d. > > I first though I could explain the variable > chaining via embedded implication, but lets > put this asside for the moment, and lets try > to formulate it another way. > > So how is classical Horn resolution defined? Well > it uses the notion of a Horn clause and Horn goal. > Which is in its full form: > > forall x1, .. xm (A v ~A1 .. ~An) n>=0 > forall x1, .. xm (~A1 .. ~An) n>=0 > > The variables x1,..,xm are assumed to be ALL the > variables from A1, .., An and optionally A. > > What would be generalized Horn resolution? Well > we would simply stretch the notion of a Horn clause > respective Horn goal. And would allow that NOT > ALL the variables would be quantified. The variables > that are not quantified are shared variables. > > Shared variables is nothing new, everbody can do > logic with them, and its possible to define FOL > so that it works with shared variables, so that > one can do reasoning such as etc..: > > x=1, y=2 |- x+y=3 > > But how would resolution work if shared variables > are around? Any pointers? > > Here is a test case. It is implemented with the > help of embedded implication. The test case would > allow cross validation between forward and backward > chaining in some cases. According to the equation > algorihm = control + logic. Forward and backward > chaining are just the control in the logic soup. > > The test case uses the following rules: > > p(a) :- q(b). > p(a) :- q(d). > p(c) :- q(d). > > Graphically this can be depicted as: > > a --- b > \ > \ > c --- d > > For the test case I assume an operator (-:)/2 > for embedded implication. Logically, and not > control wise, it should do: > > G, A |- B > ----------- (-:R) > G |- A -: B > > Here are the test cases: > > Homo Ergaster: Backward Chaining > Script: ?- p(a) -: q(X). > Expected Result 1: X=b > Expected Result 2: X=d > > Homo Antecessor: Backward Chaining > Script: ?- p(X) -: q(d). > Expected Result 1: X=a > Expected Result 2: X=c > > Homo Rhodesiensis: Forward Chaining > Script: ?- p(a) -: q(X). > Expected Result 1: X=b > Expected Result 2: X=d > > Homo Sapiens: Forward Chaining > Script: ?- p(X) -: q(d). > Expected Result 1: X=a > Expected Result 2: X=c > > Currently I have not yet a solution for a system that > could solve the Homo Sapiens problem, although the > rest of the stages, Homo Ergaster, Homo Antecessor and > Homo Rhodesiensis already work. >
In SQL the user interface outputs result sets instead of compiling to BagOf Lists.
You can also output clauses in the form they were queried, with the minor proviso of 1 single Goal per Query so the output clause-template (TABLE HEADER) can be determined.