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



The short answer is that Isabelle/Pure is intuitionistic higher-order logic, and it is described in my paper "The foundation of a generic theorem prover", see http://www.cl.cam.ac.uk/~lp15/papers/isabelle.html

Unfortunately, this very old paper does not say anything about axiomatic type classes and other novelties that have been introduced since...

However, I'm not sure how meaningful it is to compare a logical framework with HOL-Light. They are doing different things.

Larry Paulson


On 14 Jan 2010, at 13:06, Matthew Wampler-Doty wrote:

> 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.