Higher-order and modal logic as a framework for explanation-based generalization

Abstract

Abstract: "Certain tasks, such as formal program development and theorem proving, are inherently higher-order because they fundamentally rely upon the manipulation of higher-order objects and predicates. Computing tools intended to assist these higher-order 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 been limited to first-order problems. We extend EBG to generalize higher-order values, thereby facilitating its application to higher-order domains.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 [lambda]Prolog, a higher-order logic programming language, as a framework for realizing higher-order EBG. This requires extending [lambda]Prolog with the necessity operator [box] of modal logic, which leads to the language [lambda][superscript [box]]Prolog. The necessity operator elegantly captures the distinction between domain theory and training instance upon which EBG depends. We develop a meta-interpreter realizing EBG for [lambda][superscript [box]]Prolog and provide examples of higher-order EBG.EBG has been described as 'speed-up' generalization in that its results, while improving performance, do not address previously unsolvable problems. By extending the framework with user interaction, EBG becomes a means by which user-provided search-control knowledge may be mademanifest. This facilitates application to domains in which unguided problem solving is often intractable. Of particular interest to us, and thus investigated here, are theorem proving and formal development."