First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification

The first-order theory of rewriting is decidable for linear variable-separated rewrite systems. We present a new decision procedure which is the basis of FORT, a decision and synthesis tool for properties expressible in the theory. The decision procedure is based on tree automata techniques and veri...

Descripción completa

Detalles Bibliográficos
Autores principales: Middeldorp, Aart, Lochmann, Alexander, Mitterwallner, Fabian
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2023
Materias:
Research
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10079773/
https://www.ncbi.nlm.nih.gov/pubmed/37038593
http://dx.doi.org/10.1007/s10817-023-09661-7

Internet

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10079773/
https://www.ncbi.nlm.nih.gov/pubmed/37038593
http://dx.doi.org/10.1007/s10817-023-09661-7

Ejemplares similares