[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] ACL2 and Axiom

From: Tim Daly
Subject: [Axiom-developer] ACL2 and Axiom
Date: Fri, 01 Oct 2010 22:54:39 -0400
User-agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv: Gecko/20100825 Thunderbird/3.1.3

 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.)

  (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-AV: E=Sophos;i="4.57,267,1283749200";
    X-SpamScore: -21
    X-BigFish: VPS-21(z2b68kz14e0M1432N98dN9371Pzz1202hzz8275bhz32i2a8h61h)
    X-Spam-TCS-SCL: 0:0
    X-WSS-ID: 0L9MCE2-02-D5L-02
    From: "Russinoff, David"<address@hidden>
    CC: "address@hidden"<address@hidden>
    Date: Fri, 1 Oct 2010 10:58:19 -0500
    Thread-Topic: algebra problem
    Thread-Index: ActhgTQ4BprFQxjpQaim1LoG0ECYFAAAEOLR
    Accept-Language: en-US
    Content-Language: en-US
    acceptlanguage: en-US
    X-MIME-Autoconverted: from quoted-printable to 8bit by 
id o91Fx8Dc014294
    X-Loop: address@hidden
    X-Sequence: 211
    X-no-archive: yes
    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: address@hidden address@hidden On Behalf Of Pete Manolios 
    Sent: Friday, October 01, 2010 10:55 AM
    To: Russinoff, David
    Cc: address@hidden
    Subject: Re: algebra problem


    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 

    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
    <address@hidden>  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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]