Lemma discovery in automating induction

DOI10.1007/3-540-61511-3_112MaRDI QIDQ4647546zbMATH OpenOpenAlexFDO

Authors Deepak Kapur, Mahadevan Subramaniam

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_112

Mathematics Subject Classification ID

Recommendations

• Appropriate lemmae discovery
• Lemma discovery for induction. A survey
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Lazy generation of induction hypotheses
• Automatic generation of generalization lemmas for proving properties of tail-recursive definitions

Cites work

• scientific article; zbMATH DE number 4074541 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 1348478 (Why is no real title available?)
• scientific article; zbMATH DE number 1149426 (Why is no real title available?)
• New uses of linear arithmetic in automated theorem proving by induction
• Productive use of failure in inductive proof
• Rippling: A heuristic for guiding inductive proofs

Cited in

(10)

• Sound lemma generation for proving inductive validity of equations
• Sound generalizations in mathematical induction
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Automatic generation of generalization lemmas for proving properties of tail-recursive definitions
• Lemma discovery for induction. A survey
• Dynamic rippling, middle-out reasoning and lemma discovery
• Lazy generation of induction hypotheses
• Appropriate lemmae discovery
• A combinator language for theorem discovery
• Proving theorems by reuse

Describes a project that uses

Uses Software

• RRL

This page was built for publication: Lemma discovery in automating induction

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