Faster, Higher, Stronger: E 2.3: E 2.3

Stephan Schulz, Simon Cruanes, Petar Vukmirovic

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.
Original languageEnglish
Title of host publicationAutomated Deduction - CADE 27
Subtitle of host publication27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings
EditorsPascal Fontaine
PublisherSpringer
Pages495-507
Number of pages13
ISBN (Electronic)9783030294366
ISBN (Print)9783030294359
DOIs
Publication statusPublished - 2019
Event27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil
Duration: 27 Aug 201930 Aug 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11716 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference27th International Conference on Automated Deduction, CADE 2019
CountryBrazil
CityNatal
Period27/08/1930/08/19

Fingerprint

Software architecture
Higher-order Logic
Software Architecture
First-order Logic
Minor
Equality
Logic
Internal
Theorem
Object
Standards

Cite this

Schulz, S., Cruanes, S., & Vukmirovic, P. (2019). Faster, Higher, Stronger: E 2.3: E 2.3. In P. Fontaine (Ed.), Automated Deduction - CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings (pp. 495-507). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI). Springer. https://doi.org/10.1007/978-3-030-29436-6_29
Schulz, Stephan ; Cruanes, Simon ; Vukmirovic, Petar. / Faster, Higher, Stronger: E 2.3 : E 2.3. Automated Deduction - CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. editor / Pascal Fontaine. Springer, 2019. pp. 495-507 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{2554365ae995415ebd4b92c8be8639c2,
title = "Faster, Higher, Stronger: E 2.3: 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.",
author = "Stephan Schulz and Simon Cruanes and Petar Vukmirovic",
year = "2019",
doi = "10.1007/978-3-030-29436-6_29",
language = "English",
isbn = "9783030294359",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "495--507",
editor = "Pascal Fontaine",
booktitle = "Automated Deduction - CADE 27",

}

Schulz, S, Cruanes, S & Vukmirovic, P 2019, Faster, Higher, Stronger: E 2.3: E 2.3. in P Fontaine (ed.), Automated Deduction - CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11716 LNAI, Springer, pp. 495-507, 27th International Conference on Automated Deduction, CADE 2019, Natal, Brazil, 27/08/19. https://doi.org/10.1007/978-3-030-29436-6_29

Faster, Higher, Stronger: E 2.3 : E 2.3. / Schulz, Stephan; Cruanes, Simon; Vukmirovic, Petar.

Automated Deduction - CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. ed. / Pascal Fontaine. Springer, 2019. p. 495-507 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI).

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Faster, Higher, Stronger: E 2.3

T2 - E 2.3

AU - Schulz, Stephan

AU - Cruanes, Simon

AU - Vukmirovic, Petar

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85076976660&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85076976660&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-29436-6_29

DO - 10.1007/978-3-030-29436-6_29

M3 - Conference contribution

SN - 9783030294359

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 495

EP - 507

BT - Automated Deduction - CADE 27

A2 - Fontaine, Pascal

PB - Springer

ER -

Schulz S, Cruanes S, Vukmirovic P. Faster, Higher, Stronger: E 2.3: E 2.3. In Fontaine P, editor, Automated Deduction - CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. Springer. 2019. p. 495-507. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-29436-6_29