ATP Systems

Classic FOF → CNF-Saturation Systems

Non-CNF-Saturation Systems

Finite Model Finders

Systems with Arithmetic Capabilities

Higher-order Systems

Meta-Systems

(Higher-order) Proof Assistants (partially "A")

The Theorem Prover Museum