*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Makarius <makarius at sketis.net>*Date*: Tue, 29 May 2012 23:00:05 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201205270818.q4R8IUWm022240@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205251146380.8953@macbroy22.informatik.tu-muenchen.de> <201205270818.q4R8IUWm022240@poisson.math.northwestern.edu>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sun, 27 May 2012, Bill Richter wrote:

Thanks, Makarius, I'll run your code and study it. Is this explained somewhere in the Isabelle dox, or could you explain it better: We are doing precise single step reasoning here, which means all the slots for the rules need to be filled in the correct order. This is not Mizar or any of the Mizar modes for HOL, which are centered around classic predicate logic with some builtin proof automation to bridge larger gaps. I would have said FOL instead of predicate logic, does that mean the same? I'm not an expert in FOL, but I think FOL proofs tend to be very tedious, and the builtin Mizar proof automation turns these FOL proofs into something that is a real pleasure to code up. Is that right? And Isabelle (Isar?) is doing something different from that?

Yes, and thus locales are definitely a real advantage of Isabelle over HOL Light right now. Still, I wonder why one can't just define all the sets you'd want in HOL Light (only very lightly typed) to get something like a locale.

That is, I think of your locale as something close to FOL Tarskiaxiomatic geometry proofs. But instead we could look at all models ofTarski's axioms, a model being some sets and functions with someproperties. Can you do this in Isabelle too?

Makarius

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

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

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

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

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

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

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

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

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

- Previous by Date: [isabelle] includes bundle works only in first case
- Next by Date: Re: [isabelle] includes bundle works only in first case
- 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 May 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