结合遗传 Harrop 公式的约束逻辑编程
编程语言
2007-05-23 v1
摘要
约束逻辑编程（CLP）与遗传 Harrop 公式（HH）是增强 Horn 子句表达能力的两种著名方法。在本文中，我们提出了一种结合这两种方法的新途径。我们展示了如何在给定约束系统的帮助下丰富 HH 的语法与证明论，使得 HH 作为逻辑编程语言的关键性质（即一致证明的存在性）得以保持。我们还提出了一个目标求解过程，证明了其在计算回答约束时的可靠性与完备性。作为该结果的推论，我们得到了 CLP 的一个新的强完备性定理，避免了构建计算回答的析取的需要，同时也得到了 HH 已知完备性定理的一个更抽象的表述。
引用
@article{arxiv.cs/0404053,
title = {Constraint Logic Programming with Hereditary Harrop Formula},
author = {Javier Leach and Susana Nieva and Mario Rodriguez-Artalejo},
journal= {arXiv preprint arXiv:cs/0404053},
year = {2007}
}
备注
Appeared in Theory and Practice of Logic Programming, vol. 1, no. 4, 2001. Appeared in Theory and Practice of Logic Programming, vol. 1, no. 4, 2001