TTTools

HOL

https://hol-theorem-prover.org/

The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. (lang: ML).

The HOL Light theorem prover https://www.cl.cam.ac.uk/~jrh13/hol-light/

The LEGO Proof Assistant

http://www.dcs.ed.ac.uk/home/lego/

LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack in Edinburgh using NJ/ML. It implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT). LEGO is a powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs. For example, features of the system like argument synthesis and universe polymorphism make proof checking more practical by bringing the level of formalization closer to that of informal mathematics. The higher-order power of its underlying type theories, and the support of specifying new inductive types, provide an expressive language for formalization of mathematical problems and program specification and development. Particularly, Zhaohui Luo's type theory UTT includes:

• type universes, which make it possible to formalize abstract mathematics

• strong sum types, which can be used to naturally express abstract structures, mathematical theories and program specifications

• a schema for inductive data types, which captures the common inductive structures in programming languages and mathematics

  LEGO may also be used to formalize different logical systems and prove theorems based on the defined logics, following the philosophy of the LF.

Logics and Type Systems - Herman Geuvers