Abstract
Ordered resolution and superposition are the state-of-the-art proof procedures used in saturation-based theorem proving, for non equational and equational clause sets respectively. In this paper, we present extensions of these calculi that permit one to reason about formulae built from terms with integer exponents (or I-terms), a schematisation language allowing one to denote infinite sequences of iterated terms [8]. We prove that the ordered resolution calculus is still refutationally complete when applied on (non equational) clauses containing I-terms. In the equational case, we prove that the superposition calculus is not complete in the presence of I-terms and we devise a new inference rule, called H-superposition, that restores completeness.
This work has been partly funded by the project ASAP of the French Agence Nationale de la Recherche (ANR-09-BLAN-0407-01).
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.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 3(4), 217–247 (1994)
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson and Voronkov [19], pp. 19–99
Baumgartner, P.: Hyper Tableaux — The Next Generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 60–76. Springer, Heidelberg (1998)
Bensaid, H., Caferra, R., Peltier, N.: Towards systematic analysis of theorem provers search spaces: First steps. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 38–52. Springer, Heidelberg (2007)
Bensaid, H., Caferra, R., Peltier, N.: Dei: A theorem prover for terms with integer exponents. In: Schmidt, R.A. (ed.) Automated Deduction – CADE-22. LNCS, vol. 5663, pp. 146–150. Springer, Heidelberg (2009)
Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic Series, vol. 31. Kluwer Academic Publishers, Dordrecht (2004)
Chen, H., Hsiang, J., Kong, H.-C.: On finite representations of infinite sequences of terms. In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol. 516, pp. 100–114. Springer, Heidelberg (1991)
Comon, H.: On unification of terms with integer exponents. Mathematical Systems Theory 28(1), 67–88 (1995)
Farmer, W.M.: A unification algorithm for second-order monadic terms. Annals of Pure and Applied Logic 39(2), 131–174 (1988)
Hermann, M., Galbavý, R.: Unification of infinite sets of terms schematized by primal grammars. Theor. Comput. Sci. 176(1-2), 111–158 (1997)
Hermant, O.: Resolution is cut-free. Journal of Automated Reasoning 44(3), 245–276 (2010)
Kirchner, H.: Schematization of infinite sets of rewrite rules generated by divergent completion processes. Theoretical Comput. Sci. 67(2-3), 303–332 (1989)
Leitsch, A.: The resolution calculus. In: Texts in Theoretical Computer Science. Springer, Heidelberg (1997)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson and Voronkov [19], pp. 371–443
Peltier, N.: Increasing the capabilities of model building by constraint solving with terms with integer exponents. Journal of Symbolic Computation 24, 59–101 (1997)
Peltier, N.: A General Method for Using Terms Schematizations in Automated Deduction. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 578–593. Springer, Heidelberg (2001)
Robinson, J.A.: Automatic deduction with hyperresolution. Intern. Journal of Computer Math. 1, 227–234 (1965)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12, 23–41 (1965)
Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 2. Elsevier/MIT Press (2001)
Salzer, G.: The unification of infinite sets of terms and its applications. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 409–420. Springer, Heidelberg (1992)
Schulz, S.: System Description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bensaid, H., Caferra, R., Peltier, N. (2010). I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness. In: Autexier, S., et al. Intelligent Computer Mathematics. CICM 2010. Lecture Notes in Computer Science(), vol 6167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14128-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-14128-7_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14127-0
Online ISBN: 978-3-642-14128-7
eBook Packages: Computer ScienceComputer Science (R0)