发布网友 发布时间:2022-04-24 10:00
共1个回答
热心网友 时间:2023-05-25 11:41
现行逻辑程序的基本语句属于一阶谓词演算的一个子集,HORN子句集。HORN子句的一般形式为:A1,…,Am←B1,B2,…,Bn,其中Ai(1≤i≤m)、Bj(1≤j≤n)都是原子公式,分别代表结论和前提的形式。前提部分是各原子的合取式,构成子句体,结论部分最多只有一个原子,称为子句头。由此可将HORN子句分成两个基本类型:①有头HORN子句(用来代表一条规则),例如,grandfather(x,z)←father(x,y),father (y,z)代表:x是y的父亲且y是z的父亲,则x是z的祖父。有头无体的HORN子句是一断言(用来代表一个事实)。例如,father(A,B)代表:A是B的父亲,father(B,C)代表:B是C的父亲。②无头HORN子句,称为目标语句(用来代表结论的否定式),例如,←grandfather(A,C)代表:A不是C的祖父。逻辑学家A.霍恩对这类子句性质作了详尽的研究,HORN子句即因此得名。
从问题归约的角度看,可将HORN子句解释为一过程,它将问题(目标)A归约为若干子问题(子目标),每一子问题Bi(1≤i≤n)又可解释为对其他过程(HORN子句)的调用。有头无尾的HORN子句则代表一个已知其解的基元问题。过程调用实际上是使构成子句体的一个原子(子目标)与某一子句头匹配,这就是运用归结原理中的合一的过程。因此逻辑程序的执行过程也就可以看成是定理证明过程,其中解释程序起定理证明器或问题求解器的作用。