1 Search Results for "Smith, Connor"


Document
Non-Omega-Overlapping TRSs are UN

Authors: Stefan Kahrs and Connor Smith

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)


Abstract
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 ⇓.

Cite as

Stefan Kahrs and Connor Smith. Non-Omega-Overlapping TRSs are UN. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kahrs_et_al:LIPIcs.FSCD.2016.22,
  author =	{Kahrs, Stefan and Smith, Connor},
  title =	{{Non-Omega-Overlapping TRSs are UN}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.22},
  URN =		{urn:nbn:de:0030-drops-59968},
  doi =		{10.4230/LIPIcs.FSCD.2016.22},
  annote =	{Keywords: consistency, omega-substitutions, uniqueness of normal forms}
}
  • Refine by Author
  • 1 Kahrs, Stefan
  • 1 Smith, Connor

  • Refine by Classification

  • Refine by Keyword
  • 1 consistency
  • 1 omega-substitutions
  • 1 uniqueness of normal forms

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail