*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Slawomir Kolodynski <skokodyn at yahoo.com>*Date*: Mon, 4 Jun 2012 00:37:49 -0700 (PDT)*Reply-to*: Slawomir Kolodynski <skokodyn at yahoo.com>

>There is, of course, Isabelle/ZF, which does use FOL and the ZF axioms Is there a deep reason to code geometry axioms inside HOL? It seems to me it would be more natural to build Tarski geometry logic based on FOL, in the similar way like ZF logic is built on FOL. slawekk http://savannah.nongnu.org/projects/isarmathlib Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

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

- Previous by Date: [isabelle] Verification of C Programs
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- 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