Extensions to a generalization critic for inductive proof

DOI10.1007/3-540-61511-3_68MaRDI QIDQ4647499zbMATH OpenOpenAlexFDO

Authors Andrew Ireland, Alan Bundy

Publication date 15 January 2019

Published in Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL https://www.pure.ed.ac.uk/ws/files/411724/Extensions_to_a_generalization_critic_for_inductive_proof.pdf

zbMATH Keywords

term structureautomated deductioninductive proofbasic criticextended critic

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1149426
• A divergence critic
• Extensions to the rippling-out tactic for guiding inductive proofs
• scientific article; zbMATH DE number 1927422
• Sound generalizations in mathematical induction

Cites work

• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3237808 (Why is no real title available?)
• A calculus for and termination of rippling
• Edinburgh LCF. A mechanized logic of computation
• Productive use of failure in inductive proof
• Rippling: A heuristic for guiding inductive proofs
• The OYSTER-CLAM system

Cited in

(6)

• scientific article; zbMATH DE number 1614721 (Why is no real title available?)
• scientific article; zbMATH DE number 1927422 (Why is no real title available?)
• Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
• Improvements in Formula Generalization
• A divergence critic
• Improving Generalization in Software IC3

Describes a project that uses

Uses Software

• CLAM
• Oyster

This page was built for publication: Extensions to a generalization critic for inductive proof

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