*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Mon, 4 Jun 2012 08:18:34 +0100*Cc*: Tjark Weber <webertj at in.tum.de>, Konrad Slind <konrad.slind at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201206040444.q544iMiZ020423@poisson.math.northwestern.edu>*References*: <201206022353.q52Nredm012382@poisson.math.northwestern.edu> <1338717861.1859.19.camel@weber> <201206040444.q544iMiZ020423@poisson.math.northwestern.edu>*Sender*: ramana.kumar at gmail.com

On Mon, Jun 4, 2012 at 5:44 AM, Bill Richter <richter at math.northwestern.edu>wrote: > Thanks, Tjark and Konrad! I'll read the HOL paper, which looks pretty > old, and so is maybe something that everyone just assumes nowadays. I > don't know about those other first-order reasoning > Automated_theorem_provers, or why folks don't use them. Possible reasons include: 1. FOL isn't expressive enough for their problems. It might technically be able to express something, but not nicely. 2. The automated provers can't solve their problems, at least not without a lot of help, and that help is tedious to give. 3. Some automated provers don't generate complete explicit proofs, and so have to be trusted; this is harder than trusting a simple proof checker. That having been said, I'm under the impression that the world of automated proving is always getting better. I don't know much about it because I don't live day-to-day in that world. Ideally, interactive provers should only benefit from progress in automation, since automatic tools can be integrated into interactive proof development environments. > My interest > in proof assistants (HOL Light, Isabelle, Coq) is that Tom Hales is > using them to formalize his Kepler conjecture proof. > > it tends to puzzle mathematicians with an interest in foundations > who have been taught that everything rests on FOL and ZFC. > > Tjark, you understand my confusion! Is something written about this? > I do contend that it's true what mathematicians are taught, but it may > not appear to be true at the technical level that proof assistants > operate on. That's of course fine, but I need to see the underlying > FOL and ZFC, even if the proof assistants aren't coded that way. > It's not just a matter of how the proof assistant is coded. The underlying logic of Isabelle/HOL is not FOL. (There is, of course, Isabelle/ZF, which does use FOL and the ZF axioms.) The piece of writing I think you might find enlightening is Andy Pitts's document on the semantics of HOL. It is the "Logic" manual available here http://hol.sourceforge.net/documentation.html. Note it is for the HOL4 system, not Isabelle/HOL, but since it's mainly about the logic, HOL, itself, that those proof assistants basically share, this shouldn't matter too much. It gives a precise description of the syntax and semantics of HOL. The semantics is given in terms of set-theoretic models, with which you're probably more familiar. I'll be happy to answer any questions about it. I was thinking of giving you syntax and semantics of FOL and then of HOL so you could see them compared, but that document is better presented than what I would have written. (By the way, FOL formulas can be embedded in HOL.) > > -- > Best, > Bill > >

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Tjark Weber

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: Re: [isabelle] proof dags?
- Next by Date: [isabelle] Verification of C Programs
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list