Proving ground confluence and inductive validity in constructor based equational specifications

DOI10.1007/3-540-56610-4_55zbMath1497.68286OpenAlexW1596501052MaRDI QIDQ5044723

Klaus 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

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

Related Items (2)

On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Improving rewriting induction approach for proving ground confluence

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automating inductionless induction using test sets
• Proofs by induction in equational theories with constructors
• On sufficient-completeness and related properties of term rewriting systems
• Proof by consistency
• Basic narrowing revisited
• Semantic confluence tests and completion methods
• Proving Properties of Programs by Structural Induction

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