Abstract
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.
An comprehensive review of the various results on simplification, including the first order case can be found in [18].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
P. Baumgartner, U. Furbach, and I. Niemelä. Hyper tableaux. In Proc. JELIA-96, LNAI 1126, pages 1–17. Springer-Verlag, 1996.
B. Beckert. Semantic tableaux with equality. Journal of Logic and Computation, 7(1):38–58, 1997.
B. Beckert and J. Possega. leanTAP: Lean tableau-based deduction. JAR, 15(3):339–358, 1995.
L. J. Claesen, editor. Formal VLSI Correctness Verification: VLSI Design Methods, volume II. Elsevier Science, 1990.
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.
M. D’Agostino and M. Mondadori. The taming of the cut. JLC, 4(3):285–319, 1994.
M. Davis, G. Longemann, and D. Loveland. A machine program for theorem-proving. Comm. of the ACM, 5(7):394–397, 1962.
M. Davis and H. Putnam. A computing procedure for quantificational theory. JACM, 7(3):201–215, 1960.
M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.
M. Fitting. First Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.
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.
M. Gordon and T. Melham. Introduction to HOL. Cambridge University Press, 1993.
J. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. AIJ, 54:319–379, 1992.
J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162–170, 1995.
U. Hustadt and R. Schmidt. On evaluating decision procedure for modal logic. In Proc. of IJCAI-97, 1997.
R. Letz, K. Mayr, and C. Goller. Controlled integration of the cut rule into connection tableau calculi. JAR, 13(3):297–337, 1994.
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.
D. McAllester, Truth maintenance. In Proc. of AAAI-90, pages 1109–1116, 1990.
N. V. Murray and E. Rosenthal. On the computational intractability of analytic tableau methods. Bulletin of the IGPL, 2(2):205–228, 1994.
F. Oppacher and E. Suen. HARP: a tableau-based theorem prover. JAR, 4:69–100, 1988.
L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
D. Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960.
W. Quine. Methods of Logic. Harvard Univ. Press, iv ed., 1983.
J. A. Robinson. A machine oriented logic based on the resolution principle. JACM, 12(1):23–41, 1965.
J. Rushby. Automated deduction and formal methods. In Proc. of CAV-96, LNCS 1102, pages 169–183. Springer-Verlag, 1996.
B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proc. of AAAI-92, 1992.
R. M. Smullyan. First Order Logic. Springer-Verlag, 1968. Republished by Dover, 1995.
T. Uribe and M. E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. In Proc. of the 1st Internat. Conf. on Constraints in Computational Logics, LNCS 845, Springer-Verlag, 1994.
A. Urquhart. The complexity of propositional proofs. Bull. of Symbolic Logic, 1(4):425–467, Dec 1995.
A. Voronkov. The anatomy of vampire (implementing bottom-up procedures with code trees). JAR, 15(2):237–265, 1995.
K. Wallace and G. Wrightson. Regressive merging in model elimination tableau-based theorem provers. Bull. of the IGPL, 3(6):921–937, 1995.
H. Zhang and M. E. Stickel. An efficient algorithm for unit-propagation. In Proc. of AI-MATH-96, 1996
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Massacci, F. (1998). Simplification A General Constraint Propagation Technique for Propositional and Modal Tableaux. In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_24
Download citation
DOI: https://doi.org/10.1007/3-540-69778-0_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64406-4
Online ISBN: 978-3-540-69778-7
eBook Packages: Springer Book Archive