TY - GEN
T1 - Simplification
T2 - International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998
AU - Massacci, F.
PY - 1998
Y1 - 1998
N2 - Tableau and sequent calculi are the basis for most popular interactive theorem provers for formal verification. Yet, when it comes to automatic proof search, tableaux are often slower than Davis-Putnam, SAT procedures or other techniques. This is partly due to the absence of a bivalence principle (viz. the cut-rule) but there is another source of ineficiency: the lack of constraint propagation mechanisms. This paper proposes an innovation in this direction: the rule of simplification, which plays for tableaux the role of subsumption for resolution and of unit for the Davis-Putnam procedure. The simplicity and generality of simplification make possible its extension in a uniform way from propositional logic to a wide range of modal logics. This technique gives an unifying view of a number of tableaux-like calculi such as DPLL, KE, HARP, hyper-tableaux, BCP, KSAT. We show its practical impact with experimental results for random 3-SAT and the industrial IFIP benchmarks for hardware verification. © Springer-Verlag Berlin Heidelberg 1998.
AB - Tableau and sequent calculi are the basis for most popular interactive theorem provers for formal verification. Yet, when it comes to automatic proof search, tableaux are often slower than Davis-Putnam, SAT procedures or other techniques. This is partly due to the absence of a bivalence principle (viz. the cut-rule) but there is another source of ineficiency: the lack of constraint propagation mechanisms. This paper proposes an innovation in this direction: the rule of simplification, which plays for tableaux the role of subsumption for resolution and of unit for the Davis-Putnam procedure. The simplicity and generality of simplification make possible its extension in a uniform way from propositional logic to a wide range of modal logics. This technique gives an unifying view of a number of tableaux-like calculi such as DPLL, KE, HARP, hyper-tableaux, BCP, KSAT. We show its practical impact with experimental results for random 3-SAT and the industrial IFIP benchmarks for hardware verification. © Springer-Verlag Berlin Heidelberg 1998.
U2 - 10.1007/3-540-69778-0_24
DO - 10.1007/3-540-69778-0_24
M3 - Conference contribution
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 217
EP - 231
BT - Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings
PB - Springer Verlag
Y2 - 5 May 1998 through 8 May 1998
ER -