Simplification A General Constraint Propagation Technique for Propositional and Modal Tableaux
- 235 Downloads
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 inefficiency: 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.
Unable to display preview. Download preview PDF.
- 1.M. Baaz and C. Fermüller. Non-elementary speedups between different versions of tableaux. In Proc. of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pages 217–230. Springer-Verlag, 1995.Google Scholar
- 2.P. Baumgartner, U. Furbach, and I. Niemelä. Hyper tableaux. In Proc. JELIA-96, LNAI 1126, pages 1–17. Springer-Verlag, 1996.Google Scholar
- 5.L. J. Claesen, editor. Formal VLSI Correctness Verification: VLSI Design Methods, volume II. Elsevier Science, 1990.Google Scholar
- 6.J. Crawford and L. Auton. Experimental results on the crossover point in satisfiability problems. In Proc. of the 11th National Conference on Artificial Intelligence (AAAI-93), pages 21–27. AAAI Press/The MIT Press, 1993.Google Scholar
- 10.M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.Google Scholar
- 11.M. Fitting. First Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.Google Scholar
- 12.F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. CADE-96, LNAI 1104, pages 583–597. Springer-Verlag, 1996.Google Scholar
- 13.M. Gordon and T. Melham. Introduction to HOL. Cambridge University Press, 1993.Google Scholar
- 16.U. Hustadt and R. Schmidt. On evaluating decision procedure for modal logic. In Proc. of IJCAI-97, 1997.Google Scholar
- 18.F. Massacci. Simplification with renaming: A general proof technique for tableau and sequent-based provers. Tech. Rep. 424, Computer Laboratory, Univ. of Cambridge (UK), 1997.Google Scholar
- 19.D. McAllester, Truth maintenance. In Proc. of AAAI-90, pages 1109–1116, 1990.Google Scholar
- 24.W. Quine. Methods of Logic. Harvard Univ. Press, iv ed., 1983.Google Scholar
- 26.J. Rushby. Automated deduction and formal methods. In Proc. of CAV-96, LNCS 1102, pages 169–183. Springer-Verlag, 1996.Google Scholar
- 27.B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proc. of AAAI-92, 1992.Google Scholar
- 28.R. M. Smullyan. First Order Logic. Springer-Verlag, 1968. Republished by Dover, 1995.Google Scholar
- 33.H. Zhang and M. E. Stickel. An efficient algorithm for unit-propagation. In Proc. of AI-MATH-96, 1996Google Scholar