Horn Clause

In logic, Horn clauses are a class of logical formulas that take the form of an implication of a conjunction of positive literals.

Definition

Fix a family of primitive predicates $P_i:A_i\to \mathbf{Prop}$ for all $i:I$.

For any set $X$, an atom over $X$ is given by an index $i:I$ and a function $f:X\to A_i.$

It denotes the proposition-valued predicate
$x\mapsto P_i(f(x)).$

So an atom over $X$ is a predicate on $X$ obtained by pulling back one of the primitive predicates along a map $X\to A_i$.

Then a generalized Horn clause over $X$ (relative to $\{P_i{\}}_{i:I}$)is either

$$\left(\underset{j:J}{\bigwedge }{Q}_j(x)\right)\to R(x)$$

where each $Q_j,R:X\to \mathbf{Prop}$ is an atom over $X$, or

$$\left(\underset{j:J}{\bigwedge }{Q}_j(x)\right)\to \perp .$$

In the case that $J$ is finite, then we have a Horn clause over $X$ (in a non-generalized sense).

Remarks

A classical Horn clause is typically written as a disjunction with at most one positive variable, however the implication form and the disjunction form diverge outside of classical settings. The simplest case is given below. The right hand side is a tautology

$$P\vee \neg P/⟺P\to P$$