[Axiom-developer] Re: Ocaml, Coq, and ACL2

[C Y]

--- "Page, Bill" <address@hidden> wrote:

> I already have Ocaml and Coq running on the axiom-developer.org
> server. If there is some interest, it would not be difficult for
> me to [snip] allow these to be accessed through the web
> like {axiom} {spad} {aldor} and {reduce}. This would not
> provide axiom/coq integration as such, but at least it would
> provide the possibility of exhibiting a coq proof along with
> some Axiom code should an author wish to do that.

Sounds interesting, but it might not be needed for a while yet, if at
all - I certainly have a long learning curve ahead of me with regards
to coq.  

> I am definitely interested by lack time right now to do
> anything serious.

Know that feeling...

> As you know, I am rather put-off by just "talking" about doing
> these things. Since quite a lot of code is freely available and
> easily accessed, I would prefer to just to dig-in and work/play
> with one or more of these tools ... then, maybe later, decide on
> which might be best and what if anything we really want to do
> with Axiom and theorem proving software.

Fair enough.  OK, I'll start digging.

> The "other" proof system is obviously of interest would be ACL2.
> Camm and some of the other lisp developer have a good connection
> to that project and so if we were to work with ACL2 and Axiom,
> I think we could expect a lot of support.

Yes, ACL2 and HOL were my other main interests in this department, with
Otter being of possible interest due to a somewhat different approach
(I still don't fully understand all the differences.)  However, proof
logic is a topic in and of itself so clearly there is a lot to learn to
be able to use any of these tools to do anything interesting/useful, so
I guess I'd better focus on the dimension and unit stuff first rather
than get sucked into proof issues.  

Cheers,
CY


                
__________________________________ 
Yahoo! Music Unlimited 
Access over 1 million songs. Try it free.
http://music.yahoo.com/unlimited/