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

Abstract

Certain tasks, such as formal program development and theorem proving, fundamentally rely upon the manipulation of higher-order objects such as functions and predicates. Computing tools intended to assist in performing these tasks are at present inadequate in both the amount of ‘knowledge’ they contain ( i.e. , the level of support they provide) and in their ability to ‘learn’ ( i.e. , their capacity to enhance that support over time). The application of a relevant machine learning technique—explanation-based generalization (EBG)—has thus far been limited to first-order problem representations. We extend EBG to generalize higher-order values, thereby enabling its application to higher-order problem encodings. Logic programming provides a uniform framework in which all aspects of explanation-based generalization and learning may be defined and carried out. First-order Horn logics ( e.g. , Prolog) are not, however, well suited to higher-order applications. Instead, we employ λProlog, a higher-order logic programming language, as our basic framework for realizing higher-order EBG. In order to capture the distinction between domain theory and training instance upon which EBG relies, we extend λProlog with the necessity operator □ of modal logic. We develop a meta-interpreter realizing EBG for the extended language, λ^□Prolog, and provide examples of higher-order EBG.