Ocaml, Coq, and ACL2

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Ocaml, Coq, and ACL2

Page, Bill
On Wednesday, October 19, 2005 9:52 AM C Y wrote:
> ...
> With apologies to Camm, there is one sense in which arriving at
> ocaml is neither full circle nor unattractive, and that is the
> coq theorem prover.  If there is indeed serious interest in
> backing Axiom with a powerful theorem prover, COQ is definitely
> up there on the list of candidates.  In fact, some work was done
> in France a while back on coq+Axiom - as yet I have not yet
> located a copy of that thesis, unfortunately.

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 provide:

\begin{ocaml}
...
\end{ocaml}

and

\begin{coq}
...
\end{coq}

on MathAction to 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.

> I think I posted here about it and got no response.

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

> ...
> I know the interest in this topic is spotty, but this is the
> time and place to raise the question - if we DO want to be
> able to back Axiom with formal provers, what are the design
> considerations that need to be taken into account?  What
> precisely will the prover be used to do, how would we interact
> with it, and how would we store and use the results?

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.

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.

So far I have not installed ACL2 on the axiom-developer server
yet, but if even one other person says they are interested then
I would be glad to do that and also make in available on MathAction
via

\begin{acl2}
...
\end{acl2}

Regards,
Bill Page


_______________________________________________
Axiom-developer mailing list
[hidden email]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Ocaml, Coq, and ACL2

Martin Rubey
I'd just like to add that Renaud Rioboo is working on Focal, which seems to be
exactly what Cliff Yapp is looking for. However, it is (and will stay)
disconnected from Axiom.

As far as I know it is based on Coq and Ocaml. See

http://focal.inria.fr/site/manual.html

I have no idea in what sense a theorem prover would be useful in a
CAS-context. Maybe Bruno Buchberger has some answers:

http://www.risc.uni-linz.ac.at/research/theorema/description/

Martin



_______________________________________________
Axiom-developer mailing list
[hidden email]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
C Y
Reply | Threaded
Open this post in threaded view
|

Re: Ocaml, Coq, and ACL2

C Y

--- Martin Rubey <[hidden email]> wrote:

> I'd just like to add that Renaud Rioboo is working on Focal, which
> seems to be exactly what Cliff Yapp is looking for. However, it is
> (and will stay) disconnected from Axiom.

Neat!

> As far as I know it is based on Coq and Ocaml. See
>
> http://focal.inria.fr/site/manual.html

I'll add that to my reading list.

> I have no idea in what sense a theorem prover would be useful in a
> CAS-context. Maybe Bruno Buchberger has some answers:
>
> http://www.risc.uni-linz.ac.at/research/theorema/description/

I've seen a couple efforts along those lines scattered around, but I
haven't taken the time to study them in depth.  Guess I should do that
before anything else.

Cheers, and thanks!

CY


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


_______________________________________________
Axiom-developer mailing list
[hidden email]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
C Y
Reply | Threaded
Open this post in threaded view
|

Re: Ocaml, Coq, and ACL2

C Y
In reply to this post by Page, Bill


--- "Page, Bill" <[hidden email]> 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/


_______________________________________________
Axiom-developer mailing list
[hidden email]
http://lists.nongnu.org/mailman/listinfo/axiom-developer