Lazy generation of induction hypotheses

DOI10.1007/3-540-58156-1_4zbMath1433.68563OpenAlexW1548250926MaRDI QIDQ5210761

Martin Protzen

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_4

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Middle-out reasoning for synthesis and induction ⋮ Proving theorems by reuse ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Patching faulty conjectures

Uses Software

• Coq

Cites Work

• Rippling: A heuristic for guiding inductive proofs
• Mechanizing structural induction. II: Strategies
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Lazy generation of induction hypotheses