A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure

DOI10.1016/0304-3975(94)00159-GzbMath0873.68186MaRDI QIDQ674399

Masami Hagiya

Publication date: 28 February 1997

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

Mathematics Subject Classification ID

Related Items

Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, A new application for explanation-based generalisation within automated deduction, Synthesis of rewrite programs by higher-order and semantic unification

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the SUP-INF Method for Proving Presburger Formulas
• Introduction to generalized type systems
• From programming-by-example to proving-by-example
• Parallel reductions in \(\lambda\)-calculus