Inductive proofs by specification transformations

DOI10.1007/3-540-51081-8_101OpenAlexW1601086057MaRDI QIDQ5055713

Hubert Comon

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-51081-8_101

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

On finite representations of infinite sequences of terms, On relationship between term rewriting systems and regular tree languages, Specification and proof in membership equational logic, Unification in pseudo-linear sort theories is decidable, Solving divergence in Knuth--Bendix completion by enriching signatures, Regular expression order-sorted unification and matching, Automata-driven automated induction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proofs by induction in equational theories with constructors
• On the correspondence between two classes of reduction systems
• On sufficient-completeness and related properties of term rewriting systems
• Reductions in tree replacement systems
• Proof by consistency
• Automatic proofs by induction in theories without constructors
• Semantic confluence tests and completion methods