Re: Help: Multiple Proof Trees

On 2005-08-30, Bart Demoen <bmd@xxxxxxxxxxxxxxxxx> wrote:
> Pasquale Renna wrote:

<snip>

> 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) ?

?- listing((_,_)).

:- module_transparent (',')/2.

A, B :-
A,
B.

So, there is a clause and that is why clause/2 does its work. This clause
is not a loop because the body is compiled. As a side-issue, this clause
used to be there to deal with G = (A,B), call(G). For quite a while I think
it is no longer in use as meta-calls of complex goals are compiled.

> Other systems will give you an error similar to the one for true.

I think clause/2 is only guaranteed to work on dynamic code. On all the
rest it may work, fail or return an error, so you must be careful what
to interpret. I'd go for

prove(Goal, Proof) :-
predicate_property(Goal, built_in), !,
Proof = Goal,
Goal.
....


Cheers --- Jan
.

Relevant Pages