Mechanically certifying formula-based Noetherian induction reasoning
From MaRDI portal
Publication:507366
DOI10.1016/j.jsc.2016.07.014zbMath1356.68202OpenAlexW2480458138MaRDI QIDQ507366
Publication date: 6 February 2017
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2016.07.014
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- Using induction and rewriting to verify and complete parameterized specifications
- Proof by consistency
- Algebraic and logic programming. Second international conference, Nancy, France, October 1--3, 1990. Proceedings
- Deductive and inductive synthesis of equational programs
- Incorporating decision procedures in implicit induction.
- Isabelle/HOL. A proof assistant for higher-order logic
- Observational proofs by rewriting.
- Mechanical verification of an ideal incremental ABR conformance algorithm
- Automata-driven automated induction
- Simultaneous checking of completeness and ground confluence for algebraic specifications
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
- Automated Certification of Implicit Induction Proofs
- Sequent calculi for induction and infinite descent
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
- Certification of Automated Termination Proofs
- Dealing with Non-orientable Equations in Rewriting Induction
- Descente Infinie + Deduction
- Automated Mathematical Induction
- Program-ing finger trees in C <scp>oq</scp>
- Lazy generation of induction hypotheses
- Induction using term orderings
- A Machine-Checked Proof of the Odd Order Theorem
- Equations: A Dependent Pattern-Matching Compiler
- Conditional rewriting in focus
- Automated Deduction – CADE-19
- A general framework to build contextual cover set induction provers
This page was built for publication: Mechanically certifying formula-based Noetherian induction reasoning
