Mechanically certifying formula-based Noetherian induction reasoning

DOI10.1016/j.jsc.2016.07.014zbMath1356.68202OpenAlexW2480458138MaRDI QIDQ507366

Sorin Stratulat

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

zbMATH Keywords

Coqcyclic induction proofsimplicit induction proofsNoetherian inductionproof certificationSPIKE

Mathematics Subject Classification ID

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

• Coq
• Isabelle/HOL
• SPIKE
• NQTHM
• CoLoR
• SPIKE
• Flyspeck
• ORME
• A3PAT
• Equations
• RRL
• REVE

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