Automated Certification of Implicit Induction Proofs

DOI10.1007/978-3-642-25379-9_5zbMath1350.68245OpenAlexW2126274963MaRDI QIDQ3100200

Vincent Demange, Sorin Stratulat

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_5

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Mechanically certifying formula-based Noetherian induction reasoning

Uses Software

• Coq
• OCaml
• seL4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inductive proof search modulo
• Incorporating decision procedures in implicit induction.
• Mechanical verification of an ideal incremental ABR conformance algorithm
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• Certification of Automated Termination Proofs
• Term Rewriting and All That
• Automated Mathematical Induction
• Automated Reasoning with Analytic Tableaux and Related Methods
• A general framework to build contextual cover set induction provers

This page was built for publication: Automated Certification of Implicit Induction Proofs