# horn-clause

## Horn clause

[https://en.wikipedia.org/wiki/Horn\_clause](https://en.wikipedia.org/wiki/Horn_clause)

A Horn clause is a logical formula of a particular rule-like form, which gives it useful properties for use in logic programming, formal specification, and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.

Horn clauses

* Horn clause: disjunction of at most one positive (non-negated) literal
* Dual-Horn clause: at most one negated literal
* Strict Horn (definite) clause: exactly one positive literal
  * Unit clause: a Definite clause with no negative literals
    * Fact: a Unit clause without variables
* Goal clause: a Horn clause without positive literals
  * Empty clause: a Goal clause without literals
* **Horn clause** is a clause, i.e. a disjunction of literals, with at most one positive (non-negated) literal.
* **Dual-Horn clause** is a disjunction of literals with at most one negated literal.
* **Definite clause** or **Strict Horn clause** is a A Horn clause with exactly one positive literal.
* _Unit clause_ is a definite clause with no negative literals.
* _Fact_ is a unit clause without variables.
* **Goal clause** is a Horn clause without a positive literal.
* _The empty clause_ is a goal clause without literals (false :- ...)

Propositional examples of the 3 kinds of Horn clauses

* Disjunctive form
  * Definite: `(¬p₁ ∨ ¬p₂ ∨ … ∨ ¬pₙ) ∨ u`   or  `u ∨ (⋁ ¬pᵢ)`
  * Fact:                             `u`   or  `u`
  * Goal:     `(¬p₁ ∨ ¬p₂ ∨ … ∨ ¬pₙ)`        or      `⋁ ¬pᵢ`
* Implication form:
  * Definite: `u <- (p₁ ∧ p₂ ∧ … ∧ pₙ)`     or `u <- ⋀ pᵢ`
  * Fact:     `u`                          or  `u`
  * Goal: `false <- (p₁ ∧ p₂ ∧ … ∧ pₙ)`    or  `⊥ <- ⋀ pᵢ`

## Horn clause

* A _clause_ is a disjunction of literals.
* _Horn clause_ is a clause having at most 1 positive (non-negated) literal.
* _Dual-Horn clause_ is a clause having at most 1 negated literal.
* _Strict (definite) Horn clause_ has exactly 1 positive literal.
* _Unit clause_ is a definite clause without negative literals.
* A _fact_ is a unit clause without variables.
* A _goal_ is a Horn clause without a positive literal (goal clause is the empty clause without literals).

| clause   | Disjunction form       | Implication form        | Read as |
| -------- | ---------------------- | ----------------------- | ------- |
| Definite | ¬p ∨ ¬q ∨ ... ∨ ¬t ∨ u | u ← p ∧ q ∧ ... ∧ t     | (1)     |
| Fact     | u                      | u                       | (2)     |
| Goal     | ¬p ∨ ¬q ∨ ... ∨ ¬t     | false ← p ∧ q ∧ ... ∧ t | (3)     |

(1) assume that, if p and q and ... and t all hold, then u also holds (2) assume that u holds (3) show that p and q and ... and t all hold

Horn clause logic is equivalent in computational power to a universal Turing machine.
