Basis for modelling | Proof assistants and Automated theorem provers | ||
Systems based on logical frameworks | |||
LF (logical framework) | LCF theorem prover, Twelf | ||
Hereditary Harrop formulae | Isabelle, Lambda-PROLOG | ||
|
Coq, LEGO theorem prover | ||
Intuitionistic type theory | NuPRL, MetaPRL, ALF theorem prover | ||
Linear logic | Forum meta-logic | ||
Systems based on direct symbolic representations | |||
Hilbert calculus | Metamath | ||
First-order logic | Mizar, Vampire theorem prover | ||
|
HOL theorem prover, Prototype Verification System, ProofPower | ||
Equational logic | Gabbay's deductive system, OBJ3 | ||
Rewriting logic | Maude system, ELAN |
To incorporate: Automath, NQTHM, MinLog, ACL2, Otter (software).