Maude-help mailing list

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

If you are indeed using equality to represent logical equivalence then equational rewriting is a sound mechanism for deduction. Rewriting can also be used to represent logical deduction in a couple of other ways, but here the relation is not symmetric and it is better to use rules:

(1) As consequence: rl a => b . means a is a consequence of b. Here you want to prove phi and so you rewrite it. If you reach logical truth you have a direct proof of phi.

(2) As entailment: rl a => b . means a entails b. Here you want to prove phi, and so you rewrite its negation, ~ phi. If you reach logical false, you have proved phi by contradiction.

Critical pairs are a problem whenever you do equational rewriting (i.e. only take a single, implementation defined path through the graph of available rewrites). They correspond to overlaps, where a lhs can match the same term as subterm of another lhs, and it becomes crucial which rewrite step is attempted first.

fmod CRIT-PAIR is
  sort Foo .
  ops a b : -> Foo .
  ops f g : Foo -> Foo .

  eq f(a) = g(b) .
  eq a = b .
endfm

red f(a) == g(b) .

Here the equality fails, even though the first equation states that f(a) = g(b). The reason is that the _==_ operator is only valid for confluent terminating rewrite systems, the system above is non-confluent because f(a) can rewrite to g(b) by the first equation, and f(b) by the second equation. Not all critical pairs produce non-confluence, and term rewriting systems with critical pair can often be "completed".

fmod CRIT-PAIR2 is
  sort Foo .
  ops a b : -> Foo .
  ops f g : Foo -> Foo .

  eq f(a) = g(b) .
  eq f(b) = g(b) .
  eq a = b .
endfm

red f(a) == g(b) .

Detecting critical pairs, confluence checking, and completion are fundamental concepts in the study of term rewriting systems; see here for example:

http://en.wikipedia.org/wiki/Knuth%E2%80%93Bendix_completion_algorithm

Steven

On 1/14/14 2:56 AM, Patrick Browne wrote:

Steven,
Thanks for your reply. You have given me plenty of topics to study.
In particular I know nothing of critical pairs.
In this case is the fact that the queries for SUPERMAN2 terminate and seem consistent with intuition any grounds for thinking that the rewriting provides a valid proof of the results?

Thanks,
Pat

On 13/01/14, Steven Eker <eker AT csl.sri.com> wrote:

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 <Maude-help AT cs.uiuc.edu>
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help