Mechanically certifying formula-based Noetherian induction reasoning
type: Item
instance of: scholarly article
title: Mechanically certifying formula-based Noetherian induction reasoning
zbMATH Open document ID: 1356.68202
author: Sorin Stratulat
published in: Journal of Symbolic Computation
publication date: 2017-02-06T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 6680829
zbMATH Keywords: Noetherian induction
zbMATH Keywords: cyclic induction proofs
zbMATH Keywords: implicit induction proofs
zbMATH Keywords: proof certification
zbMATH Keywords: Coq
zbMATH Keywords: SPIKE
describes a project that uses: NQTHM
describes a project that uses: ORME
describes a project that uses: A3PAT
describes a project that uses: Equations
describes a project that uses: RRL
describes a project that uses: SPIKE
describes a project that uses: REVE
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: CoLoR
describes a project that uses: Flyspeck
MaRDI profile type: Publication
full work available at URL: j.jsc.2016.07.014
OpenAlex ID: W2480458138
cites work: Dealing with Non-orientable Equations in Rewriting Induction
cites work: Incorporating decision procedures in implicit induction.
cites work: Resolution theorem proving
cites work: Q2754027
cites work: Q4484330
cites work: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
cites work: Q4447243
cites work: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
cites work: Using induction and rewriting to verify and complete parameterized specifications
cites work: Simultaneous checking of completeness and ground confluence for algebraic specifications
cites work: Automata-driven automated induction
cites work: Automated Mathematical Induction
cites work: Observational proofs by rewriting.
cites work: Q2767092
cites work: Q3835049
cites work: Conditional rewriting in focus
cites work: Induction using term orderings
cites work: Sequent calculi for induction and infinite descent
cites work: Inductionless induction
cites work: Certification of Automated Termination Proofs
cites work: Automated Deduction – CADE-19
cites work: Orderings for term-rewriting systems
cites work: Deductive and inductive synthesis of equational programs
cites work: A Machine-Checked Proof of the Odd Order Theorem
cites work: Proof by consistency
cites work: Q3783519
cites work: Q4712663
cites work: Algebraic and logic programming. Second international conference, Nancy, France, October 1--3, 1990. Proceedings
cites work: Paramodulation-based theorem proving
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Lazy generation of induction hypotheses
cites work: Mechanical verification of an ideal incremental ABR conformance algorithm
cites work: Program-ing finger trees in C <scp>oq</scp>
cites work: Equations: A Dependent Pattern-Matching Compiler
cites work: A general framework to build contextual cover set induction provers
cites work: Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
cites work: Automated Certification of Implicit Induction Proofs
cites work: Descente Infinie + Deduction
cites work: Term rewriting induction
DOI: 10.1016/J.JSC.2016.07.014
description: scientific article; zbMATH DE number 6680829