H ? « ‹ ← → › »

Language peer sets for Isabelle:
United Kingdom↑
United Kingdom/1988↑
Designed 1988 ↑
1980s languages ↑
Fifth generation↑
Late Cold War↑

Isabelle(ID:3672/isa004)

alternate simple view
Country: United Kingdom
Designed 1988
Published: 1988

Isabelle is a highly automated generic theorem prover written in
Standard ML.  
New logics are introduced by specifying their syntax and
rules of inference.  Proof procedures can be expressed using tactics
and tacticals.
Isabelle comes with 8 different logics, including LCF,
some modal logics, first-order logic, Zermelo-Fraenkel set theory, and
higher-order logic.

Structures:
Related languages
SML/NJ → Isabelle   Written using
Isabelle → Isabelle/HOL   Adaptation of
Isabelle → Isabelle-91   Evolution of
References:
  • Paulson, Lawrence C. (1988) Paulson, Lawrence C. "A formulation of the simple theory of types (for Isabelle)" December 1988 Proceedings of the International Conference on Computer Logic Abstract
  • Paulson, Lawrence C. (1988) Paulson, Lawrence C. "Isabelle: The Next Seven Hundred Theorem Provers" Proceedings of the 9th International Conference on Automated Deduction May 1988 Abstract
  • Wiedijk, Freek (1998) Wiedijk, Freek "The Fifteen Provers of the World" Abstract
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder