Abstract

In this paper we present an overview of infeasibility methods for oriented 3-CTRSs, one of the most popular types of conditional rewriting. In such systems extra variables in conditions and right-hand sides of rewrite rules are allowed. Moreover, satisfiability of the conditions amounts to reachability. As a consequence of the latter, establishing infeasibility is similar to the problem of eliminating arrows in dependency graph approximations, a problem which has been investigated extensively in the literature. The difference is that we deal with CTRSs and the terms we test may share variables. In the sequel we summarize the methods that we have analyzed and adapted for infeasibility. The methods have been implemented in our confluence tool ConCon and experimental data will be presented.

BibTeX

@inproceedings{TSAM-IWC15,
 author    = "Thomas Sternagel and Aart Middeldorp",
 title     = "Infeasible Conditional Critical Pairs",
 booktitle = "Proceedings of the 4th International Workshop on Confluence",
 pages     = "13--17",
 year      = 2015
}