Smith, Connor Lane, Kahrs, Stefan (2016) Non-omega-overlapping TRSs are UN. In: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). 2016 Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics , 52. 22:1-22:17. Schloss Dagstuhl: Leibniz-Zentrum für Informatik, Porto, Portugal ISBN 978-3-95977-010-1. (doi:10.4230/LIPIcs.FSCD.2016.22)

PDF - Author's Accepted Manuscript

 Preview
Official URL
http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.22

## Abstract

This paper solves problem #79 of RTA’s list of open problems [14] — in the positive. If the

normal forms. We solve the problem by reducing the problem to one of consistency for “similar”

relation ⇓ that is consistent by construction, and which — if transitive — would coincide with

We then prove the transitivity of ⇓ by coalgebraic reasoning. Any concrete proof for instances

relation on that coalgebra which coincides with ⇓.

Item Type: Conference or workshop item (Paper) 10.4230/LIPIcs.FSCD.2016.22 term rewriting, functional programming, consistency Q ScienceQ Science > QA Mathematics (inc Computing science)Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics Faculties > Sciences > School of Computing > Programming Languages and Systems Group Stefan Kahrs 10 May 2016 11:06 UTC 30 Jan 2020 16:19 UTC https://kar.kent.ac.uk/id/eprint/55349 (The current URI for this page, for reference purposes)