Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
Logic in Computer Science
2016-09-13 v1
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\'ia-S\'aenz.
Cite
@article{arxiv.1609.03341,
title = {Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs},
author = {Thomas Sternagel and Christian Sternagel},
journal= {arXiv preprint arXiv:1609.03341},
year = {2016}
}
Comments
IWC 2016