Takahito Aoto

Ground Confluence Prover based on Rewriting Induction

2016 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Recently, interests in proving confluence of term rewriting systems automatically has grown, and confluence provers have been developed. But they mainly focus …