Appropriate lemmae discovery

DOI10.1016/J.INS.2003.06.012zbMATH Open1049.03010OpenAlexW2075452789MaRDI QIDQ1827320FDOQ1827320

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

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

zbMATH Keywords

Automated theorem provingImplicative formulaeLemmae discoveryMathematical inductionProgram synthesis

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Productive use of failure in inductive proof
• The automation of proof by mathematical induction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Lemma discovery in automating 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)