Abstract
An extension of the superposition-based E-prover [8] is described. The extension allows terms with integer exponents [3] in the input language. Obviously, this possibility increases the capabilities of the E-prover particularly for preventing non-termination.
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
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)
Chen, H., Hsiang, J., Kong, H.: 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 System Theory 28, 67–88 (1995)
Hermann, M., Galbavý, R.: Unification of Infinite Sets of Terms schematized by Primal Grammars. Theoretical Computer Science 176(1-2), 111–158 (1997)
Loechner, V.: Polylib: A library for manipulating parametrized polyhedra. Tech. rep., ICPS, Universite Louis Pasteur de Strasbourg (1999)
Peltier, N.: A General Method for Using Terms Schematizations in Automated Deduction. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 578–593. Springer, Heidelberg (2001)
Salzer, G.: The unification of infinite sets of terms and its applications. In: Voronkov, A. (ed.) LPAR 1992. LNCS (LNAI), vol. 624, pp. 409–429. 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
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bensaid, H., Caferra, R., Peltier, N. (2009). Dei: A Theorem Prover for Terms with Integer Exponents. In: Schmidt, R.A. (eds) Automated Deduction – CADE-22. CADE 2009. Lecture Notes in Computer Science(), vol 5663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02959-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-02959-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02958-5
Online ISBN: 978-3-642-02959-2
eBook Packages: Computer ScienceComputer Science (R0)