约束逻辑编程

约束逻辑编程是约束编程的一种形式，其中逻辑编程被扩展到包括约束满足的概念。约束逻辑程序是一个逻辑程序，它在子句的主体中包含约束。如同在常规逻辑编程中一样，程序被查询到一个目标的可证明性，该目标除了字面意思外还可能包含约束条件。一个目标的证明是由子句组成的，子句的主体是可满足的约束和字词，而这些约束和字词又可以用其他子句来证明。执行是由解释器进行的，它从目标开始，递归地扫描试图证明目标的子句。在这个扫描过程中遇到的约束被放在一个叫做约束存储的集合中。如果这个集合被发现是不可满足的，解释器就会回溯，尝试使用其他条款来证明目标。在实践中，约束存储的可满足性可以用一个不完全的算法来检查，该算法并不总是能发现不一致的地方。

从形式上看，约束逻辑程序与常规的逻辑程序一样，但是除了常规的逻辑编程字词之外，子句的主体还可以包含约束。像常规逻辑编程一样，这又需要证明目标B(X,1)。与常规逻辑编程相反，这也需要满足一个约束条件。X>0，最后一个子句中的约束（在常规逻辑编程中，X>0不能被证明，除非X被绑定到一个完全接地的项上，如果不是这样，程序的执行将失败）。一个约束是否被满足并不总是在遇到该约束时就能确定。例如，在这种情况下，当最后一个子句被评估时，X的值就不能确定。因此，在这一点上，X>0的约束没有被满足，也没有被违反。解释器不是在评价B(X,1)时继续进行，然后检查X的结果值是否为正值，而是存储约束X>0，然后在评价B(X,1)时继续进行；这样，解释器可以在评价B(X,1)时发现对约束X>0的违反，如果是这种情况，可以立即进行回溯，而不是等待B(X,1)的评价结束。

一般来说，约束逻辑程序的评估和普通逻辑程序一样进行。然而，在评估过程中遇到的约束被放在一个叫做约束存储的集合中。例如，对目标A(X,1)的评价是通过评价xxx个子句的主体Y=1来进行的；这种评价将X>0添加到约束存储中，并要求目标B(X,1)被证明。在试图证明这个目标时，xxx个子句被应用，但是它的评价将X<0添加到约束存储中。这个添加使得约束存储不可满足。解释器然后回溯，从约束存储中删除最后的添加。第二个子句的评估将X=1和Y>0添加到约束库中。由于约束存储是可满足的，并且没有其他的字词需要证明，解释器以解决方案X=1，Y=1而停止。

约束逻辑程序的语义可以用一个虚拟解释器来定义，该解释器维护一对在执行过程中。这一对中的xxx个元素被称为当前目标；第二个元素被称为约束存储。当前目标包含解释器试图证明的字词，也可能包含它试图满足的一些约束；约束存储包含解释器到目前为止假设可满足的所有约束。最初，当前的目标是目标，约束存储是空的。解释器通过从当前目标中移除xxx个元素并对其进行分析来开展工作。这个分析的细节将在下面解释，但最后这个分析可能产生一个成功的终止或失败。这个分析可能涉及到递归调用和向当前目标添加新的字词以及向约束存储添加新的约束。