Document Open Access Logo

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

Authors Franziska Rapp, Aart Middeldorp



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.36.pdf
  • Filesize: 0.49 MB
  • 12 pages

Document Identifiers

Author Details

Franziska Rapp
Aart Middeldorp

Cite AsGet 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.
Keywords
  • first-order theory
  • ground rewrite systems
  • automation
  • synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  2. 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.
  3. 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.
  4. 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.
  5. M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable (extended version). Technical Report I.T. 197, LIFL, 1990. Google Scholar
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
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