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 |
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 |
--- 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 |
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 |
Free forum by Nabble | Edit this page |