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