Abstract
The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the associated logical system. This equivalence, however, does not extend to rewrite systems directly rewriting atomic propositions.
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
L. Bachmair and N. Dershowitz, Equational Inference, Canonical Proofs, and Proof Orderings. Journal of the ACM 41(2), 1994, pp. 236–276
A. Church and J.B. Rosser, Some properties of conversion. Transactions of the American Mathematical Society, 39, 1936, pp. 472–482.
M. Crabbé. Non-normalisation de ZF. Manuscript, 1974.
G. Dowek, Axioms vs. rewrite rules: from completeness to cut elimination. H. Kirchner and Ch. Ringeissen (Eds.) Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 1794, Springer-Verlag, 2000, pp. 62–72.
G. Dowek, Th. Hardin, and C. Kirchner. Theorem proving modulo. Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, 1998. Journal of Automated Reasoning (to appear).
G. Dowek and B. Werner. Proof normalization modulo. In Types for proofs and programs 98, Lecture Notes in Computer Science 1657, Springer-Verlag, 1999, pp. 62–77.
G. Dowek and B. Werner. An inconsistent theory modulo defined by a confluent and terminating rewrite system. Manuscript, 2000.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.
M.H.A. Newman, On theories with a combinatorial definition of “equivalence”. Annals of Mathematics, 43,2, 1942, pp. 223–243.
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
Dowek, G. (2003). Confluence as a Cut Elimination Property. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_2
Download citation
DOI: https://doi.org/10.1007/3-540-44881-0_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40254-1
Online ISBN: 978-3-540-44881-5
eBook Packages: Springer Book Archive