System E

E

People

Stephan Schulz, Simon Cruanes, Martin Moehrmann, Petar Vukmirovic (major contributions) and others.

Short Description

E 3.0 is a purely equational theorem prover for many-sorted first-order logic with equality, and for monomorphic higher-order logic. It consists of an (optional) clausifier for pre-processing full first-order formulae into clausal form, and a saturation algorithm implementing an instance of the superposition calculus with negative literal selection and a number of redundancy elimination techniques, optionally with higher-order extensions. E is based on the DISCOUNT-loop variant of the given-clause algorithm, i.e., a strict separation of active and passive facts. No special rules for non-equational literals have been implemented. Resolution is effectively simulated by paramodulation and equality resolution. As of E 2.1, PicoSAT can be used to periodically check the (on-the-fly grounded) proof state for propositional unsatisfiability.

Capabilities

• Proving
• Model finding

Input Language

E supports SETHEO's LOP, TPTP-1/2 and the current TPTP-3/TSTP syntax. If the user does explicitly requests a syntax, it tries to automatically detect the input syntax, and usually succeeds. In particular, it should always recogizde TPTP-3 files correctly.

Output

E follows the SZS reporting standard.

Proof Format

In addition to TPTP-3/TSTP, E also supports the historic PCL2 format, although it's use is deprecated.

Official Page

https://www.eprover.org

Other relevant information

E is implemented in standard C and widely portable among different UNIX-based operating systems. It's primarily developed and tested on macOS and Linux.

The prover is Free/Open Source software and is licensed under the GNU GPL 2.

E regularly participates in the annual CASC ATP system competition.

Status

Maintained

References

S. Schulz. E – A Brainiac Theorem Prover. Journal of AI Communications, 15(2/3):111–126, 2002.

Stephan Schulz, Simon Cruanes, Petar Vukmirovic: Faster, Higher, Stronger: E 2.3, Proceedings of the 27th Conference on Automated Deduction (CADE'19), Natal, Brazlil. Volume 11716 of LNAI. Springer, 2019. https://doi.org/10.1007/978-3-030-29436-6_29

Petar Vukmirovic, Jamin Christian Blanchette, Stephan Schulz: Extending a High-Performance Prover to Higher-Order Logic, Proceedings of the 29th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), Paris, France, Volume 13994 of LNCS. Springer, 2023. https://doi.org/10.1007/978-3-031-30820-8_10

Tools

The E distribution comes with a number of barely documented tools in various states of maintenance.