||Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent
Sakai, Masahiko ,
Oyamaguchi, MichioOgawa, Mizuhito
Lecture Notes in Computer Science
126 , 2015-07-25 , Springer
A term is weakly shallow if each defined function symbol occurs either at the root or in the ground subterms, and a term rewriting system is weakly shallow if both sides of a rewrite rule are weakly shallow. This paper proves that non-E-overlapping, weakly-shallow, and non-collapsing term rewriting systems are confluent by extending reduction graph techniques in our previous work [SO10] with towers of expansions.
25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings