Proving ground confluence and inductive validity in constructor based equational specifications

DOI10.1007/3-540-56610-4_55MaRDI QIDQ5044723zbMATH OpenOpenAlexFDO

Authors K. Becker

Publication date 2 November 2022

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-56610-4_55

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On notions of inductive validity for first-order equational clauses
• Automatic proofs by induction in theories without constructors
• Inductive proofs by specification transformations
• Ground confluence prover based on rewriting induction
• Proof by consistency

Cites work

• Automating inductionless induction using test sets
• Basic narrowing revisited
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 44484 (Why is no real title available?)
• scientific article; zbMATH DE number 1300969 (Why is no real title available?)
• scientific article; zbMATH DE number 1988979 (Why is no real title available?)
• On sufficient-completeness and related properties of term rewriting systems
• Proof by consistency
• Proofs by induction in equational theories with constructors
• Proving Properties of Programs by Structural Induction
• Semantic confluence tests and completion methods

Cited in

(9)

• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Constructor-Based Inductive Theorem Prover
• Deciding Equality in the Constructor Theory
• scientific article; zbMATH DE number 7455704 (Why is no real title available?)
• Improving rewriting induction approach for proving ground confluence
• On notions of inductive validity for first-order equational clauses
• A constructor-based approach for positive/negative-conditional equational specifications
• Proving ground confluence of equational specifications modulo axioms
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies

This page was built for publication: Proving ground confluence and inductive validity in constructor based equational specifications

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