Re: [isabelle] Skolemization in first-order logic without the Axiom of Choice, Literature on Isabelle



The 1994 book is frequently cited, but it is merely the three manuals of the time joined together. Those manuals continued to be updated for years afterwards, so that book is a snapshot, and it doesn't present any theory. The 1989 paper covers Isabelle as a logical framework. In the past year or two, papers have emerged giving an account of the semantics of Isabelle/HOL, including type classes and other extended definitional mechanisms.

Larry Paulson



> On 3 Mar 2018, at 16:37, Ken Kubota <mail at kenkubota.de> wrote:
> 
> 2. If one publication (or maybe two) should be taken as main reference for 
> Isabelle (the logical framework, not an object logic like Isabelle/HOL)
> - preferably a printed publication instead of just an online file - which one 
> would you choose?
> The literature on Isabelle is so vast that it becomes difficult to single out a 
> specific publication.
> My first guess would be
> [29] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. 
> LNCS 828.
> which is newer than your 1989 article available online at
> 	https://arxiv.org/pdf/cs/9301105.pdf





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