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



Thanks Larry!

Well, I am personally interested in the axioms and rules of
Isabelle/Pure, since I would like to know how they compare to
HOL-Light, the other system which I am familiar. Am I mistaken, or
does Isabelle/Pure and all of its extensions ultimately construct
objects with a theorem type in SML in a similar fashion to the HOLs?
I know this is how HOL-Light functions - the constructor rules are all
given in a file thm.ml.  If this is how Isabelle functions, I'd be
curious to know all the primitive constructors for theorems.

Anyway, since my thesis will be given to logicians, I'm sure they'd
have other logics they'd be familiar with that they might want to
compare Isabelle/Pure's logic to.

~Matthew P. Wampler-Doty

On Thu, Jan 14, 2010 at 11:38 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 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.