博文
霍恩（Alfred Horn）与霍恩子句（Horn Clause）
||
1. 霍恩
霍恩（Alfred Horn 1918-2001），美国逻辑学家，因其在格子理论和通用代数方面的工作而闻名。他在1951年发表的论文“On sentences which are true of direct unions of algebras”描述了Horn子句和Horn句子，后来成为逻辑编程的基础。
霍恩出生在曼哈顿下东城，父母都是聋哑人，父亲在霍恩三岁的时候去世，由祖父母的大家庭抚养长大。霍恩就读于纽约市立学院，后来在纽约大学获得了数学硕士学位，在加利福尼亚大学伯克利分校获得博士学位，然后他开始在加州大学洛杉矶分校工作，直到1988年退休。
2，霍恩子句（Horn Clause）
在数理逻辑中，霍恩子句是带有最多一个肯定文字的子句（文字的析取），由逻辑学家霍恩在 1951 年的文章《On sentences which are true of direct unions of algebras》中指出这种子句的重要性。
有且只有一个肯定文字的霍恩子句叫做明确子句，只有一个肯定文字的霍恩子句叫做事实，没有任何肯定文字的霍恩子句叫做目标子句：
霍恩子句类型 | 析取式 | 蕴含式 | 解读 |
明确子句 | ¬p ∨ ¬q ∨ ... ∨ ¬t ∨ u | p ∧ q ∧ ... ∧ t → u | 如果p，q…t成立，那么u也成立 |
事实 | u | true → u | u 成立 |
目标子句 | ¬p ∨ ¬q ∨ ... ∨ ¬t | p ∧ q ∧ ... ∧ t →false | 证明p，q…t都成立 |
霍恩子句的合取是合取范式，也叫做霍恩公式。霍恩子句在逻辑编程中扮演基本角色并且在构造性逻辑中很重要。
参考文献：
https://en.wikipedia.org/wiki/Horn_clause
https://blog.sciencenet.cn/blog-2322490-1367252.html
上一篇：什么是“理论”？
下一篇：[转载]“丝绸之路” - 世界文化遗产
