Isabelle(ID:3672/isa004)

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. "A formulation of the simple theory of types (for Isabelle)" December 1988 Proceedings of the International Conference on Computer Logic view details Abstract:
  • Paulson, Lawrence C. "Isabelle: The Next Seven Hundred Theorem Provers" Proceedings of the 9th International Conference on Automated Deduction May 1988 view details Abstract:
  • Wiedijk, Freek "The Fifteen Provers of the World" view details Abstract: We compare the styles of several proof assistants for mathematics. We present Pythagoras' proof of the irrationality of pi both informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq, (5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX, (10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl, (15)O­mega.