3 Higher-Order Model Generation

Abstract

The simply typed λ-calculus can be taken as the basis of a formalism in which we assign meaning to the basic expressions of a natural language and explain the meaning of larger constituents by the composition of the meaning of their parts. However, under a conventional higher-order semantic for the λ-calculus, we cannot give a model generation method based on the well-known techniques of first-order model generation. By weakening the semantic of higher-order logic, we formulate a logical language that has the compositional expressivity of a higher-order logic but the finitely representable models of a first-order one. A generic model generation technique for this language is presented and discussed, and a refinement for minimal model generation is introduced.