Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting

DOI10.1007/978-3-030-45237-7_11zbMath1483.68149OpenAlexW3016713933MaRDI QIDQ5164173

Aart Middeldorp, Alexander Lochmann

Publication date: 10 November 2021

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-45237-7_11

zbMATH Keywords

tree automataformalizationfirst-order theory of rewriting

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Certifying proofs in the first-order theory of rewriting

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability, confluence, and termination analysis with state-compatible automata
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Decidability for left-linear growing term rewriting systems.
• Isabelle/HOL. A proof assistant for higher-order logic
• 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
• Certification of Termination Proofs Using CeTA
• Term Rewriting and All That
• Proving non-termination by finite automata

This page was built for publication: Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting