Maude-help mailing list

[Patrick Browne <patrick.browne AT dit.ie>]

Dear list,
Below are two modules based on a Gries & Schneider example of propositional calculus.
My intuition is that SUPERMAN1 demonstrates that the propositions form a valid argument, and SUPERMAN2 provides a proof of the conclusion.
The implications of SUPERMAN1 have been replaced by 'equivalent' equations in SUPERMAN2.
But I am unsure about the logic used in SUPERMAN2. Does it represent valid reasoning?
Any clarification or pointers to the literature would be appreciated.
I am only interested in using basic Maude language rather than writing or using additional provers.
Regards,
Pat

***(
From: A Logical Approach to Discrete Math by D. Gries and F. Schneider. pages 37 & 88.

http://books.google.ie/books?id=ZWTDQ6H6gsUC&pg=PA89&lpg=PA89&dq=gries+schneider+superman&source=bl&ots=k92-M86Rgx&sig=8Ejywk2mW14BMBtLIZK4uhTM4RE&hl=en&sa=X&ei=u0HRUruWCoGQhQfApYDgCQ&ved=0CCoQ6AEwAA#v=onepage&q=gries%20schneider%20superman&f=false

The following English sentences consists of assumptions about Superman an one conclusion.
 The conclusion is supposed to follow from the assumptions.
 English paragraph
 If Superman were able and willing to prevent evil, he would do so.
 If Superman were unable to prevent evil, he would be ineffective and if he were unwilling to prevent evil, he would be malevolent.
 Superman does not prevent evil.
 If Superman exists, he is neither ineffective nor malevolent.
 Therefore Superman does not exist.


 We associate a Boolean identifier with each primitive sub-proposition in the above paragraph.
 a: Superman is able to prevent evil.
 w: Superman is willing to prevent evil.
 i: Superman is ineffective.
 m : Superman is malevolent.
 p: Superman prevents evil.
 e: Superman exists.
)

fmod SUPERMAN1 is
ops a w i m p e aw na nw np ee :  -> Bool .
eq   aw = ((a and w) implies p) .
eq   na = ((not a) implies i)  .
eq   nw = ((not w) implies m) .
eq   np = not p .
eq   ee = (e implies ((not i) and (not m)))  .
endfm
***> Using the above propositions we get either true or a string of exclusive or of conjunctions
***> This reduction shows that the propositions represent a valid argument.
red (aw and na and nw and np and ee) implies (not e) .
***> The next reduction does not establish anything.
red (aw and na and nw and np and ee) implies  e .

***> In SUPERMAN2 we write implications from SUPERMAN1 as equations in SUPERMAN2
***> Also we write the negated p as false.
fmod SUPERMAN2 is
ops a w i m p e :  -> Bool .
eq  (a and w) = p .
***> Contrapositive: (not a  implies i) == (not i implies a)
eq  not i =  a .
eq  not m =  w .
eq  p = false .
eq  e = (not i) and (not m)  .
endfm

***> Using reduce we ask is the conclusion true.
red not e .