Re: How do I prove an asserted fact with LP?

To: Patrice Chalin <chalin@cs.concordia.ca>
Subject: Re: How do I prove an asserted fact with LP?
From: "Stephen J. Garland" <garland@larch.lcs.mit.edu>
Date: Tue, 11 Apr 95 18:36:55 -0400
Cc: larch-interest@pa.dec.com
Delivery-Date: Tue, 11 Apr 95 15:39:44 -0700
In-Reply-To: Your message of "Tue, 11 Apr 95 17:16:57 EDT." <9504112116.aa28436@manitou.cs.concordia.ca>

The reason that the proof

    declare sort S
    declare op   s: -> S
    declare var  x: S
    assert  x = s
    prove   x = s

does not succeed automatically in LP is that the assertion "x = s" cannot be
oriented into a rewrite rule (because the left side of a rewrite rule cannot be
a variable, and the right side cannot introduce a variable that is not on the
left side).

The work-around succeeds because LP orients the assertion "(x = s) = true" into
the rewrite rule "x = s -> true", which normalizes the conjecture to "true".

The success of the work-around suggests that LP should automatically orient
formulas like "x = s" into rewrite rules "x = s -> true".  I will put that
suggestion on the agenda for a future release.

Another work-around that uses the original unorderable axiom is as follows:
    prove x = s by contradiction
      instantiate x by xc in formula

Reference(s):

How do I prove an asserted fact with LP?

From: Patrice Chalin <chalin@cs.concordia.ca>

Prev: CU-DCS-TR-95-04: Shortcomings of LCL 2.4
Next: How do I prove an asserted fact with LP?
Index: Larch archive index