* [Spark] Splitting 'and' conditions into multiple conditions
@ 2003-03-25 21:48 Lutz Donnerhacke
2003-03-26 9:41 ` Peter Amey
0 siblings, 1 reply; 2+ messages in thread
From: Lutz Donnerhacke @ 2003-03-25 21:48 UTC (permalink / raw)
The simplifier is often unable to prove easy conclusions, because conditions
given als assert, precondition, and postcondition occur as a single
conclusion.
Example:
C1: res__1 >= buf__first and res__1 <= buf__last and (res__1 >= 0 and res__1
<= 0) -> res__1 >= buf__first and res__1 <= buf__last .
Or do I misinterpret this line containing an implication?
Should the simplifier not able to handle this by transfering the frist part
to the hypothis?
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: [Spark] Splitting 'and' conditions into multiple conditions
2003-03-25 21:48 [Spark] Splitting 'and' conditions into multiple conditions Lutz Donnerhacke
@ 2003-03-26 9:41 ` Peter Amey
0 siblings, 0 replies; 2+ messages in thread
From: Peter Amey @ 2003-03-26 9:41 UTC (permalink / raw)
Lutz Donnerhacke wrote:
> The simplifier is often unable to prove easy conclusions, because conditions
> given als assert, precondition, and postcondition occur as a single
> conclusion.
>
> Example:
> C1: res__1 >= buf__first and res__1 <= buf__last and (res__1 >= 0 and res__1
> <= 0) -> res__1 >= buf__first and res__1 <= buf__last .
>
> Or do I misinterpret this line containing an implication?
> Should the simplifier not able to handle this by transfering the frist part
> to the hypothis?
Lutz,
We are always interested in collecting examples where the Simplifier can
be improved. You should note, however, that the Simplifier is just
that, it is not intended to be a heavyweight proof engine like PVS. The
idea is to limit what the Simplifier gets up to so as to maintain clear
traceability between what goes into it and what comes out and to avoid
the possibility of multiple substitutions leaving the formulae in a
worse state than they started. The unsimplified VCs that are left can
always be tacked with the interactive Prof Checker tool.
Peter
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2003-03-26 9:41 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2003-03-25 21:48 [Spark] Splitting 'and' conditions into multiple conditions Lutz Donnerhacke
2003-03-26 9:41 ` Peter Amey
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox