Skip to Main content Skip to Navigation
Conference papers

Faster, Higher, Stronger: E 2.3

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Petar Vukmirovic Connect in order to contact the contributor
Submitted on : Wednesday, September 25, 2019 - 3:41:13 PM
Last modification on : Sunday, January 19, 2020 - 1:10:01 AM
Long-term archiving on: : Sunday, February 9, 2020 - 10:09:53 PM


Files produced by the author(s)



Simon Cruanes, Stephan Schulz, Petar Vukmirović. Faster, Higher, Stronger: E 2.3. TACAS 2019, Apr 2019, Prague, Czech Republic. pp.495-507, ⟨10.1007/978-3-030-29436-6_29⟩. ⟨hal-02296188⟩



Les métriques sont temporairement indisponibles