Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
Franziska Rapp and Aart Middeldorp
Proceedings of the 1st International Conference on Formal Structures for
Computation and Deduction (FSCD 2016), Leibniz International Proceedings in
Informatics 52, pp. 36:1 – 36:12, 2016.
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{RM-FSCD16,
author = "Franziska Rapp and Aart Middeldorp",
title = "Automating the First-Order Theory of Rewriting for
Left-Linear Right-Ground Rewrite Systems",
booktitle = "Proceedings of the 1st International Conference on Formal
Structures for Computation and Deduction",
editor = "Delia Kesner and Brigitte Pientka",
series = "Leibniz International Proceedings in Informatics"
volume = 52,
pages = "36:1--36:12",
year = 2016,
doi = "10.4230/LIPIcs.FSCD.2016.36"
}