Abstract
Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may require in particular to prove cut elimination for an extended notion of proof that combines deductions and computations. This suggests new interactions between automated theorem proving and proof theory.
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
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. In: Rapport de Recherche INRIA 3400 (1998)
Dowek, G., Hardin, T., Kirchner, C.: HOL-lambda-sigma: an intentional first- order expression of higher-order logic. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 317–331. Springer, Heidelberg (1999)
Dowek, G., Werner, B.: Proof normalization modulo. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 62–77. Springer, Heidelberg (1999); Rapport de Recherche 3542, INRIA (1998)
Fay, M.J.: First-order unification in an equational theory. In: Fourth Workshop on Automated Deduction, pp. 161–167 (1979)
Gallier, J.: Logic in computer science. Harper and Row, New York (1986)
Girard, J.Y., Lafont, Y., Taylor, P.: Types and proofs. Cambridge University Press, Cambridge (1989)
Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)
Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. Journal of the ACM 38(3), 559–587 (1991)
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Peterson, G.: A Technique for establishing completeness results in theorem proving with equality. Siam J. Comput. 12(1), 82–100 (1983)
Plotkin, G.: Building-in equational theories. Machine Intelligence 7, 73–90 (1972)
Robinson, G.A., Wos, L.: Paramodulation and theorem proving in first-order theories with equality. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 135–150. American Elsevier, Amsterdam (1969)
Stickel, M.: Automated deduction by theory resolution. Journal of Automated Reasoning 4(1), 285–289 (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dowek, G. (2000). Axioms vs. Rewrite Rules: From Completeness to Cut Elimination. In: Kirchner, H., Ringeissen, C. (eds) Frontiers of Combining Systems. FroCoS 2000. Lecture Notes in Computer Science(), vol 1794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720084_5
Download citation
DOI: https://doi.org/10.1007/10720084_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67281-4
Online ISBN: 978-3-540-46421-1
eBook Packages: Springer Book Archive