Towards Inductive Generalization in Higher Order Logic

Abstract

In many cases, higher order (Horn) clauses are more suited to express certain concepts when relations between predicates exist. However, to date there has been no appropriate higher order formalism within which efficient inductive generalisation can be carried out. This paper describes inductive generalisation in Mλ – a higher order formalism which not only retains the expressiveness of λ-calculus but also provides for effective and efficient inductive generalisation. The main strength of Rλ is twofold: it is a higher formalism extension of the (clausal) first order logic and it can be mechanised in a way similar to the first order case in Horn clause form. For a class of restricted Mλ, their least general generalisation (LGG) is unique, and so is their most general unification. Inductive generalisation in Mλ is implemented in the algorithm HOLGG. This algorithm has been applied to some interesting induction problems in the induction of higher order rule templates and automatic program transformation.