Well you've finally given me an example to motivate me.
We've had the "in-plan" task to embed ACL2 under Axiom (since
both run in common lisp) so we can use the facilities of ACL2
in our computer algebra system. I suspect there will be a bit of
dancing to get the initialization correct and to hide the top
level interface but Axiom and ACL2 live in different packages
so there shouldn't be much conflict.
In particular, this facility is of interest as a reasoning mechanism
behind a "proviso" facility, that is, "1/x provided x != 0".
Does ACL2 handle reasoning about interval arithmetic?
Are there particular books in ACL2 I should study?
Also, the SUBSETP test failed in GCL-2.6.8.
I will pull the latest GCL sources and try again.
Tim Daly
Axiom Lead Developer
On 10/1/2010 12:11 PM, Matt Kaufmann wrote:
The following works. (I got the set-default-hints form from output of
the include-book form.)
(encapsulate
()
(local (include-book "arithmetic-5/top" :dir :system))
(local (set-default-hints
'((nonlinearp-default-hint stable-under-simplificationp
hist pspv))))
(defthm russinoff
(implies (and (rationalp a)
(rationalp b)
(rationalp c)
(<= 1 a)
(< 0 b)
(< 0 c)
(<= (expt a 2) (* b (+ c 1)))
(<= b (* 4 c)))
(< (expt (- a 1) 2) (* b c)))))
-- Matt
X-IronPort-MID: 58854409
X-IronPort-MID: 244575640
X-SBRS: 4.5
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result:
Ar4AAOyhpUzVx5rNkWdsb2JhbACXDYs+AQEBAQkLCgcRBB6sKZsDhUQEhFGIcxCCTYU3
X-IronPort-AV: E=Sophos;i="4.57,267,1283749200";
d="scan'208";a="244575640"
X-SpamScore: -21
X-BigFish: VPS-21(z2b68kz14e0M1432N98dN9371Pzz1202hzz8275bhz32i2a8h61h)
X-Spam-TCS-SCL: 0:0
X-WSS-ID: 0L9MCE2-02-D5L-02
X-M-MSG:
From: "Russinoff, David"<[email protected]>
CC: "[email protected]"<[email protected]>
Date: Fri, 1 Oct 2010 10:58:19 -0500
Thread-Topic: algebra problem
Thread-Index: ActhgTQ4BprFQxjpQaim1LoG0ECYFAAAEOLR
Accept-Language: en-US
Content-Language: en-US
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
acceptlanguage: en-US
X-Reverse-DNS: ausb3extmailp02.amd.com
X-MIME-Autoconverted: from quoted-printable to 8bit by riley.its.utexas.edu
id o91Fx8Dc014294
X-Loop: [email protected]
X-Sequence: 211
X-no-archive: yes
List-Owner:<mailto:[email protected]>
X-SpamAssassin-Status: No, hits=-1.7 required=5.0
X-UTCS-Spam-Status: No, hits=-110 required=165
Sorry, I meant to say a>= 1.
________________________________________
From: [email protected] [[email protected]] On Behalf Of Pete Manolios
[[email protected]]
Sent: Friday, October 01, 2010 10:55 AM
To: Russinoff, David
Cc: [email protected]
Subject: Re: algebra problem
David,
Here is the formalization of your conjecture in ACL2.
(thm (implies (and (rationalp a)
(rationalp b)
(rationalp c)
(< 0 a)
(< 0 b)
(< 0 c)
(<= (expt a 2) (* b (+ c 1)))
(<= b (* 4 c)))
(< (expt (- a 1) 2) (* b c))))
I tried it in ACL2s, the ACL2 Sedan (the one I hinted you might want to
try).
After 0 seconds, here is what it returned:
We falsified the conjecture. Here is the counterexample:
-- (A 1/4), (B 13/23) and (C 9/47)
On Fri, Oct 1, 2010 at 11:39 AM, Russinoff, David
<[email protected]> wrote:
> Here is a high school algebra problem that I've been staring at for
> a couple of hours and is making me feel pretty stupid.
>
> Proposition: Let a, b, and c be positive rationals. If a^2<= b*(c+1)
> and b<= 4*c, then (a-1)^2< b*c.
>
> Proof: sqrt(b*(c+1)) - sqrt(b*c)<= sqrt(4*c*(c+1)) - sqrt(4*c*c)
> < sqrt(4*c*c + 4*c + 1) - 2*c
> = 2*c + 1 - 2*c
> = 1.
> Therefore, a<= sqrt(b*(c+1))< sqrt(b*c) + 1 and a - 1< sqrt(b*c).
>
> I need an ACL2 proof. I should be able to prove it without mentioning
> square roots. As J says (I paraphrase), "If it's true, you can prove it.
> So what?" But I'm still staring and feeling stupid.
>
>
--
Pete Manolios
Northeastern University
http://www.ccs.neu.edu/home/pete
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
