Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?



Isabelle/Pure sets up the logical framework on which logics themselves are defined, so its axioms are no relevance to you unless you were comparing Isabelle/Pure with another logical framework.

The axioms of Isabelle/HOL can be found by searching for "axioms" and "axiomatization" declarations. Nearly all of them are in the file HOL.thy, and they specify the logical connectives and quantifiers. The axiom of infinity is introduced later, in Nat.thy, and the axiom of choice later still, in Hilbert_Choice.thy. All these will be visible if you work in the theory Main.
Larry Paulson


On 14 Jan 2010, at 01:16, Matthew Wampler-Doty wrote:

> Dear all,
> 
> I'm formalizing a completeness theorem for a modal logic my MSc thesis
> in Isabelle/HOL, and I would like to have a section outlining the
> axioms and basic rules Isabelle/HOL (since it's an LCF system after
> all, so there shouldn't be too many of these).  I can't seem to figure
> out how to find these out; they appear to be scattered across
> Isabelle/Pure and Isabelle/HOL.  Can someone direct me to a listing of
> all the rules and axioms?
> 
> Thanks!
> 
> ~Matthew P. Wampler-Doty
> 






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