Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization

Logic programming provides a uniform framework in which all aspects of explanation-based generalization and learning may be defined and carried out, but first-order Horn logic is not well suited to application domains such as theorem proving or program synthesis where functions and predicates are the objects of computation. We explore the use of a higher-order representation language and extend EBG to a higher-order logic programming language. Variables may now range over functions and predicates, which leads to an expansion of the space of possible generalizations. We address this problem by extending the logic with the modal operator (indicating necessary truth) which leads to the language λ Prolog. We develop a meta-interpreter realizing EBG for λ Prolog and give some examples in an version of this extended abstract which is available as a technical report [2].

• Type: Conference
• Year: 1989
• Where: ICML
• Authors: Scott Dietzen, Frank Pfenning
• Keywords: ICML 1989, Logic Programming, Machine Learning, Meta-interpreter Realizing Ebg, first-order Horn Logic