Advertisement

Simplification A General Constraint Propagation Technique for Propositional and Modal Tableaux

  • Fabio Massacci
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    P. Baumgartner, U. Furbach, and I. Niemelä. Hyper tableaux. In Proc. JELIA-96, LNAI 1126, pages 1–17. Springer-Verlag, 1996.Google Scholar
  3. 3.
    B. Beckert. Semantic tableaux with equality. Journal of Logic and Computation, 7(1):38–58, 1997.CrossRefMathSciNetGoogle Scholar
  4. 4.
    B. Beckert and J. Possega. leanTAP: Lean tableau-based deduction. JAR, 15(3):339–358, 1995.zbMATHCrossRefGoogle Scholar
  5. 5.
    L. J. Claesen, editor. Formal VLSI Correctness Verification: VLSI Design Methods, volume II. Elsevier Science, 1990.Google Scholar
  6. 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
  7. 7.
    M. D’Agostino and M. Mondadori. The taming of the cut. JLC, 4(3):285–319, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    M. Davis, G. Longemann, and D. Loveland. A machine program for theorem-proving. Comm. of the ACM, 5(7):394–397, 1962.zbMATHCrossRefGoogle Scholar
  9. 9.
    M. Davis and H. Putnam. A computing procedure for quantificational theory. JACM, 7(3):201–215, 1960.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.Google Scholar
  11. 11.
    M. Fitting. First Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.Google Scholar
  12. 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. 13.
    M. Gordon and T. Melham. Introduction to HOL. Cambridge University Press, 1993.Google Scholar
  14. 14.
    J. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. AIJ, 54:319–379, 1992.zbMATHMathSciNetGoogle Scholar
  15. 15.
    J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162–170, 1995.CrossRefMathSciNetGoogle Scholar
  16. 16.
    U. Hustadt and R. Schmidt. On evaluating decision procedure for modal logic. In Proc. of IJCAI-97, 1997.Google Scholar
  17. 17.
    R. Letz, K. Mayr, and C. Goller. Controlled integration of the cut rule into connection tableau calculi. JAR, 13(3):297–337, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 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. 19.
    D. McAllester, Truth maintenance. In Proc. of AAAI-90, pages 1109–1116, 1990.Google Scholar
  20. 20.
    N. V. Murray and E. Rosenthal. On the computational intractability of analytic tableau methods. Bulletin of the IGPL, 2(2):205–228, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    F. Oppacher and E. Suen. HARP: a tableau-based theorem prover. JAR, 4:69–100, 1988.MathSciNetGoogle Scholar
  22. 22.
    L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.zbMATHGoogle Scholar
  23. 23.
    D. Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960.zbMATHMathSciNetCrossRefGoogle Scholar
  24. 24.
    W. Quine. Methods of Logic. Harvard Univ. Press, iv ed., 1983.Google Scholar
  25. 25.
    J. A. Robinson. A machine oriented logic based on the resolution principle. JACM, 12(1):23–41, 1965.zbMATHCrossRefGoogle Scholar
  26. 26.
    J. Rushby. Automated deduction and formal methods. In Proc. of CAV-96, LNCS 1102, pages 169–183. Springer-Verlag, 1996.Google Scholar
  27. 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. 28.
    R. M. Smullyan. First Order Logic. Springer-Verlag, 1968. Republished by Dover, 1995.Google Scholar
  29. 29.
    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.CrossRefGoogle Scholar
  30. 30.
    A. Urquhart. The complexity of propositional proofs. Bull. of Symbolic Logic, 1(4):425–467, Dec 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  31. 31.
    A. Voronkov. The anatomy of vampire (implementing bottom-up procedures with code trees). JAR, 15(2):237–265, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  32. 32.
    K. Wallace and G. Wrightson. Regressive merging in model elimination tableau-based theorem provers. Bull. of the IGPL, 3(6):921–937, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  33. 33.
    H. Zhang and M. E. Stickel. An efficient algorithm for unit-propagation. In Proc. of AI-MATH-96, 1996Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Fabio Massacci
    • 1
  1. 1.Dipartimento di Informatica e SistemisticaUniversità di Roma “La Sapienza”RomaItaly

Personalised recommendations