Re: Help: Multiple Proof Trees

Pasquale Renna wrote: 
Let's take this small program as an example:

:- op(500, xfy, <==).

prove(true, true).
prove( (Goal1, Goal2), (Proof1, Proof2) ) :- prove(Goal1, Proof1),
prove(Goal2, Proof2).
prove( Goal, Goal <== Proof) :- clause(Goal, Body), prove(Body, Proof).

a :- b,c.
a :- e.
b.
c.
e.



The goal prove(a, Proof) succeeds for the first time, but it gives
errors on backtracking. Any suggestions on obtaining all the proof
trees for a specified goal? Thanks in advance!


For future use: don't say "it gives errors on backtracking", say "the error
message is 'ERROR: clause/2: No permission to access private_procedure `true/0''"

The problem occurs because backtracking causes the last clause to be activated
with Goal equal to true, and the goal clause(true,Body) results in the error
message.
You could adapt the program as follows:


prove(true, true).
prove( (Goal1, Goal2), (Proof1, Proof2) ) :-
        prove(Goal1, Proof1),
        prove(Goal2, Proof2).
prove( Goal, Goal <== Proof) :-
        Goal \== true,
        clause(Goal, Body), prove(Body, Proof).

However, you will next observe something weird (if you are using SWI): you get
answers like

	Proof = a<== (b, c)<== (b, c)<== (b<==true, c<==true)

because SWI make ?- clause((A,B),C). succeed [Jan, is that a bug (using 5.5.3) ?]
Other systems will give you an error similar to the one for true.

So you should also prevent backtracking from the second to the third clause ...
maybe better use some cuts, as in

prove(true, Proof) :- !, Proof = true.
prove( (Goal1, Goal2), Proof) :- !, Proof = (Proof1, Proof2),
        prove(Goal1, Proof1),
        prove(Goal2, Proof2).
prove( Goal, Goal <== Proof) :-
        clause(Goal, Body),
        prove(Body, Proof).

BTW, SWI allows you to do clause/2 on a (and b ...) but in other systems, you need
to declare them dynamic.

Cheers

Bart Demoen
.

Relevant Pages

  • Re: swi prolog and odbc connectivity
    ... > the first record and showing it successfully, ... > backtracking to pick up all possible solutions. ... The fail predicate ... > It sounds like odbc_query doesn't know whether it succeeds or fails. ...
    (comp.lang.prolog)
  • ECLiPSe counting nodes
    ... for backtracking: ... Does the fact that it returns a 0 first time round imply that it went ... I was expecting a much larger value than 0. ... Essentially I want it to return the number of times indomain was called, ...
    (comp.lang.prolog)