How do I prove an asserted fact with LP?

• To: larch-interest@pa.dec.com
• Subject: How do I prove an asserted fact with LP?
• From: Patrice Chalin <chalin@cs.concordia.ca>
• Date: Tue, 11 Apr 95 17:16:57 -0400
• Cc: chalin@cs.concordia.ca
• Delivery-Date: Tue, 11 Apr 95 14:22:29 -0700

Consider the following simple LP script

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

Executing this script results in the following fact:

  |  % display facts
  |  
  |  Formulas:
  |  
  |  user.1: x = s

and the proof is suspended:

  |  % display proof
  |  
  |  Conjecture user.2: x = s
  |    Attempting a proof by normalization
  |  

At this point, how can I make use of the fact `user.1' to prove the conjecture
`user.2'?  I have tried the apply command, but that doesn't help: the system
still considers ``x = s'' to be in normal form.


I have found a work-around (although I hope there is another way): if I
assert ``(x = s) = true'' instead of ``x = s'' the proof succeeds

  |  
  |  Conjecture user.2
  |  [] Proved by normalization.
  |  

even though we seem to have the same facts

  |  % display facts
  |  
  |  Formulas:
  |  
  |  user.1: x = s

Patrice

• Re: How do I prove an asserted fact with LP?
• From: "Stephen J. Garland" <garland@larch.lcs.mit.edu>

• Prev: Re: How do I prove an asserted fact with LP?
• Next: Recommended: "Ten Commandments of Formal Methods"
• Index: Larch archive index