```Date: Dec 7, 2012 9:00 PM
Author: Graham Cooper
Subject: Forward Branching MODUS PONENS!

If you were given a set of AXIOMSand a FORMULAhow would you decide if the FORMULAwas a THEOREM of those AXIOMS?AXIOM --> THM ---> THM ---> THM ---> FORMULA?MPOLD & if( OLD, NEW ) -> NEWThere 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*|v3|v4     2*| \  /|   v|   5|   |v   v7   6 \ /  v  8  |  v  9This makes any INFERENCE RULEinto an AXIOM (level 1 theorem)t(if(X,Y),1) :- if(X,Y).This is different to MODUS PONENS becauseit uses TRANSITIVE IMPLY and a LEVEL 1 THEOREMwhich makes it START WITH ANY AXIOMand BRANCH FORWARD!t(NEW,l(L)) :- trif(AXIOM,NEW,L), t(AXIOM,1).TRANSITIVE IFtrif( 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= 1LVL= 1THM= 2LVL= 2* 1 and 2 are THEOREMS *THM= if(1,3)LVL=1THM= if(3,4)LVL=1THM= if( and(2,4), 5)LVL = 1THM = if(5,6)LVL = 1THM= if(4,7)LVL = 1THM= if( and(6,7), 8)LVL = 1THM= if(8,9)LVL = 1THM= 3LVL = l(l(_))* 3 is a LEVEL 2 THEOREM *THM= 4LVL = l(l(l(_)))THM=7LVL = 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  9MODUS PONENS would work these out in the reverse order!  (whenchecking a formula)Herc
```