Abstract
The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful lifting of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL’s optimizations, and so has the potential of leading to much faster implementations.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bachmair, L., Ganzinger, H.: Equational Reasoning in Saturation-Based Theorem Proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. A Basis for Applications, vol. I, ch. 11, Kluwer, Dordrecht (1998)
Baumgartner, P.: Hyper Tableaux—The Next Generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 60–76. Springer, Heidelberg (1998)
Baumgartner, P.: FDPLL—A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831. Springer, Heidelberg (2000)
Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. Fachberichte Informatik 1–2003, Universität Koblenz-Landau (2003)
Bibel, W.: Automated Theorem Proving. Vieweg (1982)
Billon, J.-P.: The Disconnection Method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol. 1071, pp. 110–126. Springer, Heidelberg (1996)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960)
Ganzinger, H., Korovin, K.: New directions in instance-based theorem proving. In: LICS - Logics in Computer Science (2003) (to appear)
Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial Instantiation Methods for Inference in First Order Logic. Journal of Automated Reasoning 28, 371–396 (2002)
Lee, S.-J., Plaisted, D.: Eliminating Duplicates with the Hyper-Linking Strategy. Journal of Automated Reasoning 9, 25–42 (1992)
Letz, R., Mayr, K., Goller, C.: Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning 13 (1994)
Letz, R., Stenz, G.: Proof and Model Generation with Disconnection Tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, p. 142. Springer, Heidelberg (2001)
Plaisted, D.A., Zhu, Y.: Ordered Semantic Hyper Linking. Journal of Automated Reasoning 25(3), 167–217 (2000)
Stenz, G.: DCTP 1.2 - System Abstract. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 335–340. Springer, Heidelberg (2002)
Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, p. 308. Springer, Heidelberg (2002)
Yahya, A., Plaisted, D.A.: Ordered Semantic Hyper-Tableaux. Journal of Automated Reasoning 29(1), 17–57 (2002)
Zhang, H., Stickel, M.E.: An efficient algorithm for unit propagation. In: Proc. of AIMATH 1996 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baumgartner, P., Tinelli, C. (2003). The Model Evolution Calculus. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive