Patching faulty conjectures

DOI10.1007/3-540-61511-3_70zbMath1415.03027OpenAlexW2108239812MaRDI QIDQ4647501

Martin Protzen

Publication date: 15 January 2019

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

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_70

zbMATH Keywords

proof treeinduction proofrecursive callground terminduction hypothesis

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• On proving the termination of algorithms by machine
• Lazy generation of induction hypotheses
• Two Examples of Computational Creativity: ILP Multiple Predicate Synthesis and the ‘Assets’ in Theorem Proving