The Isabelle theorem prover an interactive theorem proving framework, a successor of the HOL theorem prover.

External link

See also: theorem prover.