Mechanically certifying formula-based Noetherian induction reasoning (Q507366): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CoLoR
@@ Property / describes a project that uses: CoLoR / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPIKE
@@ Property / describes a project that uses: SPIKE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.jsc.2016.07.014
+Normal rank
@@ Property / OpenAlex ID @@
+W2480458138
@@ Property / OpenAlex ID: W2480458138 / rank @@
+Normal rank
@@ Property / cites work @@
+Dealing with Non-orientable Equations in Rewriting Induction
+Normal rank
@@ Property / cites work @@
+Incorporating decision procedures in implicit induction.
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754027
@@ Property / cites work: Q2754027 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484330
@@ Property / cites work: Q4484330 / rank @@
+Normal rank
@@ Property / cites work @@
+Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Q4447243
@@ Property / cites work: Q4447243 / rank @@
+Normal rank
@@ Property / cites work @@
+CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
+Normal rank
@@ Property / cites work @@
+Using induction and rewriting to verify and complete parameterized specifications
+Normal rank
@@ Property / cites work @@
+Simultaneous checking of completeness and ground confluence for algebraic specifications
+Normal rank
@@ Property / cites work @@
+Automata-driven automated induction
@@ Property / cites work: Automata-driven automated induction / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Mathematical Induction
@@ Property / cites work: Automated Mathematical Induction / rank @@
+Normal rank
@@ Property / cites work @@
+Observational proofs by rewriting.
@@ Property / cites work: Observational proofs by rewriting. / rank @@
+Normal rank
@@ Property / cites work @@
+Q2767092
@@ Property / cites work: Q2767092 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3835049
@@ Property / cites work: Q3835049 / rank @@
+Normal rank
@@ Property / cites work @@
+Conditional rewriting in focus
@@ Property / cites work: Conditional rewriting in focus / rank @@
+Normal rank
@@ Property / cites work @@
+Induction using term orderings
@@ Property / cites work: Induction using term orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Sequent calculi for induction and infinite descent
+Normal rank
@@ Property / cites work @@
+Q2751366
@@ Property / cites work: Q2751366 / rank @@
+Normal rank
@@ Property / cites work @@
+Certification of Automated Termination Proofs
@@ Property / cites work: Certification of Automated Termination Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+Orderings for term-rewriting systems
@@ Property / cites work: Orderings for term-rewriting systems / rank @@
+Normal rank
@@ Property / cites work @@
+Deductive and inductive synthesis of equational programs
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Proof by consistency
@@ Property / cites work: Proof by consistency / rank @@
+Normal rank
@@ Property / cites work @@
+Q3783519
@@ Property / cites work: Q3783519 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4712663
@@ Property / cites work: Q4712663 / rank @@
+Normal rank
@@ Property / cites work @@
+Algebraic and logic programming. Second international conference, Nancy, France, October 1--3, 1990. Proceedings
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Lazy generation of induction hypotheses
@@ Property / cites work: Lazy generation of induction hypotheses / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical verification of an ideal incremental ABR conformance algorithm
+Normal rank
@@ Property / cites work @@
+Program-ing finger trees in C             <scp>oq</scp>
@@ Property / cites work: Program-ing finger trees in C <scp>oq</scp> / rank @@
+Normal rank
@@ Property / cites work @@
+Equations: A Dependent Pattern-Matching Compiler
@@ Property / cites work: Equations: A Dependent Pattern-Matching Compiler / rank @@
+Normal rank
@@ Property / cites work @@
+A general framework to build contextual cover set induction provers
+Normal rank
@@ Property / cites work @@
+Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
+Normal rank
@@ Property / cites work @@
+Automated Certification of Implicit Induction Proofs
+Normal rank
@@ Property / cites work @@
+Descente Infinie + Deduction
@@ Property / cites work: Descente Infinie + Deduction / rank @@
+Normal rank