```Date: Dec 5, 2012 2:39 AM
Author: Graham Cooper
Subject: Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>

> I worked out an inference rule that works with Modus Ponens that> performs pseudo-resolution>> or(X,Y)  :-  or(X,C) , or(Y,not(C).>> Are there rules like the above format that does cut-elimination?I worked out (half way) how to do CUTS with first principles modusponens.WHEN GIVEN P and Ryou can cut Ato 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) -> vor(p & r) -> (p & d)(p & r) -> vor(p & r) -> d(p & r) -> (v or d)QEDOK 1st stepr ->  (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 PROLOGUNIFY (or Modus Ponens as a separate control and if rules as facts.)OLD and [OLD->NEW] -> NEWis all you need to imply *ANY* create|check formula systemHerc--or(X,Y)  :-  or(X,C) , or(Y,not(C).   RESOLUTIONand(P,Z) :- and(P,R) , if(R,Z)       CUTDepth Limiting or Smart Control Logic Required!
```