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

DOI10.1016/0304-3975(94)00159-GzbMATH Open0873.68186MaRDI QIDQ674399FDOQ674399

Masami Hagiya

Publication date: 28 February 1997

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

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 \(\lambda\) calculus
• Sound generalizations in mathematical induction
• Mathematical induction in Otter-lambda

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• On the SUP-INF Method for Proving Presburger Formulas
• Title not available (Why is that?)
• Title not available (Why is that?)
• Introduction to generalized type systems
• From programming-by-example to proving-by-example
• 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
• Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
• Mechanical procedure for proof construction via closed terms in typed \(\lambda\) calculus
• Title not available (Why is that?)
• A new application for explanation-based generalisation within automated deduction

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)