zbMATH — the first resource for mathematics

Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. (English) Zbl 1388.68155
Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 29, 16 p. (2016).
Summary: T. Suzuki et al. [“Level-confluence of conditional rewrite systems with extra variables in right-hand sides”, Lect. Notes Comput. Sci. 914, 179–193 (1995; doi:10.1007/3-540-59200-8_56); RIMS Kokyuroku 918, 1–15 (1995; Zbl 0939.68679)] showed that properly oriented, right-stable, orthogonal, and oriented conditional term rewrite systems with extra variables in right-hand sides are confluent. We present our Isabelle/HOL formalization of this result, including two generalizations. On the one hand, we relax proper orientedness and orthogonality to extended proper orientedness and almost orthogonality modulo infeasibility, as suggested by Suzuki et al. [loc. cit.]. On the other hand, we further loosen the requirements of the latter, enabling more powerful methods for proving infeasibility of conditional critical pairs. Furthermore, we formalized a construction by F. Jacquemard [“Decidable approximations of term rewriting systems”, Lect. Notes Comput. Sci. 1103, 362–376 (1996; doi:10.1007/3-540-61464-8_65)] that employs exact tree automata completion for non-reachability analysis and apply it to certify infeasibility of conditional critical pairs. Combining these two results and extending the conditional confluence checker ConCon accordingly, we are able to automatically prove and certify confluence of an important class of conditional term rewrite systems.
For the entire collection see [Zbl 1351.68020].

68Q42 Grammars and rewriting systems
68Q45 Formal languages and automata
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
ConCon; Isabelle/HOL
Full Text: DOI