  This paper introduces a model theory for resolution on Higher Order
Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog
programming language, and proves soundness and completeness of resolution. The
semantics and the proof of completeness of the formal system is shown in
several ways, suitably adapted to deal with the impredicativity of higher-order
logic, which rules out definitions of truth based on induction on formula
structure. First, we use the least fixed point of a certain operator on
interpretations, in the style of Apt and Van Emden, Then a constructive
completeness theorem is given using a proof theoretic variant of the Lindenbaum
algebra, which also contains a new approach to establishing cut-elimination.
