# TTTools

## HOL

[https://hol-theorem-prover.org/](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/](https://www.cl.cam.ac.uk/~jrh13/hol-light/)

## The LEGO Proof Assistant

[http://www.dcs.ed.ac.uk/home/lego/](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
