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

automated deductionbasic criticextended criticinductive proofterm structure

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

• A calculus for and termination of rippling
• Edinburgh LCF. A mechanized logic of computation
• 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?)
• Productive use of failure in inductive proof
• Rippling: A heuristic for guiding inductive proofs
• The OYSTER-CLAM system

Cited in

(7)

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

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)