霍恩子句

（计算机术语）

霍恩子句，在数理逻辑中，霍恩子句（Horn Clause）是带有最多一个肯定文字的子句(文字的析取)。霍恩子句得名于逻辑学家Alfred Horn，他在 1951 年首先在文章《On sentences which are true of direct unions of algebras》， Journal of Symbolic Logic， 16， 14-21 中指出这种子句的重要性。