Horn clause
- A horn clause is a clause (a disjunction of literals) with at most one positive.
- Definite clause: Horn clauses with exactly one positive literal.
- Fact: Definite clauses without negative literals.
| Name | Disjunction form | Implication form | Read intuitively as |
|---|---|---|---|
| Definite clause | ¬p ∨ ¬q ∨ ... ∨ ¬t ∨ u | u ← p ∧ q ∧ ... ∧ t | assume that, if p and q and ... and t all hold, then also u holds |
| Fact | u | u | assume that u holds |
