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