2026-07-23T12:53:56Z https://drops.dagstuhl.de/oai

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

Non-Omega-Overlapping TRSs are UN Kahrs, Stefan Smith, Connor consistency omega-substitutions uniqueness of normal forms This paper solves problem #79 of RTA's list of open problems --- in the positive. If the rules of a TRS do not overlap w.r.t. substitutions of infinite terms then the TRS has unique normal forms. We solve the problem by reducing the problem to one of consistency for "similar" constructor term rewriting systems. For this we introduce a new proof technique. We define a relation ⇓ that is consistent by construction, and which --- if transitive --- would coincide with the rewrite system's equivalence relation =R. We then prove the transitivity of ⇓ by coalgebraic reasoning. Any concrete proof for instances of this relation only refers to terms of some finite coalgebra, and we then construct an equivalence relation on that coalgebra which coincides with ⇓. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefan Kahrs and Connor Smith 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.22 urn:nbn:de:0030-drops-59968 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.22 eng https://creativecommons.org/licenses/by/3.0/legalcode