Certifying Proofs in the First-Order Theory of Rewriting

The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables...

Descripción completa

Detalles Bibliográficos
Autores principales: Mitterwallner, Fabian, Lochmann, Alexander, Middeldorp, Aart, Felgenhauer, Bertram
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2021
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984549/
http://dx.doi.org/10.1007/978-3-030-72013-1_7
_version_ 1783668088794775552
author Mitterwallner, Fabian
Lochmann, Alexander
Middeldorp, Aart
Felgenhauer, Bertram
author_facet Mitterwallner, Fabian
Lochmann, Alexander
Middeldorp, Aart
Felgenhauer, Bertram
author_sort Mitterwallner, Fabian
collection PubMed
description The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present FORT-h, a reincarnation of the decision tool FORT with certifiable output, and the formally verified certifier FORTify.
format Online
Article
Text
id pubmed-7984549
institution National Center for Biotechnology Information
language English
publishDate 2021
record_format MEDLINE/PubMed
spelling pubmed-79845492021-03-23 Certifying Proofs in the First-Order Theory of Rewriting Mitterwallner, Fabian Lochmann, Alexander Middeldorp, Aart Felgenhauer, Bertram Tools and Algorithms for the Construction and Analysis of Systems Article The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present FORT-h, a reincarnation of the decision tool FORT with certifiable output, and the formally verified certifier FORTify. 2021-02-26 /pmc/articles/PMC7984549/ http://dx.doi.org/10.1007/978-3-030-72013-1_7 Text en © The Author(s) 2021 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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 license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license 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.
spellingShingle Article
Mitterwallner, Fabian
Lochmann, Alexander
Middeldorp, Aart
Felgenhauer, Bertram
Certifying Proofs in the First-Order Theory of Rewriting
title Certifying Proofs in the First-Order Theory of Rewriting
title_full Certifying Proofs in the First-Order Theory of Rewriting
title_fullStr Certifying Proofs in the First-Order Theory of Rewriting
title_full_unstemmed Certifying Proofs in the First-Order Theory of Rewriting
title_short Certifying Proofs in the First-Order Theory of Rewriting
title_sort certifying proofs in the first-order theory of rewriting
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984549/
http://dx.doi.org/10.1007/978-3-030-72013-1_7
work_keys_str_mv AT mitterwallnerfabian certifyingproofsinthefirstordertheoryofrewriting
AT lochmannalexander certifyingproofsinthefirstordertheoryofrewriting
AT middeldorpaart certifyingproofsinthefirstordertheoryofrewriting
AT felgenhauerbertram certifyingproofsinthefirstordertheoryofrewriting

Ejemplares similares