Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.