Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

A several points:

(1) BOOL converts all expressions in to polynomial form (in the Boolean ring with "+" as "xor" and "*" and "and") and then uses the well known confluent and terminating AC term rewriting system to put this in a unique normal form, which might be true or false, but in general is an xor of products over the unknowns. This is sufficient for deciding equalities between Boolean expressions, assuming the unknowns are distinct.

(2) Equality between Boolean expressions (i.e. equations and == tests) is logically two-way implication.

(3) Adding defining equations for unknowns such as:
  eq   ee = (e implies ((not i) and (not m)))  .
is fine since ee is not otherwise known, and thus there can be no critical pair.

(4) Adding new pattern in the lhs of an equation is asking for trouble:
  eq  not i =  a .
Here the lhs forms a critical pair with the lhs of:
  eq not A = A xor true .
from the BOOL-OPS module in the prelude, and it is undefined whether "not i" becomes "a" or "i xor true"; i.e. the term rewriting system is no longer confluent, which breaks the basic contract for equations to behave correctly.

(5) It's possible to use the Maude LTL sat-solver to check if a formula is universally false or has a model (i.e. a satisfying assignment). If the negation of a formula phi is universally false, then phi must be universally true.

load model-checker

fmod SUPER-SAT is
  pr SAT-SOLVER .

  ops a w i m p e aw na nw np ee : -> Formula .

  eq aw = (a /\ w) -> p .
  eq na = ~ a -> i .
  eq nw = ~ w -> m .
  eq np = ~ p .
  eq ee = e -> (~ i /\ ~ m) .
endfm

red satSolve((aw /\ na /\ nw /\ np /\ ee) ->  ~ e) .
red satSolve(~((aw /\ na /\ nw /\ np /\ ee) ->  ~ e)) .

red satSolve((aw /\ na /\ nw /\ np /\ ee) -> e) .
red satSolve(~((aw /\ na /\ nw /\ np /\ ee) -> e)) .

Again it is a bad idea to write lhs patterns involving the defined symbols of LTL since these will likely conflict with (i.e. have critical pairs with) the defining equations in model-checker.maude

Steven

On 1/11/14 7:50 AM, Patrick Browne wrote:

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 .

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help