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: Forward Branching MODUS PONENS!
Replies: 0

 Graham Cooper Posts: 4,495 Registered: 5/20/10
Forward Branching MODUS PONENS!
Posted: Dec 7, 2012 9:00 PM

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
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