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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,c7103d08119b3a51,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.224.207.72 with SMTP id fx8mr11642078qab.2.1346766543948; Tue, 04 Sep 2012 06:49:03 -0700 (PDT) Received: by 10.52.34.115 with SMTP id y19mr2298985vdi.1.1346766543910; Tue, 04 Sep 2012 06:49:03 -0700 (PDT) Path: da15ni7637554qab.0!nntp.google.com!b19no790215qas.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 4 Sep 2012 06:49:03 -0700 (PDT) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=8.25.3.17; posting-account=hKGsDAoAAAC9HB_9misjykjawYQeT_yf NNTP-Posting-Host: 8.25.3.17 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Having trouble proving modus ponens using checker From: Ben Hocking Injection-Date: Tue, 04 Sep 2012 13:49:03 +0000 Content-Type: text/plain; charset=ISO-8859-1 Date: 2012-09-04T06:49:03-07:00 List-Id: I have the following VC: ==================== H1: a - b * (c - d) div e < 0 -> my_fn(a - b * (c - d) div e) <= f H2: a - b * (c - d) div e < 0 --> C1: my_fn(a - b * (c - d) div e) <= f ==================== I've tried the following: ==================== [EXECUTE]: infer c#1 using implies. infer c # 1 using implies. Cannot infer my_fn(a - b * (c - d) div e) <= f using rule-family implies. FAIL [EXECUTE]: infer c#1 using implies(3). infer c # 1 using implies(3). Cannot infer my_fn(a - b * (c - d) div e) <= f using rule implies(3). FAIL [EXECUTE]: infer c#1 using implies(3) from [2, 1]. infer c # 1 using implies(3) from [2, 1]. Cannot infer my_fn(a - b * (c - d) div e) <= f using rule implies(3). FAIL ==================== Does anybody know what I might be doing wrong? The rule implies(3) is defined in LOGIC.RUL as: implies(3): true -> A may_be_replaced_by A. That's the closest I can find to modus ponens. Thanks for any help, -Ben