Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.


Math Forum
»
Discussions
»
sci.math.*
»
sci.math
Topic:
Challenge Generalized Horn Resolution (Was: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!)
Replies:
2
Last Post:
Jun 17, 2013 5:35 PM




Re: Challenge Generalized Horn Resolution (Was: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!)
Posted:
Jun 17, 2013 5:35 PM


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 LambdaProlog, > 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 clausetemplate (TABLE HEADER) can be determined.
http://phpprolog.com/help.php
FAQ 5  WHAT ARE THE DIFFERENCES TO STANDARD PROLOG?
STANDARD PROLOG
owns(tom, house). ENTERING A FACT owns(tom, car). owns(tom, cat).
? owns(tom, X) ASKING A QUERY X = house X = car X = cat
======================================
PHPPROLOG
owns tom house. ENTERING A FACT owns tom car. owns tom cat.
owns tom X ? ASKING A QUERY
owns  tom  X  owns  tom  house owns  tom  car owns  tom  cat
In general forward chaining has exponential complexity
O( inf_rules ^ ply )
so you need to specify what is the need.
e.g. for detecting contradictions you should be able to design a cut down forward chainer for that!
Herc  www.phpPROLOG.com



