Definition. Horn clauses - Syntax [004v]
Definition. Horn clauses - Syntax [004v]
A Horn clause is a disjunctive clause (disjunction of literals) with at most one positive, i.e. unnegated literal. Often written in implication form as a conjunction of literals implying some literal called the head.
\[ \underbrace {\underbrace {p(x_1, x_2) \land q(x_1, x_2, x_3) \land \ldots }_\text {queries} \land \underbrace {\phi }_\text {constraint}}_\text {body} \to \underbrace {H}_\text {head} \]Here:
- queries are relations over some vector of variables
- \(\phi \) represents a formula in a first-order theory which does not contain queries
- \(H\) is called the head and represents either a query in which case we also call the horn clause a definite class if it has the following shape \[ (p \land q \land \ldots \land \phi ) \to H \] or a fact if it has the following shape \[ \top \to H \] \(H\) can also be \(\bot \) in which case we refer to the horn clause as a gloal clause with the shape \[ (p \land q \land \ldots \land \phi ) \to \bot \] with the idea being that as opposed to assuming the query holds we now show that it holds
Free variables are implicitly universally quantified over, so a horn clause like
\[ \texttt {mortal}(X) \to \texttt {human}(X) \]stands for
\[ \forall X.\ \texttt {mortal}(X) \to \texttt {human}(X) \]