The logician Alfred Horn first recognized the importance of Horn clauses in 1951. Horn clauses are a type of logical formula used in logic programming, formal specification, universal algebra, and model theory due to their helpful qualities in these areas and others. 

Types of Horn Clauses :

• Definite clause / Strict Horn clause – It has precisely one positive literal.
• Unit clause - Definite clause containing no negative literals.
• Goal clause – Horn clause lacking a literal positive.

Horn clauses perform a fundamental role in both constructive and computational logic. 

Quantifiers

In Datalog, rules are represented as Horn clauses, a restricted form of clauses in which a clause may contain no more than one literal. The following quantifiers may be used in a formula:

• Universal quantifier – It can be interpreted as "For all x, P(x) holds", which means that P(x) is true for every x-object in the universe. For instance, every lorry has wheels.
• Existential quantifier – It can be interpreted as follows: "There exists an x such that P(x)", which means that P(x) is true for at least one object x in the universe. For instance, somebody cares about you.

Computational complexity

Computational complexity is also interested in propositional Horn clauses. HORNSAT refers to the problem of discovering truth-value assignments that make a conjunction of propositional Horn clauses true. This problem is P-complete and linearly solvable. Note that the issue of unrestricted Boolean satisfiability is NP-complete.

Quasi-identities 

In universal algebra, "quasi-identities" is commonly used to denote definite Horn clauses. Sets of quasi-identities that define classes of algebras are known as quasivarieties. These quasivarieties have certain advantageous qualities with varieties, which are equational classes that impose more stringent restrictions.

Horn sentences are significant from a model-theoretic standpoint because they are identical (up to logical equivalence) to sentences preserved under reduced products; in particular, they are preserved under direct products. Alternatively, some sentences are not Horn but are preserved under arbitrary direct products.

Solving the problem entails deriving a contradiction symbolized by the vacant clause (or "false"). The solution to the problem is substituting terms for the variables in the objective clause, which can be derived from the contradiction proof. In this context, goal clauses are analogous to conjunctive queries in relational databases, and the computational capacity of Horn clause logic is equivalent to that of a universal Turing machine.

Prolog notation

The notation employed in Prolog exhibits ambiguity, and there is also occasional ambiguity in the usage of the phrase "goal clause." The variables within a goal clause have the potential to be interpreted with either universal or existential quantification. The derivation of "false" can be seen in two ways: as the derivation of a contradiction or as the derivation of a successful solution to the problem.

Van Emden and Kowalski (1976) showed that each set D of definite clauses D has a unique minimum model M in logic programming.

A formula atomic A is implied logically by D if and only if A is true in M. P, represented by an existentially quantified conjunction of positive literals, is logically indicated by D if and only if P is true in M. Furthermore, the stable model semantics of logic programs are based on the minimal model semantics of Horn clauses.

Image source: Unsplash