From: Ben Hocking <benjaminhocking@gmail.com>
Subject: Re: Having trouble proving modus ponens using checker
Date: Tue, 4 Sep 2012 07:24:25 -0700 (PDT)
Date: 2012-09-04T07:24:25-07:00 [thread overview]
Message-ID: <c0acfa15-1895-46c6-8172-6a202c04d559@googlegroups.com> (raw)
In-Reply-To: <f2ed6dda-4e8b-4c5c-8a99-011167eb8158@googlegroups.com>
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
prev parent reply other threads:[~2012-09-04 14:24 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-09-04 13:49 Having trouble proving modus ponens using checker Ben Hocking
2012-09-04 14:24 ` Ben Hocking [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox