Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
DOUBLE NEGATION via MODUS PONENS!
Posted:
Nov 29, 2012 5:42 PM
|
|
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
|
|
|
|
