* Having trouble proving modus ponens using checker
@ 2012-09-04 13:49 Ben Hocking
2012-09-04 14:24 ` Ben Hocking
0 siblings, 1 reply; 2+ messages in thread
From: Ben Hocking @ 2012-09-04 13:49 UTC (permalink / 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
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Having trouble proving modus ponens using checker
2012-09-04 13:49 Having trouble proving modus ponens using checker Ben Hocking
@ 2012-09-04 14:24 ` Ben Hocking
0 siblings, 0 replies; 2+ messages in thread
From: Ben Hocking @ 2012-09-04 14:24 UTC (permalink / raw)
On Tuesday, September 4, 2012 9:49:03 AM UTC-4, Ben Hocking wrote:
> 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
Never mind. Using "simplify." was all I needed.
-Ben
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2012-09-04 14:24 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-09-04 13:49 Having trouble proving modus ponens using checker Ben Hocking
2012-09-04 14:24 ` Ben Hocking
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox