Predicate Elimination for Preprocessing in First-Order Theorem Proving

Zurab Khasidashvili; Konstantin Korovin

doi:10.1007/978-3-319-40970-2_22

Predicate Elimination for Preprocessing in First-Order Theorem Proving

Zurab Khasidashvili, Konstantin Korovin

Intel Corporation

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

Preprocessing plays a major role in efficient propositional reasoning
but has been less studied in first-order theorem proving.
In this paper we propose a predicate elimination procedure which can be used as a preprocessing step in first-order theorem proving and is also applicable for simplifying quantified formulas in a general framework of satisfiability modulo theories (SMT). We describe how this procedure is implemented in a first-order theorem prover iProver and show that many problems in the TPTP library can be simplified using this procedure. We also evaluated our preprocessing on the HWMCC'15 hardware verification benchmarks and show that more than 50\% of predicates can be eliminated without increasing the problem sizes.

Original language	English
Title of host publication	Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
Editors	Nadia Creignou, Daniel Le Berre
Place of Publication	Springer
Publisher	Springer Nature
Pages	361--372
ISBN (Print)	9783319409702
DOIs	https://doi.org/10.1007/978-3-319-40970-2_22
Publication status	Published - 11 Jun 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9710
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

Automated theorem proving

Access to Document

10.1007/978-3-319-40970-2_22

Cite this

Khasidashvili, Z., & Korovin, K. (2016). Predicate Elimination for Preprocessing in First-Order Theorem Proving. In N. Creignou, & D. Le Berre (Eds.), Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (pp. 361--372). (Lecture Notes in Computer Science; Vol. 9710). Springer Nature. https://doi.org/10.1007/978-3-319-40970-2_22

Khasidashvili, Zurab ; Korovin, Konstantin. / Predicate Elimination for Preprocessing in First-Order Theorem Proving. Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . editor / Nadia Creignou ; Daniel Le Berre. Springer : Springer Nature, 2016. pp. 361--372 (Lecture Notes in Computer Science).

@inproceedings{3be8aaeb3a3f4ce7ac5c97a795db5f2d,

title = "Predicate Elimination for Preprocessing in First-Order Theorem Proving",

abstract = "Preprocessing plays a major role in efficient propositional reasoning but has been less studied in first-order theorem proving. In this paper we propose a predicate elimination procedure which can be used as a preprocessing step in first-order theorem proving and is also applicable for simplifying quantified formulas in a general framework of satisfiability modulo theories (SMT). We describe how this procedure is implemented in a first-order theorem prover iProver and show that many problems in the TPTP library can be simplified using this procedure. We also evaluated our preprocessing on the HWMCC'15 hardware verification benchmarks and show that more than 50\% of predicates can be eliminated without increasing the problem sizes.",

keywords = "Automated theorem proving",

author = "Zurab Khasidashvili and Konstantin Korovin",

year = "2016",

month = jun,

day = "11",

doi = "10.1007/978-3-319-40970-2_22",

language = "English",

isbn = "9783319409702",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "361----372",

editor = "Nadia Creignou and {Le Berre}, Daniel",

booktitle = "Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings",

address = "United States",

}

Khasidashvili, Z & Korovin, K 2016, Predicate Elimination for Preprocessing in First-Order Theorem Proving. in N Creignou & D Le Berre (eds), Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . Lecture Notes in Computer Science, vol. 9710, Springer Nature, Springer, pp. 361--372. https://doi.org/10.1007/978-3-319-40970-2_22

Predicate Elimination for Preprocessing in First-Order Theorem Proving. / Khasidashvili, Zurab; Korovin, Konstantin.
Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . ed. / Nadia Creignou; Daniel Le Berre. Springer: Springer Nature, 2016. p. 361--372 (Lecture Notes in Computer Science; Vol. 9710).

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Predicate Elimination for Preprocessing in First-Order Theorem Proving

AU - Khasidashvili, Zurab

AU - Korovin, Konstantin

PY - 2016/6/11

Y1 - 2016/6/11

N2 - Preprocessing plays a major role in efficient propositional reasoning but has been less studied in first-order theorem proving. In this paper we propose a predicate elimination procedure which can be used as a preprocessing step in first-order theorem proving and is also applicable for simplifying quantified formulas in a general framework of satisfiability modulo theories (SMT). We describe how this procedure is implemented in a first-order theorem prover iProver and show that many problems in the TPTP library can be simplified using this procedure. We also evaluated our preprocessing on the HWMCC'15 hardware verification benchmarks and show that more than 50\% of predicates can be eliminated without increasing the problem sizes.

AB - Preprocessing plays a major role in efficient propositional reasoning but has been less studied in first-order theorem proving. In this paper we propose a predicate elimination procedure which can be used as a preprocessing step in first-order theorem proving and is also applicable for simplifying quantified formulas in a general framework of satisfiability modulo theories (SMT). We describe how this procedure is implemented in a first-order theorem prover iProver and show that many problems in the TPTP library can be simplified using this procedure. We also evaluated our preprocessing on the HWMCC'15 hardware verification benchmarks and show that more than 50\% of predicates can be eliminated without increasing the problem sizes.

KW - Automated theorem proving

U2 - 10.1007/978-3-319-40970-2_22

DO - 10.1007/978-3-319-40970-2_22

M3 - Conference contribution

SN - 9783319409702

T3 - Lecture Notes in Computer Science

SP - 361

EP - 372

BT - Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings

A2 - Creignou, Nadia

A2 - Le Berre, Daniel

PB - Springer Nature

CY - Springer

ER -

Khasidashvili Z, Korovin K. Predicate Elimination for Preprocessing in First-Order Theorem Proving. In Creignou N, Le Berre D, editors, Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . Springer: Springer Nature. 2016. p. 361--372. (Lecture Notes in Computer Science). Epub 2016 Jun 11. doi: 10.1007/978-3-319-40970-2_22

Predicate Elimination for Preprocessing in First-Order Theorem Proving

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this