Paper Info
Title
Preprocessing techniques for first-order clausification.
Abstract
It is well known that preprocessing is crucial for efficient reasoning on large industrial problems. Although preprocessing is well developed for propositional logic, it is much less investigated for first-order logic. In this paper we introduce several preprocessing techniques for simplifying first-order formulas aimed at improving clausification. These include definition inlining and merging, simplifications based on a new data structure, quantified AIG, and its combination with BDDs. We implemented our preprocessing methods and evaluated them over encodings of industrial hardware verification problems into the effectively propositional (EPR) fragment of first-order logic and over standard first-order (TPTP) and SMT (SMT-LIB) benchmarks. We also investigated preprocessing methods that help obtain EPR-resulting clausification in cases where standard clausification would lead outside the EPR fragment. We demonstrate that our methods enable one to considerably reduce the number of clauses obtained after clausification and by that help speedup first-order reasoning.
Year
Venue
Keywords
2012
FMCAD
binary decision diagrams,computability,data structures,formal logic,formal verification,inference mechanisms,BDD,EPR,EPR fragmentation,SMT,TPTP,and-inverter graphs,data structure,effectively propositional fragment,first-order clausification,first-order formulas,first-order logic,first-order reasoning,industrial hardware verification problems,preprocessing techniques,propositional logic,quantified AIG
Field
DocType
Citations 
Data structure,Autoepistemic logic,Computer science,Propositional calculus,Algorithm,Zeroth-order logic,Theoretical computer science,Computability,Propositional variable,Speedup,Formal verification
Conference
4
PageRank 
References 
Authors
0.41
0
4
Name
Order
Citations
PageRank
Kryštof Hoder1584.02
Zurab Khasidashvili230725.40
Konstantin Korovin328820.64
Andrei Voronkov42670225.46