Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
From MaRDI portal
(Redirected from Publication:3522029)
Recommendations
- Dealing with Non-orientable Equations in Rewriting Induction
- Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
- Term rewriting induction
- How to prove equivalence of term rewriting systems without induction
- Mechanically certifying formula-based Noetherian induction reasoning
Cites work
- A general framework to build contextual cover set induction provers
- Automated Mathematical Induction
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automated theorem proving by test set induction
- Dealing with Non-orientable Equations in Rewriting Induction
- Descente Infinie + Deduction
- scientific article; zbMATH DE number 2043539 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Implicit induction in conditional theories
- Incorporating decision procedures in implicit induction.
- Mechanical verification of an ideal incremental ABR conformance algorithm
- Orderings for term-rewriting systems
- Proving termination with multiset orderings
- Term rewriting induction
- The automation of proof by mathematical induction
Cited in
(4)
This page was built for publication: Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3522029)
