Extensions to a generalization critic for inductive proof

DOI10.1007/3-540-61511-3_68zbMATH Open1412.68238OpenAlexW2135869557MaRDI QIDQ4647499FDOQ4647499

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

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

zbMATH Keywords

term structureautomated deductioninductive proofbasic criticextended critic

Mathematics Subject Classification ID

Cites Work

• Edinburgh LCF. A mechanized logic of computation
• Productive use of failure in inductive proof
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A calculus for and termination of rippling
• Rippling: A heuristic for guiding inductive proofs
• The OYSTER-CLAM system

Cited In (6)

• A divergence critic
• Improvements in Formula Generalization
• Title not available (Why is that?)
• Title not available (Why is that?)
• Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
• Improving Generalization in Software IC3

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)