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
Descripción
Sumario: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.

Ejemplares similares