comp.lang.ada
 help / color / mirror / Atom feed
From: Ben Hocking <benjaminhocking@gmail.com>
Subject: Having trouble proving modus ponens using checker
Date: Tue, 4 Sep 2012 06:49:03 -0700 (PDT)
Date: 2012-09-04T06:49:03-07:00	[thread overview]
Message-ID: <f2ed6dda-4e8b-4c5c-8a99-011167eb8158@googlegroups.com> (raw)

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



             reply	other threads:[~2012-09-04 13:49 UTC|newest]

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2012-09-04 13:49 Ben Hocking [this message]
2012-09-04 14:24 ` Having trouble proving modus ponens using checker Ben Hocking

replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox