Document Open Access Logo

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

Authors Franziska Rapp, Aart Middeldorp

PDF

File

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

Document Identifiers

Subject Classification

Keywords
  • first-order theory
  • ground rewrite systems
  • automation
  • synthesis

Metrics

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

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.

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

Author Details

Franziska Rapp
Aart Middeldorp

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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact