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
_version_ 1785020781714997248
author Middeldorp, Aart
Lochmann, Alexander
Mitterwallner, Fabian
author_facet Middeldorp, Aart
Lochmann, Alexander
Mitterwallner, Fabian
author_sort Middeldorp, Aart
collection PubMed
description 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.
format Online
Article
Text
id pubmed-10079773
institution National Center for Biotechnology Information
language English
publishDate 2023
publisher Springer Netherlands
record_format MEDLINE/PubMed
spelling pubmed-100797732023-04-08 First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification Middeldorp, Aart Lochmann, Alexander Mitterwallner, Fabian J Autom Reason Research 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. Springer Netherlands 2023-04-06 2023 /pmc/articles/PMC10079773/ /pubmed/37038593 http://dx.doi.org/10.1007/s10817-023-09661-7 Text en © The Author(s) 2023 https://creativecommons.org/licenses/by/4.0/Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/ (https://creativecommons.org/licenses/by/4.0/) .
spellingShingle Research
Middeldorp, Aart
Lochmann, Alexander
Mitterwallner, Fabian
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
title First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
title_full First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
title_fullStr First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
title_full_unstemmed First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
title_short First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
title_sort first-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
topic Research
url 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
work_keys_str_mv AT middeldorpaart firstordertheoryofrewritingforlinearvariableseparatedrewritesystemsautomationformalizationcertification
AT lochmannalexander firstordertheoryofrewritingforlinearvariableseparatedrewritesystemsautomationformalizationcertification
AT mitterwallnerfabian firstordertheoryofrewritingforlinearvariableseparatedrewritesystemsautomationformalizationcertification

Ejemplares similares