Inductive proofs by specification transformations

DOI10.1007/3-540-51081-8_101MaRDI QIDQ5055713zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Automatic proofs by induction in theories without constructors
• Proofs by induction in equational theories with constructors
• Induction = I-axiomatization + first-order consistency.
• scientific article; zbMATH DE number 3891336
• Proof by consistency

Cites work

• Automatic proofs by induction in theories without constructors
• scientific article; zbMATH DE number 4164137 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 4060701 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• On sufficient-completeness and related properties of term rewriting systems
• On the correspondence between two classes of reduction systems
• Proof by consistency
• Proofs by induction in equational theories with constructors
• Reductions in tree replacement systems
• Semantic confluence tests and completion methods

Cited in

(26)

• Equational formulae with membership constraints
• Automatic proofs by induction in theories without constructors
• Induction = I-axiomatization + first-order consistency.
• Automata-driven automated induction
• Inductive theorem proving for design specifications
• Specification and proof in membership equational logic
• Order-sorted equality enrichments modulo axioms
• Turning Inductive into Equational Specifications
• Inductive prover based on equality saturation for a lazy functional language
• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• scientific article; zbMATH DE number 4074541 (Why is no real title available?)
• scientific article; zbMATH DE number 67458 (Why is no real title available?)
• scientific article; zbMATH DE number 139989 (Why is no real title available?)
• scientific article; zbMATH DE number 177848 (Why is no real title available?)
• Unification in pseudo-linear sort theories is decidable
• Proving ground confluence and inductive validity in constructor based equational specifications
• On relationship between term rewriting systems and regular tree languages
• On notions of inductive validity for first-order equational clauses
• Generic induction proofs
• On finite representations of infinite sequences of terms
• Proof by consistency in conditional equational theories
• Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
• Solving divergence in Knuth--Bendix completion by enriching signatures
• Regular expression order-sorted unification and matching
• Proofs by induction in equational theories with constructors
• A general proof rule for procedures in predicate transformer semantics

This page was built for publication: Inductive proofs by specification transformations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055713)