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 :
Book sections
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 : Friday, September 27, 2019 - 1:17:58 AM

File

sde2_3.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Stephan Schulz, Simon Cruanes, Petar Vukmirovic. Faster, Higher, Stronger: E 2.3. CADE 2019, 11716, pp.495-507, 2019, LNAI, ⟨10.1007/978-3-030-29436-6_29⟩. ⟨hal-02296188⟩

Share

Metrics

Record views

9

Files downloads

176