Abstract

We present an Isabelle/HOL formalization of a characterization of confluence for
quasi-reductive strongly deterministic conditional term rewrite systems, due to
Avenhaus and Lorı́a-Sáenz.

BibTeX

@inproceedings{TSCS-IWC16,
 author    = "Thomas Sternagel and Christian Sternagel",
 title     = "Formalized Confluence of Quasi-Decreasing, Strongly Deterministic
              Conditional TRSs",
 booktitle = "Proceedings of the 5th International Workshop on Confluence",
 pages     = "60--64",
 year      = 2016
}