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 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* create|check 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!