PROLOG THEORY BUG!

Hercules ofZeus

unread,

Oct 30, 2012, 5:47:32 AM10/30/12

to

Why this is marked as abuse? It has been marked as abuse.

Report not abuse

f(0).
t(1).

wff(X) :- t(X).
wff(X) :- f(X).
what(X,true) :- t(X).
what(X,false) :- f(X).

if(X,Y) :- t(X), t(Y).
if(X,Y) :- f(X), f(Y).
if(X,Y) :- f(X), t(Y).

f(if(X,Y)) :- t(X),f(Y).

t(if(X,Y)) :- if(X,Y).

-------------------

OK, X should be any Boolean Predicate Formula, just if(x,y) at this
stage.

?- wff( if(1,1) )
YES

?- wff( if(1,0) )
*HANGS*

It should complete matching the WFF(X) :- t(X) without success and
proceed onto WFF(X) :- f(X).

Herc

William Elliot

unread,

Oct 30, 2012, 5:56:24 AM10/30/12

to

On Tue, 30 Oct 2012, Hercules ofZeus wrote:

> f(0).
> t(1).
>
> wff(X) :- t(X).
> wff(X) :- f(X).
> what(X,true) :- t(X).
> what(X,false) :- f(X).
>
> if(X,Y) :- t(X), t(Y).
> if(X,Y) :- f(X), f(Y).
> if(X,Y) :- f(X), t(Y).
>
> f(if(X,Y)) :- t(X),f(Y).
>

What's f?

> t(if(X,Y)) :- if(X,Y).

t(X) :- X

What's :- supposed to mean?

> OK, X should be any Boolean Predicate Formula, just if(x,y) at this
> stage.
>
> ?- wff( if(1,1) )
> YES
>
> ?- wff( if(1,0) )
> *HANGS*
>

You got a problem with a lynching?

> It should complete matching the WFF(X) :- t(X) without success and
> proceed onto WFF(X) :- f(X).

Why?

Gary Forbis

unread,

Oct 30, 2012, 9:39:43 AM10/30/12

to

I think you're talking in riddles.

I haven't use prolog in decades.

The problem I see is a bit more basic.

?- wff(if()

How is prolog to evaluate that?
I'm pretty sure it isn't well formed.
As is his notion of about how to go about
determining if a formula is well formed.
And he claims to have written a prolog compiler.

A syntactically incorrect program won't compile.
A syntactically correct program will compile.
That's all wff means with respect to a programming langauge.
The programmer may have written something that doesn't
map to the intended semantics but that is a separate issue.

Gary Forbis

unread,

Oct 30, 2012, 10:13:30 AM10/30/12

to

I don't remember my prolog all that well. It's been decades.
Please help me remember.

tom(male).
?- tom(X)
returns
tom(male).
is that correct?

-? wff(if(1,0))
having found wff(X) :- t(X).
wants to evaluate t(if(1,0)).
having found t(if(X,Y)) :- if(X,Y).
wants to evaluate if(1,0).
having found if(X,Y) := t(X), t(Y).
wants to evalueate t(1).
Find t(1)
RETURNS success.
wants to evaluate t(0).
RETURNS failure.
wants to evaluate t(if(if(1,0),Y) :- if(if(1,0),Y)
wants to evaluate if(1,0)
...

Graham Cooper

unread,

Oct 30, 2012, 3:41:10 PM10/30/12

to

On Oct 30, 7:56 pm, William Elliot <ma...@panix.com> wrote:
> On Tue, 30 Oct 2012, Hercules ofZeus wrote:
> > f(0).
> > t(1).
>
> > wff(X) :- t(X).
> > wff(X) :- f(X).
> > what(X,true) :- t(X).
> > what(X,false) :- f(X).
>
> > if(X,Y) :- t(X), t(Y).
> > if(X,Y) :- f(X), f(Y).
> > if(X,Y) :- f(X), t(Y).
>
> > f(if(X,Y)) :- t(X),f(Y).
>
> What's f?
>

a Predicate that signifies it's argument string is false in the
Theory.

>
> > t(if(X,Y)) :- if(X,Y).
>
> t(X) :- X
>
> What's :- supposed to mean?

<-

Backward Chained inference.

>
> > OK, X should be any Boolean Predicate Formula, just if(x,y) at this
> > stage.
>
> > ?- wff( if(1,1) )
> > YES
>
> > ?- wff( if(1,0) )
> > *HANGS*
>
> You got a problem with a lynching?
>
> > It should complete matching the WFF(X) :- t(X) without success and
> > proceed onto WFF(X) :- f(X).
>
> Why?
>

It's a formal system in PROLOG.

In Predicate sysntax...

f(0).
t(1).

wff(X) <- t(X).
wff(X) <- f(X).
what(X,true) <- t(X).
what(X,false) <- f(X).

if(X,Y) <- t(X) ^ t(Y).
if(X,Y) <- f(X) ^ f(Y).
if(X,Y) <- f(X) ^ t(Y).

f(if(X,Y)) <- t(X) ^ f(Y).

t(if(X,Y)) <- if(X,Y).

-----------

I think now I've introduced a value into f(...), f(0).

t( if(X,Y) ) <- if(X,Y) ^ t(X) ^ f(X).

needs to be changed. I think if(1,0) is triggering t(if(1,0)).

so I've mixed up a 1 truth value logic with a boolean logic here..

----------

t( 'boolean-arg-predicates' ) is how I manipulate the formulas with
1OL PROLOG rules.
i.e. now the Theory Predicate is just an ARGUMENT (of either t(..) or
f(..) so it's do-able in 1OL.

Herc

Graham Cooper

unread,

Oct 30, 2012, 3:59:44 PM10/30/12

to

OK I got it working! Check this WFF FORMULA CHECKER!

f(0).
t(1).

wff(X) :- t(X).
wff(X) :- f(X).
what(X,true) :- t(X).
what(X,false) :- f(X).

t(if(X,Y)) :- t(X), t(Y).
t(if(X,Y)) :- f(X), f(Y).
t(if(X,Y)) :- f(X), t(Y).

f(if(X,Y)) :- t(X),f(Y).

-----------------------

?- wff (1 ).
YES

?- wff( if(1,1) )
YES

?- wff( if(1,0) )

YES

?- what( if(1,1) , V ).
V = true

?- what( if(1,0), V )
V = false

?- what( if ( if(1,1) , if(1,0) ) , V ).
V = false

ALL SET! A full formal theory with arithmetic, quantifiers, sets,
proof by resolution should only be about 50 lines of PROLOG code!

Herc

Graham Cooper

unread,

Nov 16, 2012, 9:28:47 PM11/16/12

to

In standard PROLOG
X = male

In micro PROLOG
tom(X)
---------
tom(male)

mP has Tabular output.

>
> -? wff(if(1,0))
> having found wff(X) :- t(X).
> wants to evaluate t(if(1,0)).
> having found t(if(X,Y)) :- if(X,Y).
> wants to evaluate if(1,0).
> having found if(X,Y) := t(X), t(Y).
> wants to evalueate t(1).
> Find t(1)
> RETURNS success.
> wants to evaluate t(0).
> RETURNS failure.
> wants to evaluate t(if(if(1,0),Y) :- if(if(1,0),Y)
> wants to evaluate if(1,0)
> ...

Haha! Very clever Gary!

Here is a FOX, GOAT, LETTUCE problem for you to try.

f(0).
t(1).
f(1) :- t(0).
t(0) :- f(1).
f(f(X)) :- t(X).

wff(X) :- t(X).
wff(X) :- f(X).
what(X,true) :- t(X).
what(X,false) :- f(X).

t(if(X,Y)) :- t(X), t(Y).
t(if(X,Y)) :- f(X), f(Y).
t(if(X,Y)) :- f(X), t(Y).

t(or(X,Y)) :- t(X).
t(or(X,Y)) :- t(Y).
t(and(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- f(X),f(Y).
t(xor(X,Y)) :- t(X),f(Y).
t(xor(X,Y)) :- f(X),t(Y).

f(if(X,Y)) :- t(X),f(Y).
f(or(X,Y)) :- f(X),f(Y).
f(and(X,Y)) :- f(X).
f(and(X,Y)) :- f(Y).
f(iff(X,Y)) :- t(X),f(Y).
f(iff(X,Y)) :- f(X),t(Y).
f(xor(X,Y)) :- t(X),t(Y).
f(xor(X,Y)) :- f(X),f(Y).

t(R) :- if(L,R), t(L).

if( river(M,F,F,L,T), river(F,F,F,L,T) ). ***
if( river(M,F,G,G,T), river(G,F,G,G,T) ).

river(0,0,0,0,0).

river(f(M),f(F),G,L2,s(T)) :- river(M,F,G,L,T).
river(f(M),F,f(G),L2,s(T)) :- river(M,F,G,L,T).

river(M,F,G,L2,s(T)) :- river(f(M),f(F),G,L,T).
river(M,F,G,L2,s(T)) :- river(f(M),G,f(G),L,T).

*** = if the Fox and Goat are on the same side of the river at the
same time T
then the Man must be on the same side as them. F,F,F (all on same
side)

I got it working out simple trips across the River.

?- river(A,B,C,D,s(s(0))).

This will return all the possible trips after crossing the river
twice!

Herc