E 2.3 is a theorem prover for many-sorted first-order logic with equality. We describe the basic logical and software architecture of the system, as well as core features of the implementation. We particularly discuss recently added features and extensions, including the extension to many-sorted logic, optional limited support for higher-order logic, and the integration of SAT techniques via PicoSAT. Minor additions include improved support for TPTP standard features, always-on internal proof objects, and lazy orphan removal. The paper also gives an overview of the performance of the system, and describes ongoing and future work.
CITATION STYLE
Schulz, S., Cruanes, S., & Vukmirović, P. (2019). Faster, higher, stronger: E 2.3. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11716 LNAI, pp. 495–507). Springer. https://doi.org/10.1007/978-3-030-29436-6_29
Mendeley helps you to discover research relevant for your work.