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 metadatas

Cited literature [31 references]  Display  Hide  Download

https://hal.inria.fr/hal-02296188
Contributor : Petar Vukmirovic <>
Submitted on : Wednesday, September 25, 2019 - 3:41:13 PM
Last modification on : Sunday, January 19, 2020 - 1:10:01 AM

File

sde2_3.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

36

Files downloads

373