In mathematical logic and logic programming, 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. Definition A Horn clause is a clause (a disjunction of literals) with at most one positive, i.e. unnegated, literal. Conversely, a disjunction of literals with at most one negated literal is called a dual-Horn clause. A Horn clause with exactly one positive literal is a definite clause or a strict Horn clause; a definite clause with no negative literals is a unit clause, and a unit clause without variables is a fact;. A Horn clause without a positive literal is a goal clause. Note that the empty clause, consisting of no literals (which is equivalent to false) is a goal clause. These three kinds of Horn clauses are illustrated in the following propositional example: All variables in a clause are implicitly universally quantified with the scope being the entire clause. Thus, for example: ¬ human(X) ∨ mortal(X) stands for: ∀X( ¬ human(X) ∨ mortal(X) ) which is logically equivalent to: ∀X ( human(X) → mortal(X) ) Significance Horn clauses play a basic role in constructive logic and computational logic. They are important in automated theorem proving by first-order resolution, because the resolvent of two Horn clauses is itself a Horn clause, and the resolvent of a goal clause and a definite clause is a goal clause. These properties of Horn clauses can lead to greater efficiency of proving a theorem: the goal clause is the negation of this theorem; see Goal clause in the above table. Intuitively, if we wish to prove φ, we assume ¬φ (the goal) and check whether such assumption leads to a contradiction. If so, then φ must hold. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals). Propositional Horn clauses are also of interest in computational complexity. The problem of finding truth-value assignments to make a conjunction of propositional Horn clauses true is known as HORNSAT. This problem is P-complete and solvable in linear time. Note that the unrestricted Boolean satisfiability problem is an NP-complete problem. Logic programming Horn clauses are also the basis of logic programming, where it is common to