Automating the First-Order Theory of Left-Linear Right-Ground Term Rewrite Systems
Franziska Rapp and Aart MiddeldorpProceedings 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
@inproceedings{FRAM-FSCD16,
author = "Franziska Rapp and Aart Middeldorp",
title = "Automating the First-Order Theory of Left-Linear
Right-Ground Term 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"
}