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

Topic: Forward Branching MODUS PONENS!
Replies: 0  

Advanced Search

Back to Topic List Back to Topic List  
Graham Cooper

Posts: 4,333
Registered: 5/20/10
Forward Branching MODUS PONENS!
Posted: Dec 7, 2012 9:00 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

If you were given a set of AXIOMS
and a FORMULA

how would you decide if the FORMULA
was a THEOREM of those AXIOMS?


AXIOM --> THM ---> THM ---> THM ---> FORMULA?


MP
OLD & if( OLD, NEW ) -> NEW

There are 2 ways to use MODUS PONENS

FORWARD BRANCHING
Match the OLD argument of if(OLD, NEW)
to some low level AXIOMS.

BACKWARD BRANCHING
OR, match the NEW argument of if(OLD,NEW)
to the FORMULA and then the next lower level formula.



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

OK, we have 2 AXIOMS, 1 and 2
(both level 1 Theorems)


t(1,1).
t(2,1).

and some inference rules.


if(1,3).
if(3,4).
if( and(2,4), 5 ).
if(5,6).
if(4,7).
if( and(6,7), 8 ).
if(8,9).

1*
|
v
3
|
v
4 2*
| \ /
| v
| 5
| |
v v
7 6
\ /
v
8
|
v
9



This makes any INFERENCE RULE
into an AXIOM (level 1 theorem)

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


This is different to MODUS PONENS because
it uses TRANSITIVE IMPLY and a LEVEL 1 THEOREM
which makes it START WITH ANY AXIOM
and BRANCH FORWARD!

t(NEW,l(L)) :- trif(AXIOM,NEW,L), t(AXIOM,1).


TRANSITIVE IF

trif( OLD , NEW , l(L) ) :- if( OLD , NEW ).
trif( OLD , NEW , l(L) ) :- if( OLD , MID ) , trif( MID, NEW , L ).



NOW we can ask PROLOG what are all the THEOREMS?

?- t( THM , LVL ).

THM= 1
LVL= 1

THM= 2
LVL= 2

* 1 and 2 are THEOREMS *

THM= if(1,3)
LVL=1

THM= if(3,4)
LVL=1

THM= if( and(2,4), 5)
LVL = 1

THM = if(5,6)
LVL = 1

THM= if(4,7)
LVL = 1

THM= if( and(6,7), 8)
LVL = 1

THM= if(8,9)
LVL = 1

THM= 3
LVL = l(l(_))

* 3 is a LEVEL 2 THEOREM *

THM= 4
LVL = l(l(l(_)))

THM=7
LVL = l(l(l(l(_))))



NOT BAD! PROLOG derived all those facts from the 2 axioms 1 & 2.

but it missed 8 and 9!

7 6
\ /
v
8
|
v
9


MODUS PONENS would work these out in the reverse order! (when
checking a formula)

Herc



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.