Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Rapp, Franziska; Middeldorp, Aart https://www.dagstuhl.de/lipics License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-60018
URL:

;

Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems

pdf-format:


Abstract

The first-order theory of rewriting is decidable for finite left-linear right-ground rewrite systems. We present a new tool that implements the decision procedure for this theory. It is based on tree automata techniques. The tool offers the possibility to synthesize rewrite systems that satisfy properties that are expressible in the first-order theory of rewriting.

BibTeX - Entry

@InProceedings{rapp_et_al:LIPIcs:2016:6001,
  author =	{Franziska Rapp and Aart Middeldorp},
  title =	{{Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{36:1--36:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6001},
  URN =		{urn:nbn:de:0030-drops-60018},
  doi =		{10.4230/LIPIcs.FSCD.2016.36},
  annote =	{Keywords: first-order theory, ground rewrite systems, automation, synthesis}
}

Keywords: first-order theory, ground rewrite systems, automation, synthesis
Seminar: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue date: 2016
Date of publication: 17.06.2016


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI