Certifying proofs in the first-order theory of rewriting

DOI10.1007/978-3-030-72013-1_7zbMath1474.68166OpenAlexW3137228870MaRDI QIDQ2233502

Aart Middeldorp, Alexander Lochmann, Bertram Felgenhauer, Fabian Mitterwallner

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-72013-1_7

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Related Items

First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification

Uses Software

• Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• FORT 2.0
• Sequentiality, monadic second-order logic and tree automata.
• Tools and algorithms for the construction and analysis of systems. 25 years of TACAS: TOOLympics, held as part of ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings. Part III
• Deriving Comparators and Show Functions in Isabelle/HOL
• MONA IMPLEMENTATION SECRETS
• Certification of Termination Proofs Using CeTA
• CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
• Proving Confluence of Term Rewriting Systems Automatically
• Term Rewriting and All That
• Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable

This page was built for publication: Certifying proofs in the first-order theory of rewriting