Editing Automated theorem proving (section)

==Benchmarks, competitions, and sources ==
The quality of implemented systems has benefited from the existence of a large library of standard [[Benchmark (computing)|benchmark]] examples—the [[Thousands of Problems for Theorem Provers]] (TPTP) Problem Library<ref>{{cite web|last=Sutcliffe|first=Geoff|title=The TPTP Problem Library for Automated Theorem Proving|url=http://www.tptp.org/|access-date=15 July 2019}}</ref>—as well as from the [[CADE ATP System Competition]] (CASC), a yearly competition of first-order systems for many important classes of first-order problems.

Some important systems (all have won at least one CASC competition division) are listed below.
* [[E theorem prover|E]] is a high-performance prover for full first-order logic, but built on a [[superposition calculus|purely equational calculus]], originally developed in the automated reasoning group of [[Technical University of Munich]] under the direction of [[Wolfgang Bibel]], and now at [[Baden-Württemberg Cooperative State University]] in [[Stuttgart]].
* [[Otter (theorem prover)|Otter]], developed at the [[Argonne National Laboratory]], is based on [[first-order resolution]] and [[paramodulation]]. Otter has since been replaced by [[Prover9]], which is paired with [[Mace4]].
* [[SETHEO]] is a high-performance system based on the goal-directed [[model elimination]] calculus, originally developed by a team under direction of [[Wolfgang Bibel]]. E and SETHEO have been combined (with other systems) in the composite theorem prover E-SETHEO.
* [[Vampire theorem prover|Vampire]] was originally developed and implemented at [[University of Manchester|Manchester University]] by [[Andrei Voronkov]] and Kryštof Hoder. It is now developed by a growing international team. It has won the FOF division (among other divisions) at the CADE ATP System Competition regularly since 2001.<ref>{{cite web |title=History |url=https://vprover.github.io/history.html |website=vprover.github.io}}</ref>
* Waldmeister is a specialized system for unit-equational first-order logic developed by Arnim Buch and Thomas Hillenbrand. It won the CASC UEQ division for fourteen consecutive years (1997–2010).
* [[SPASS]] is a first-order logic theorem prover with equality. This is developed by the research group Automation of Logic, [[Max Planck Institute for Computer Science]].

The Theorem Prover Museum<ref>{{cite web|url=https://theoremprover-museum.github.io |title=The Theorem Prover Museum |access-date=2022-11-20 |publisher=[[Michael Kohlhase]]}}</ref> is an initiative to conserve the sources of theorem prover systems for future analysis, since they are important cultural/scientific artefacts. It has the sources of many of the systems mentioned above.