Horn子句（Horn clause）是逻辑中的一个概念，它指的是一种特殊的逻辑语句，具有特定的结构。在逻辑编程和自动推理领域，Horn子句尤为重要。
Horn子句的定义如下：
1. 它是一个逻辑语句，通常写作“前提 → 结论”的形式。
2. 在这个形式中，前提可以是一个合取（AND）表达式，而结论是一个原子命题（即一个不可再分解的命题）。
3. 前提中的合取表达式中的每一个子句（即每一个逻辑“与”的部分）都只能是以下两种形式之一：
一个原子命题。
一个或多个原子命题的析取（OR）。
用更正式的符号来表示，一个Horn子句可以写作：
```
P1 ∨ P2 ∨ ... ∨ Pn → Q
```
其中，P1, P2, ..., Pn 是原子命题或它们的析取，Q 是一个原子命题。
Horn子句的例子：
```
A ∧ B → C
?A ∨ B → C
```
Horn子句在逻辑编程和自动推理中具有以下重要性质：
每个Horn子句都有唯一的析取范式（DNF），即它可以被分解为若干个原子命题的析取。
Horn子句的合取可以转换为等价的析取范式，但不是所有的析取范式都能转换为等价的Horn子句。
Horn子句在逻辑编程语言如Prolog中有着广泛的应用，因为它们可以用来表示规则，并且可以通过DPLL算法（一种用于解决Horn子句问题的算法）进行高效求解。
