Paper Info
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.
Year
DOI
Venue
2016
10.1007/978-3-319-40970-2_22
Lecture Notes in Computer Science
Field
DocType
Volume
Discrete mathematics,Computer science,First order,Automated theorem proving,Automated proof checking,Preprocessor,Unit propagation,Predicate (grammar),Compactness theorem,Satisfiability modulo theories
Conference
9710
ISSN
Citations 
PageRank 
0302-9743
2
0.38
References 
Authors
21
2
Name
Order
Citations
PageRank
Zurab Khasidashvili130725.40
Konstantin Korovin228820.64