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: DOUBLE NEGATION via MODUS PONENS!
Replies: 0  

Advanced Search

Back to Topic List Back to Topic List  
Graham Cooper

Posts: 4,253
Registered: 5/20/10
DOUBLE NEGATION via MODUS PONENS!
Posted: Nov 29, 2012 5:42 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic 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




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.