Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: Challenge Generalized Horn Resolution (Was: Set Theorists use
EXTENSIONALITY ..... Logic Programmers UNIFY!)

Replies: 2   Last Post: Jun 17, 2013 5:35 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View  
Graham Cooper

Posts: 4,237
Registered: 5/20/10
Re: Challenge Generalized Horn Resolution (Was: Set Theorists use
EXTENSIONALITY ..... Logic Programmers UNIFY!)

Posted: Jun 17, 2013 5:35 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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.

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



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.