Journal Article Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent

Sakai, Masahiko  ,  Oyamaguchi, Michio  ,  Ogawa, Mizuhito

9195pp.111 - 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

Number of accesses :  

Other information