一句话：为高阶约束 Horn 子句提出简单归结证明系统，并证明其在标准与 Henkin 语义下可靠且反驳完备。
本文研究高阶约束 Horn 子句（HoCHC）——一种高阶逻辑模理论的片段。作者提出一个简单的归结证明系统，并在标准语义与 Henkin 语义下证明其可靠性与反驳完备性。作为推论，对半可判定背景理论得到紧致性定理与 HoCHC 的半可判定性，并证明 HoCHC 具有规范模型性质。论文还证明一种由高阶到一阶逻辑的翻译变体在两种语义下都可靠且完备，并展示如何把一阶逻辑模理论（片段）的可判定性结果迁移到高阶设定；示例是 HoCHC 在受限线性整数算术下的 Bernays–Schönfinkel–Ramsey 片段。
We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC)-a system of higher-order logic modulo theories-and prove its soundness and refutational completeness w.r.t. both standard and Henkin semantics. As corollaries, we obtain the compactness theorem and semi-decidability of HoCHC for semi-decidable background theories, and we prove that HoCHC satisfies a canonical model property. Moreover a variant of the well-known translation from higher-order to 1st-order logic is shown to be sound and complete for HoCHC in both semantics. We illustrate how to transfer decidability results for (fragments of) 1st-order logic modulo theories to our higher-order setting, using as example the Bernays-Schonflukel-Ramsey fragment of HoCHC modulo a restricted form of Linear Integer Arithmetic.