Appropriate lemmae discovery

DOI10.1016/J.INS.2003.06.012MaRDI QIDQ1827320zbMATH OpenOpenAlexFDO

Authors M. Demba, Khaled Bsaies

Publication date 6 August 2004

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ins.2003.06.012

zbMATH Keywords

Automated theorem provingImplicative formulaeLemmae discoveryMathematical inductionProgram synthesis

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Lemma discovery for induction. A survey
• Lemma discovery in automating induction
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• On the generation of quantified lemmas
• Sound lemma generation for proving inductive validity of equations

Cites work

• scientific article; zbMATH DE number 3956408 (Why is no real title available?)
• 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?)
• Lemma discovery in automating induction
• Productive use of failure in inductive proof
• The automation of proof by mathematical induction

Cited in

(8)

• On terminating lemma speculations.
• The resonance strategy
• Patching faulty conjectures
• Predicting failures of and repairing inductive proof attempts
• Lemma discovery in automating induction
• Automatic generation of generalization lemmas for proving properties of tail-recursive definitions
• Lemma discovery for induction. A survey
• Lazy generation of induction hypotheses

This page was built for publication: Appropriate lemmae discovery

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