Intuitively, if we wish to prove φ, we assume ¬φ (the goal) and check whether such assumption leads to a contradiction.
The problem of finding truth-value assignments to make a conjunction of propositional Horn clauses true is known as HORNSAT.
In universal algebra, definite Horn clauses are generally called quasi-identities; classes of algebras definable by a set of quasi-identities are called quasivarieties and enjoy some of the good properties of the more restrictive notion of a variety, i.e., an equational class.
On the other hand, there are sentences that are not Horn but are nevertheless preserved under arbitrary direct products.
The solution of the problem is a substitution of terms for the variables X in the top-level goal clause, which can be extracted from the resolution proof.
Van Emden and Kowalski (1976) investigated the model-theoretic properties of Horn clauses in the context of logic programming, showing that every set of definite clauses D has a unique minimal model M. An atomic formula A is logically implied by D if and only if A is true in M. It follows that a problem P represented by an existentially quantified conjunction of positive literals is logically implied by D if and only if P is true in M. The minimal model semantics of Horn clauses is the basis for the stable model semantics of logic programs.