Abstract
In many theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the Model Evolution calculus ( \(\mathcal{ME}\)), a first-order version of the propositional DPLL procedure. The new calculus, \(\mathcal{ME}_{\rm E}\), is a proper extension of the \(\mathcal{ME}\) calculus without equality. Like \(\mathcal{ME}\) it maintains an explicit candidate model, which is searched for by DPLL-style splitting. For equational reasoning \(\mathcal{ME}_{\rm E}\) uses an adapted version of the ordered paramodulation inference rule, where equations used for paramodulation are drawn (only) from the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many simplification techniques known from superposition-style theorem proving. Our main result is the correctness of the \(\mathcal{ME}_{\rm E}\) calculus in the presence of very general redundancy elimination criteria.
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
Bachmair, L., Ganzinger, H.: Equational Reasoning in Saturation-Based Theorem Proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. A Basis for Applications, Foundations. Calculi and Refinements, vol. I, pp. 353–398. Kluwer, Dordrecht (1998)
Baumgartner, P.: FDPLL – A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 200–219. Springer, Heidelberg (2000)
Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the Model Evolution Calculus. In: International Journal on Artificial Intelligence Tools, IJAIT (2005) (to appear)
Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 350–364. Springer, Heidelberg (2003)
Baumgartner, P., Tinelli, C.: The Model Evolution Calculus with Equality (2005), http://www.mpi-sb.mpg.de/~baumgart/publications/MEE.pdf
Billon, J.-P.: The Disconnection Method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, 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)
Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 71–84. Springer, Heidelberg (2004)
Ganzinger, H., Korovin, K.: New Directions in Instance-Based Theorem Proving. In: Proc. LICS (2003)
Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 176–190. Springer, Heidelberg (2002)
Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371–443. Elsevier, Amsterdam (2001)
Plaisted, D.A., Zhu, Y.: Ordered Semantic Hyper Linking. Journal of Automated Reasoning 25(3), 167–217 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baumgartner, P., Tinelli, C. (2005). The Model Evolution Calculus with Equality. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_29
Download citation
DOI: https://doi.org/10.1007/11532231_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28005-7
Online ISBN: 978-3-540-31864-4
eBook Packages: Computer ScienceComputer Science (R0)