*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Tue, 01 May 2012 11:13:03 +1200*Cc*: Josef Urban <josef.urban at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201204300355.q3U3tgBd020699@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <201204300355.q3U3tgBd020699@poisson.math.northwestern.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120412 Thunderbird/11.0.1

On 30/04/12 15:55, Bill Richter wrote: > How do we code up first order logic (FOL) proofs that follow from some > FOL axioms? I really think the Isabelle dox ought to explain this. I think what you might be looking for is Isabelle's locales. In my thesis, I used a locale (actually, several incremental locales) to characterize Tarski's axioms. Then, I could prove consequences of the axioms inside the locales, and I could define models of the axioms outside the locales that I later proved were instances of the locales. Tim <><

**Attachment:
signature.asc**

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