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
Descripción
Sumario: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 verified in Isabelle. Several extensions make the theory more expressive and FORT more versatile. We present a certificate language that enables the output of FORT to be certified by the certifier FORTify generated from the formalization, and we provide extensive experiments.

Ejemplares similares