Automated Certification of Implicit Induction Proofs

DOI10.1007/978-3-642-25379-9_5MaRDI QIDQ3100200zbMATH OpenOpenAlexFDO

Authors Sorin Stratulat, Vincent Demange

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)

Recommendations

• scientific article; zbMATH DE number 1389654
• scientific article; zbMATH DE number 3880144
• Automating Inductive Proofs Using Theory Exploration
• Automatic proofs by induction in theories without constructors
• The automation of proof by mathematical induction
• Automated constructivization of proofs
• Automated theorem proving by test set induction
• Automated mutual explicit induction proof in separation logic
• Automated mutual induction proof in separation logic

Cites work

• A general framework to build contextual cover set induction provers
• Automated Mathematical Induction
• Automated Reasoning with Analytic Tableaux and Related Methods
• Certification of Automated Termination Proofs
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• scientific article; zbMATH DE number 1670787 (Why is no real title available?)
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• scientific article; zbMATH DE number 2043539 (Why is no real title available?)
• Incorporating decision procedures in implicit induction.
• Inductive proof search modulo
• Mechanical verification of an ideal incremental ABR conformance algorithm
• Term Rewriting and All That

Cited in

(3)

• Automating Inductive Proofs Using Theory Exploration
• Mechanically certifying formula-based Noetherian induction reasoning
• A unified view of induction reasoning for first-order logic

Describes a project that uses

Uses Software

• OCaml
• Coq
• seL4

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

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