Automated Mathematical Induction

DOI10.1093/LOGCOM/5.5.631MaRDI QIDQ4849648zbMATH OpenOpenAlexFDO

Authors Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch

Publication date 20 February 1996

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/94ea3100907cc2f50b7a37c480f2ac4918210b4d

zbMATH Keywords

program verificationspecification systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated mathematical induction
• scientific article; zbMATH DE number 907678
• The automation of proof by mathematical induction
• Automata-driven automated induction
• scientific article; zbMATH DE number 4043814
• Automated theorem proving methods

Cited in

(23)

• Rule-based induction
• Automated theorem proving by test set induction
• Test sets for the universal and existential closure of regular tree languages.
• Automata-driven automated induction
• Sound generalizations in mathematical induction
• Implicit induction in conditional theories
• Automated mathematical induction
• Automated Certification of Implicit Induction Proofs
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• scientific article; zbMATH DE number 3898269 (Why is no real title available?)
• scientific article; zbMATH DE number 1149426 (Why is no real title available?)
• scientific article; zbMATH DE number 4776 (Why is no real title available?)
• scientific article; zbMATH DE number 907678 (Why is no real title available?)
• Mechanically certifying formula-based Noetherian induction reasoning
• Improving rewriting induction approach for proving ground confluence
• A divergence critic
• On notions of inductive validity for first-order equational clauses
• Correctness of Context-Moving Transformations for Term Rewriting Systems
• A general framework to build contextual cover set induction provers
• Using induction and rewriting to verify and complete parameterized specifications
• A unified view of induction reasoning for first-order logic
• Induction models on \(\mathbb{N}\)
• Formal design and verification of operational transformation algorithms for copies convergence

This page was built for publication: Automated Mathematical Induction

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