霍恩条款

在数理逻辑和逻辑编程中，霍恩条款是一个具有特殊规则形式的逻辑公式，使其具有用于逻辑编程、形式化规范和模型理论的有用属性。霍恩条款是以逻辑学家阿尔弗雷德-霍恩命名的，他在1951年首次指出了其重要性。

霍恩子句是一个最多只有一个正字，即无字的子句（字数的二元连接）。反过来说，一个最多只有一个被否定的字词的字词连接被称为双角句。一个正好有一个正字的Horn子句是一个定语从句或严格的Horn子句；一个没有负字的定语从句是一个单元子句，一个没有变量的单元子句是一个事实；一个没有正字的Horn子句是一个目标子句。注意，没有字的空子句（相当于假）是一个目标子句。这三种Horn子句在下面的命题例子中得到说明。一个子句中的所有变量都被隐含地普遍量化了，其范围是整个子句。因此，举例来说。

霍恩条款在构造逻辑和计算逻辑中起着基本作用。它们在一阶解析的自动定理证明中很重要，因为两个霍恩子句的解析器本身就是一个霍恩子句，而一个目标子句和一个确定子句的解析器就是一个目标子句。霍恩子句的这些特性可以使证明一个定理的效率更高：目标子句是这个定理的否定句；见上表中的目标子句。直观地说，如果我们想证明φ，我们假设¬φ（目标），并检查这种假设是否导致矛盾。如果是，那么φ就一定成立。这样，一个机械证明工具只需要维护一套公式（假设），而不是两套（假设和（子）目标）。命题霍恩条款在计算复杂性方面也很有意义。寻找真值分配以使命题霍恩条款的结合体为真，这个问题被称为HORNSAT。这个问题是P完备的，可以在线性时间内解决。请注意，无限制的布尔可满足性问题是一个NP完备的问题。

霍恩条款也是逻辑编程的基础，在逻辑编程中，常见的是以暗示的形式写定语。(p∧q∧...∧t)→u事实上，用定语从句解析目标从句以产生一个新的目标从句是SLD解析推理规则的基础，在逻辑编程语言Prolog的实现中使用。在逻辑编程中，定语从句表现为一个目标还原过程。例如，上面写的Horn条款的行为是这样的程序。以显示u，显示p和显示q以及...和显示t。为了强调该子句的这种反向使用，它经常被写成反向形式。在逻辑编程中，计算和查询的评估是通过把要解决的问题的负数表示为一个目标句来进行的。例如，解决正字词的存在性量化联结的问题。∃X(p∧q∧...∧t)是通过否定这个问题（否认它有一个解决方案），并以目标句的逻辑等价形式来表示它。解决这个问题相当于导出一个矛盾，这个矛盾由空句（或假句）表示。

问题的解决是目标句中变量的替换，可以从矛盾的证明中提取。以这种方式使用，目标子句类似于关系数据库中的共轭查询，而霍恩子句逻辑在计算能力上等同于通用图灵机。Prolog的符号实际上是模棱两可的，"目标句"这个词有时也被模棱两可地使用。目标子句中的变量可以被理解为普遍的或存在的量化，推导出"假"可以被解释为推导出一个矛盾，也可以被解释为推导出一个待解决的问题的成功方案。VanEmden和Kowalski(1976)在逻辑编程的背景下研究了Horn条款的模型理论特性，表明每一组定语D都有一个xxx的最小模型M。一个原子式A在逻辑上被D暗示，当且仅当A在M中为真。由此可见，当且仅当P在M中为真时，由存在量化的正字连词表示的问题P在逻辑上被D隐含。Horn条款的最小模型语义是逻辑程序稳定模型语义的基础。