Mechanically certifying formula-based Noetherian induction reasoning

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

Authors 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)

Recommendations

• Automated Certification of Implicit Induction Proofs
• Induction = I-axiomatization + first-order consistency.
• Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
• Automatic proofs by induction in theories without constructors
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities

Cites Work

• scientific article; zbMATH DE number 1670732 (Why is no real title available?)
• scientific article; zbMATH DE number 1696825 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 4112064 (Why is no real title available?)
• scientific article; zbMATH DE number 2043539 (Why is no real title available?)
• scientific article; zbMATH DE number 1927413 (Why is no real title available?)
• scientific article; zbMATH DE number 4776 (Why is no real title available?)
• A general framework to build contextual cover set induction provers
• A machine-checked proof of the odd order theorem
• Algebraic and logic programming. Second international conference, Nancy, France, October 1--3, 1990. Proceedings
• Automata-driven automated induction
• Automated Certification of Implicit Induction Proofs
• Automated Mathematical Induction
• Certification of Automated Termination Proofs
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• Conditional rewriting in focus
• Dealing with Non-orientable Equations in Rewriting Induction
• Deductive and inductive synthesis of equational programs
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Descente Infinie + Deduction
• Equations: a dependent pattern-matching compiler
• Incorporating decision procedures in implicit induction.
• Induction using term orderings
• Inductionless induction
• Isabelle/HOL. A proof assistant for higher-order logic
• Lazy generation of induction hypotheses
• Mechanical verification of an ideal incremental ABR conformance algorithm
• Observational proofs by rewriting.
• Orderings for term-rewriting systems
• Paramodulation-based theorem proving
• Program-ing finger trees in Coq
• Proof by consistency
• Proof search and proof check for equational and inductive theorems.
• Resolution theorem proving
• Sequent calculi for induction and infinite descent
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• Term rewriting induction
• Using induction and rewriting to verify and complete parameterized specifications

Cited In (4)

• Title not available (Why is no real title available?)
• Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities

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)