霍恩子句

Horn子句是一个逻辑不连贯的字词，其中最多一个字词是正数，而其他字词都是负数。它是以Alfred Horn的名字命名的，他在1951年的一篇文章中描述了它们。

恰好有一个积极字面的Horn从句是定语从句；没有消极字面的定语从句有时称为"事实"；没有积极字面的Horn从句有时称为目标句。这三种Horn分句在下面的命题例子中得到了说明。

定语从句。¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg qvee \cdots \vee \neg t ∨ u}。

事实：u {/displaystyle u}。

目标句。¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \neg t}。

在非命题的情况下，一个分句中的所有变量都被隐含地统一量化，范围是整个分句。因此，例如：

¬人 ( X ) ∨凡人 ( X ) {\displaystyle {neg {text{human}}(X)\lor {text{mortal}}(X)}.

代表：

∀ X ( ¬人 ( X ) ∨凡人 ( X ) ) ){displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))}。

这在逻辑上等同于：

∀ X ( 人类 ( X ) → 凡人 ( X ) ) 。{displaystyle \forall X({text{human}}(X)\rightarrow {text{mortal}}(X)).}

Horn子句在构造逻辑和计算逻辑中起着基本的作用。它们在一阶解析的自动定理证明中非常重要，因为两个Horn子句的解析子本身就是一个Horn子句，一个目标子句和一个定语从句的解析子也是一个目标子句。Horn子句的这些特性可以使定理的证明效率更高（用目标子句的否定来表示）。

喇叭子句也是逻辑程序设计的基础，在逻辑程序设计中，通常以内涵的形式写定语从句。

( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u}。

事实上，用定语从句解析目标从句产生新的目标从句是SLD解析推理规则的基础，用于实现逻辑编程和编程语言Prolog。

在逻辑编程中，一个定语从句表现为一个目标还原过程。例如，上面写的Horn子句就表现为一个程序。

显示u {displaystyle u}，显示p {displaystyle p}和显示q {displaystyle q}和⋯ {displaystyle ⋯cdots }。并显示t {\displaystyle t} 。

为了强调这种倒装句的用法，常常写成倒装句。

u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)}。

在Prolog中，这写成。

Prolog的符号其实是有歧义的，"目标子句"这个词有时也被含糊地使用。目标子句中的变量可以理解为普遍性的，也可以理解为存在性的量化，推导出"假"既可以解释为推导出矛盾，也可以解释为推导出要解决的问题的成功解。

Van Emden和Kowalski(1976)在逻辑程序设计的背景下研究了Horn子句的模型理论特性，表明每一个定语从句集D都有一个唯一的最小模型M.一个原子式A如果且仅当A在M中为真时，就会被D逻辑地隐含，由此可见，一个由正字的存在性量化连接表示的问题P如果且仅当P在M中为真时，就会被D逻辑地隐含，Horn子句的最小模型语义是逻辑程序稳定模型语义的基础。

命题角子句在计算复杂性方面也很有意义，其中寻找真值赋值以使命题角子句的连接为真的问题是一个P-完全问题(事实上是可以在线性时间内解决的)，有时称为HORNSAT。然而非限制性布尔可满足性问题是一个NP-完全问题）。一阶Horn子句的可满足性是不可决定的。

问题和答案

按字母搜索