In formal logic, Horn-satisfiability is the problem of deciding whether a given set of Horn clauses is satisfiable or not.
A Horn clause is a clause with at most one positive literal (called the head of the clause). Negative literals, if any, are called the body of the clause. A Horn formula is a propositional formula formed by ANDing Horn clauses.
See also
