\input zb-basic
\input zb-ioport
\iteman{io-port 06027888}
\itemau{Aoto, Takahito}
\itemti{Automated confluence proof by decreasing diagrams based on rule-labelling.}
\itemso{Lynch, Christopher (ed.), Proceedings of the 21st international conference on rewriting techniques and applications (RTA 2010), July 11--13, 2010, Edinburgh, Scottland, UK. Wadern: Schloss Dagstuhl -- Leibniz Zentrum f\"ur Informatik (ISBN 978-3-939897-18-7). LIPICS -- Leibniz International Proceedings in Informatics 6, 7-16, electronic only (2010).}
\itemab
Summary: Decreasing diagrams technique [{\it V. van Oostrom}, Theor. Comput. Sci. 126, No. 2, 259--280 (1994; Zbl 0803.68058)] is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams technique to prove confluence of rewrite systems, rule-labelling heuristic has been proposed by van Oostrom. We show how constraints for ensuring confluence of term rewriting systems constructed based on the rule-labelling heuristic are encoded as linear arithmetic constraints suitable for solving the satisfiability of them by external SMT solvers. We point out an additional constraint omitted in [{\it V. van Oostrom}, Lect. Notes Comput. Sci. 5117, 306--320 (2008; Zbl 1146.68044)] that is needed to guarantee the soundness of confluence proofs based on the rule-labelling heuristic extended to deal with non-right-linear rules. We also present several extensions of the rule-labelling heuristic by which the applicability of the technique is enlarged.
\itemrv{~}
\itemcc{}
\itemut{confluence; decreasing diagrams; automation; term rewriting systems}
\itemli{doi:10.4230/LIPIcs.RTA.2010.7 http://subs.emis.de/LIPIcs/frontdoor\_0da0.html}
\end