LIPIcs.FSCD.2016.36.pdf
- Filesize: 0.49 MB
- 12 pages
Document
Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
Authors
-
Part of:
Volume:
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2016-06-17
Cite As Get BibTex
Franziska Rapp and Aart Middeldorp. Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 36:1-36:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.36
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.
Subject Classification
Keywords
- first-order theory
- ground rewrite systems
- automation
- synthesis
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
- H. Comon. Sequentiality, monadic second-order logic and tree automata. I&C, 157(1-2):25-51, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2838.
- H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications, 2007. URL: http://www.grappa.univ-lille3.fr/tata.
- M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In Proc. 5th LICS, pages 242-248, 1990. URL: http://dx.doi.org/10.1109/LICS.1990.113750.
-
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable (extended version). Technical Report I.T. 197, LIFL, 1990.
- E. Jiresch. A term rewriting laboratory with systematic and random generation and heuristic test facilities. Master’s thesis, Vienna University of Technology, 2008. URL: http://www.logic.at/staff/jiresch/thesis/thesis.pdf.
- J. Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. In Proc. 8th RTA, volume 1232 of LNCS, pages 241-253, 1997. URL: http://dx.doi.org/10.1007/3-540-62950-5_75.
- A. Stump, H. Zantema, G. Kimmell, and R. El Haj Omar. A rewriting view of simple typing. LMCS, 9(1), 2012. URL: http://dx.doi.org/10.2168/LMCS-9(1:4)2013.
- R. Treinen. The first-order theory of linear one-step rewriting is undecidable. TCS, 208(1-2):179-190, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(98)00083-8.
- S. Vorobyov. The undecidability of the first-order theories of one step rewriting in linear canonical systems. I&C, 175(2):182-213, 2002. URL: http://dx.doi.org/10.1006/inco.2002.3151.
- H. Zantema. Automatically finding non-confluent examples in term rewriting. In Proc. 2nd IWC, pages 11-15, 2013. URL: http://cl-informatik.uibk.ac.at/iwc/iwc2013.pdf.