2026-07-22T04:53:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5987 2024-03-06T10:37:27Z ddc:004 open_access

Ground Confluence Prover based on Rewriting Induction Aoto, Takahito Toyama, Yoshihito Ground Confluence Rewriting Induction Non-Orientable Equations Term Rewriting Systems 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 on confluence and not ground confluence. In fact, little interest has been paid to developing tools for proving ground confluence automatically. We report an implementation of a ground confluence prover based on rewriting induction, which is a method originally developed for proving inductive theorems. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Takahito Aoto and Yoshihito Toyama 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.33 urn:nbn:de:0030-drops-59873 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.33 eng https://creativecommons.org/licenses/by/3.0/legalcode