Proving ground confluence and inductive validity in constructor based equational specifications
From MaRDI portal
Publication:5044723
DOI10.1007/3-540-56610-4_55zbMath1497.68286MaRDI QIDQ5044723
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
68Q60: Specification and verification (program logics, model checking, etc.)
68Q42: Grammars and rewriting systems
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
Improving rewriting induction approach for proving ground confluence, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
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