From: Ben Hocking <benjaminhocking@gmail.com>
Subject: Proving B given that A >= 0 -> B and A < 0 -> B
Date: Mon, 3 Sep 2012 07:19:28 -0700 (PDT)
Date: 2012-09-03T07:19:28-07:00 [thread overview]
Message-ID: <c05c6143-cbde-4916-8655-e16197981997@googlegroups.com> (raw)
I've run into this scenario a couple times and I have yet to come up with a simple solution. I have the following rule in my .rlu file:
combine_cases2: PREDB may_be_deduced_from [A >= 0 -> PREDB, A < 0 -> PREDB, goal(checktype(A, number))].
(Evidently there's no boolean type in prolog, so I can't assert that PREDB is of type boolean. Correct me if I'm wrong on that.)
Unfortunately, this rule doesn't seem to be helping me on the following:
…
H15: x - a * (y - z) div b >= 0 ->
my_fn(x - a * (y - z) div b) <= c .
H16: x - a * (y - z) div b < 0 ->
my_fn(x - a * (y - z) div b) <= c .
…
->
C1: my_fn(x - a * (y - z) div b) <= c .
I'm also open to solving this problem using "checker", but I'm not sure what rules I would use on the .siv file, either.
Thanks for any help or insight.
-Ben
next reply other threads:[~2012-09-03 14:19 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-09-03 14:19 Ben Hocking [this message]
2012-09-04 8:43 ` Proving B given that A >= 0 -> B and A < 0 -> B Phil Thornley
2012-09-04 14:23 ` 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