Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: DOUBLE NEGATION via MODUS PONENS!
Replies: 0

 Search Thread: Advanced Search

 Graham Cooper Posts: 4,495 Registered: 5/20/10
DOUBLE NEGATION via MODUS PONENS!
Posted: Nov 29, 2012 5:42 PM
 Plain Text Reply

threm(R,step(S)) <- threm(L,S) & if(L,R).

if( not(not(X)), X ).

******************

TRY to understand this 2 line Prolog program!

Otherwise all the automated proof theory to come won't make sense.

******************

threm( not(not(me)) , 1 ).

This is just ADDING A THEOREM
~~me

******************

?- threm( me , 1 ).
NO

This is testing if me is a level 1 theorem.
ANSWER = NO

******************

?- threm( me, step(1) )
YES

This is how Prolog worked out that T|-me
is a theorem after 1 step of inferences.

******************

MODUS PONENS
threm(R,step(S)) <- threm(L,S) & if(L,R).

INFERENCE RULE
if( not(not(X)), X ).

FACT
threm( not(not(me)) , 1 ).

QUERY
?- threm( me, step(1) )

******************

The QUERY ENGINE looks up MODUS PONENS

MODUS PONENS
threm(R,step(S)) <- TAIL

THEN IT UNIFIES
R=me S=1

---------- QUERY ------------ MP HEAD
UNIFY( threm(me, step(1)) , threm(R, step(S)) )
R=me S=1

*****************

Then the QUERY ENGINE solves the TAIL of MODUS PONENS

HEAD <- threm(L,S) & if(L,R).

and substitutes R=me
and S=1
(same formula)

threm(L,1) ^ if(L,me)

It's basically looking for a Theorem to imply 'me' - the Query.

******************

Then Prolog searches for an INFERENCE RULE
if(L,me)

INFERENCE RULE
if( not(not(X)), X ).

L=not(not(X))
R=me

and it also solves

threm( L , 1 )
threm( not(not(me)) , 1 )

and then can UNIFY that with a given FACT.

FACT
threm( not(not(me)) , 1 ).

This 'AXIOM' was worked out backwards
by matching the RHS of INFERENCE RULES
and Backward Chaining to Lower Level Theorems and Axioms.

******************

There are no more TAILS SUBGOALS to solve
so PROLOG returns YES - me is a theorem in 1 step.

?- threm( me , step(1) )

Herc
--
if( if(S,not(R)) , if(R,not(S)) ).
if it's sunny then it's not raining
ergo
if it's raining then it's not sunny

© The Math Forum at NCTM 1994-2018. All Rights Reserved.