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.

翻译：本文针对高阶遗传哈罗普公式（HOHH）的消解引入了模型理论，该逻辑是Lambda-Prolog编程语言的基础，并证明了消解的可靠性与完备性。该形式系统的语义与完备性证明通过多种方式展示，这些方式经过适当调整以处理高阶逻辑的非直谓性——该特性排除了基于公式结构归纳的真值定义。首先，我们采用Apt与Van Emden风格，使用解释上特定算子的最小不动点。随后，利用林登鲍姆代数的证明论变体给出了一个构造性完备性定理，该证明同时包含了一种建立切割消去的新方法。