Abstract

Suzuki et al. 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. 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 Jacquemard 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.

BibTeX

@inproceedings{CSTS-FSCD16,
  author    = "Christian Sternagel and Thomas Sternagel",
  title     = "Certifying Confluence of Almost Orthogonal CTRSs via
Exact Tree Automata Completion",
  booktitle = "Proceedings of the 1st International Conference on Formal
Structures for Computation and Deduction",
  editor    = "Delia Kesner and Brigitte Pientka",
  series    = "Leibniz International Proceedings in Informatics",
  volume    = 52,
  pages     = "29:1--29:16",
  year      = 2016,
  doi       = "10.4230/LIPIcs.FSCD.2016.29",
}