遗传Harrop公式约束逻辑程序设计
Constraint Logic Programming with Hereditary Harrop Formula
摘要：
约束逻辑程序设计（CLP）和遗传Harrop公式（HH）是两种提高Horn子句表达能力的方法。在本文中，我们提出了一种新的组合这两种方法。我们展示了如何丰富的语法和证明理论的HH与一个给定的约束系统的帮助下，在这样一种方式，HH作为一个逻辑程序设计语言（即，存在的统一证明）的关键属性被保存。我们还提出了一个目标求解程序，显示其合理性和完整性计算答案的限制。由于这一结果，我们得到了一个新的强完备性定理CLP，避免了需要建立析取计算的答案，以及一个更抽象的制定一个已知的完整性定理HH。
英文摘要：
Constraint Logic Programming (CLP) and Hereditary Harrop formulas (HH) are two well known ways to enhance the expressivity of Horn clauses. In this paper, we present a novel combination of these two approaches. We show how to enrich the syntax and proof theory of HH with the help of a given constraint system, in such a way that the key property of HH as a logic programming language (namely, the existence of uniform proofs) is preserved. We also present a procedure for goal solving, showing its soundness and completeness for computing answer constraints. As a consequence of this result, we obtain a new strong completeness theorem for CLP that avoids the need to build disjunctions of computed answers, as well as a more abstract formulation of a known completeness theorem for HH.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
