A typed -calculus for proving-by-example and bottom-up generalization procedure

DOI10.1016/0304-3975(94)00159-GMaRDI QIDQ674399zbMATH OpenFDO

Authors Masami Hagiya

Publication date 28 February 1997

Published in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 4058907
• Programming by example and proving by example using higher-order unification
• Mechanical procedure for proof construction via closed terms in typed calculus
• Sound generalizations in mathematical induction
• Mathematical induction in Otter-lambda

Cites work

• scientific article; zbMATH DE number 4164123 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 1324440 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• From programming-by-example to proving-by-example
• Introduction to generalized type systems
• On the SUP-INF Method for Proving Presburger Formulas
• Parallel reductions in \(\lambda\)-calculus
• Programming by example and proving by example using higher-order unification

Cited in

(6)

• Programming by example and proving by example using higher-order unification
• Synthesis of rewrite programs by higher-order and semantic unification
• scientific article; zbMATH DE number 4058907 (Why is no real title available?)
• A new application for explanation-based generalisation within automated deduction
• Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
• Mechanical procedure for proof construction via closed terms in typed \(\lambda\) calculus

This page was built for publication: A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure

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