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.
|Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998
|5/05/98 → 8/05/98