Knowledge Representation, Computation, and Learning in Higher-order Logic
John Wylie Lloyd · 2002
This paper contains a systematic study of the foundations of knowledge representation, computation, and learning in higher-order logic. First, a polymorphically-typed higher-order logic, whose origins can be traced back to Church's simple theory of types, is presented. A model theory and proof theory for this logic are developed and basic theorems relating these two are given. A metric space of certain closed terms, which provides a rich language for representing individuals, is then studied. Also a method of systematically constructing predicates on such individuals is given. The technique of programming with abstractions is illustrated. Major applications of the logic to declarative programming languages and machine learning are indicated. 1