From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,b15074035c1cfe43 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-03-26 01:39:39 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!fu-berlin.de!uni-berlin.de!213.155.153.242!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: [Spark] Splitting 'and' conditions into multiple conditions Date: Wed, 26 Mar 2003 09:41:24 +0000 Message-ID: <3E8175C4.80500@praxis-cs.co.uk> References: NNTP-Posting-Host: 213.155.153.242 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: fu-berlin.de 1048671578 79246197 213.155.153.242 (16 [69815]) User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.0.2) Gecko/20030208 Netscape/7.02 X-Accept-Language: en-us, en Xref: archiver1.google.com comp.lang.ada:35717 Date: 2003-03-26T09:41:24+00:00 List-Id: 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