Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Replies: 6   Last Post: Dec 5, 2012 2:39 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,280
Registered: 5/20/10
Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Posted: Dec 5, 2012 2:39 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.