Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
From MaRDI portal
Publication:3522029
DOI10.1007/978-3-540-70590-1_24zbMath1145.68454OpenAlexW1480151951MaRDI QIDQ3522029
Publication date: 28 August 2008
Published in: Rewriting Techniques and Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-70590-1_24
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Mechanically certifying formula-based Noetherian induction reasoning ⋮ Automated Certification of Implicit Induction Proofs
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- Automated theorem proving by test set induction
- Incorporating decision procedures in implicit induction.
- Mechanical verification of an ideal incremental ABR conformance algorithm
- Implicit induction in conditional theories
- Dealing with Non-orientable Equations in Rewriting Induction
- Proving termination with multiset orderings
- Descente Infinie + Deduction
- Automated Mathematical Induction
- Automated Reasoning with Analytic Tableaux and Related Methods
- A general framework to build contextual cover set induction provers
This page was built for publication: Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
