Abstract
This paper describes a new confluence tool for term rewrite systems. Due to its modular design, the few techniques implemented so far can be combined flexibly. Methods developed for termination analysis are adapted to prove and disprove confluence. Preliminary experimental results show the potential of our tool.
This research is supported by FWF (Austrian Science Fund) project P22467.
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.
Similar content being viewed by others
References
Aoto, T.: Automated confluence proof by decreasing diagrams based on rule-labelling. In: Lynch, C. (ed.) RTA 2010. LIPIcs, vol. 6, pp. 7–16. Schloss Dagstuhl, Dagstuhl (2010)
Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 93–102. Springer, Heidelberg (2009)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schauß, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 21–30. Schloss Dagstuhl, Dagstuhl (2011)
Felgenhauer, B., Zankl, H., Middeldorp, A.: Proving confluence with layer systems (2011); submitted for publication
Genet, T.: Decidable approximations of sets of descendants and sets of normal forms. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 151–165. Springer, Heidelberg (1998)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. JACM 27(4), 797–821 (1980)
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Korp, M., Middeldorp, A.: Match-bounds revisited. I&C 207(11), 1259–1283 (2009)
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)
van Oostrom, V.: Confluence by decreasing diagrams. TCS 126(2), 259–280 (1994)
van Oostrom, V.: Developing developments. TCS 175(1), 159–181 (1997)
van Oostrom, V.: Confluence by decreasing diagrams. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 306–320. Springer, Heidelberg (2008)
Terese: Term Rewriting Systems, vol. 55. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)
Tiwari, A.: Deciding confluence of certain term rewriting systems in polynomial time. In: LICS 2002, pp. 447–457 (2002)
Zankl, H., Felgenhauer, B., Middeldorp, A.: Labelings for decreasing diagrams. In: Schmidt-Schauß, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 377–392. Schloss Dagstuhl, Dagstuhl (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zankl, H., Felgenhauer, B., Middeldorp, A. (2011). CSI – A Confluence Tool. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-22438-6_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22437-9
Online ISBN: 978-3-642-22438-6
eBook Packages: Computer ScienceComputer Science (R0)