
Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Posted:
Dec 5, 2012 2:39 AM


> I worked out an inference rule that works with Modus Ponens that > performs pseudoresolution > > or(X,Y) : or(X,C) , or(Y,not(C). > > Are there rules like the above format that does cutelimination?
I worked out (half way) how to do CUTS with first principles modus ponens.
WHEN GIVEN P and R you can cut A to get (D or V)
r > (a or d) (p & a) > v  (p & r) > (d or v)
PROOF:
(p & r) > (p & (a or d))
(p & (a or d)) > (p & a) or (p & d)
(p & r) > (p & (a or d)) > v or (p & d)
(p & r) > v or (p & r) > (p & d)
(p & r) > v or (p & r) > d
(p & r) > (v or d)
QED
OK 1st step
r > (a or d) (p & r) > ?
To get: (p & r) > (p & (a or d))
use: Z=(a or d)
and(P,Z) : and(P,R) , if(R,Z)
UNIFY VERSION

So, resolution, binary MP, and cuts etc. can all be worked out with the right inference rules and naked PROLOG UNIFY (or Modus Ponens as a separate control and if rules as facts.)
OLD and [OLD>NEW] > NEW
is all you need to imply *ANY* createcheck formula system
Herc  or(X,Y) : or(X,C) , or(Y,not(C). RESOLUTION and(P,Z) : and(P,R) , if(R,Z) CUT
Depth Limiting or Smart Control Logic Required!

