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

(20)

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

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)