Mechanically certifying formula-based Noetherian induction reasoning

DOI10.1016/J.JSC.2016.07.014zbMATH Open1356.68202OpenAlexW2480458138MaRDI QIDQ507366FDOQ507366

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

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• Isabelle/HOL. A proof assistant for higher-order logic
• Resolution theorem proving
• Orderings for term-rewriting systems
• Observational proofs by rewriting.
• Paramodulation-based theorem proving
• Sequent calculi for induction and infinite descent
• Automata-driven automated induction
• Using induction and rewriting to verify and complete parameterized specifications
• Descente Infinie + Deduction
• Proof by consistency
• Inductionless induction
• A Machine-Checked Proof of the Odd Order Theorem
• 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.
• Mechanical verification of an ideal incremental ABR conformance algorithm
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• Automated Certification of Implicit Induction Proofs
• 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
• Automated Mathematical Induction
• Program-ing finger trees in C <scp>oq</scp>
• Lazy generation of induction hypotheses
• Induction using term orderings
• Equations: A Dependent Pattern-Matching Compiler
• Conditional rewriting in focus
• Automated Deduction – CADE-19
• A general framework to build contextual cover set induction provers
• Term rewriting induction

Cited In (3)

• Title not available (Why is that?)
• Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques

Uses Software

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

This page was built for publication: Mechanically certifying formula-based Noetherian induction reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q507366)