[Axiom-developer] Re: ACL2 list

[root]

(journaling ACL2 note)

Matt,

The referenced web page item is mine, not David's. (I'm the lead
developer on Axiom.)  I worked with Nqthm years ago (trying to prove a
rule based program written in OPS5) and have recently tried to spin up
on ACL2. The misunderstandings are mine. We've emailed each other a
long time ago but the whole discussion died because I'm still buried
under making Axiom open source. The use and support of ACL2 in Axiom
is, as you can see, still on the todo list.

Axiom lacks two fundamental things.  First, Axiom does not support
proofs. I believe I can correct this issue in the next few years and
ACL2 seems like a well-founded system to use as a basis. Exactly how
this should be done is an open research question. I have some ideas
but I need a running Axiom system to do the research work.

Second, Axiom's algorithms are unproven.  It is going to take
considerable research to figure out how to match ACL2's model to
Axiom's model. I spent a fair amount of time reading ACL2 documents
and Dijkstra's work last summer (shortly after his death) and
pondering this question. At the moment it's all "on the shelf". If you
look at Axiom with a 30 year timeframe it is unacceptable that the
algorithms are unproven. The answers given will still be valid 30
years from now but how can we trust a system without at least
attempting to prove it correct?

It is true that Chandy and Misra have nothing to do with ACL2 but they
formed part of my background research on the subject. The latest piece
of background reading (unmentioned on the webpage) is on MetaPRL. 

My apologies for spamming the ACL2 list. 

Tim Daly
address@hidden
address@hidden

=====================================================================
X-Original-To: address@hidden
Date: Wed, 13 Aug 2003 13:26:04 -0500
From: Matt Kaufmann <address@hidden>
To: address@hidden
Cc: address@hidden, address@hidden, address@hidden
Subject: ACL2 list
X-UIDL: BoC!!~6"#!'O2!!>ja!!

Hi --

I notice that you just joined the ACL2 list.  Welcome!

I have probably been remiss in waiting to point something about about the ACL2
list.  I believe that most ACL2 users, while very interested in using GCL, are
not likely to be interested in GCL implementation/development issues.  It's
completely up to you (and Camm, and other GCL people) what to email to the ACL2
list, but I thought I should mention this.

On another note, you mention the following, and I have some comments below.

  In http://www.nongnu.org/axiom/

   BOYER-MOORE THEOREM PROVER INTEGRATION
    Motivation: Computational logic is a branch of computer mathematics
                that is not currently available in Axiom. The Boyer-Moore
                theorem prover, written in common lisp, provides a good
                general purpose platform to study the interaction of the
                theorem proving systems with Axiom
  -  Contact Boyer & Moore
  -  Contact Chandy & Misra
  -  Download ACL2
     Build ACL2
     Invoke ACL2 from Axiom
     Integrate ACL2 into Axiom
       Use Dijkstra's methods against SetCategory
     Draft research paper

The Boyer-Moore theorem prover, also called Nqthm, is indeed a product of Bob
Boyer and J Moore.  ACL2 is authored by me (Matt Kaufmann) and J Moore, albeit
with significant early contributions from Boyer, who however is no longer
involved (by his choice).

I believe that integrating ACL2 into Axiom could be an interesting project, and
if you succeed I (and others on the ACL2 list, I believe) would like to know
about it.  It would be especially interesting if Axiom could somehow contribute
to ACL2's proofs, but that may be a difficult problem (if for no other reason
than that their logics are presumably different).

By the way, I'm not aware of any connection that Chandy or Misra have to this
stuff.

Regards,
Matt