Horn clause

Summary

A Horn clause is a disjunction of literals in which at most one literal is unnegated. Such a clause can be read as a rule: "if all of these hold, then that holds". With no unnegated literal, it is a constraint: "these do not all hold". Satisfiability of a conjunctive normal form made of Horn clauses can be decided in polynomial time, unlike general satisfiability. Horn clauses are the basis of logic programming, and their first-order universal forms axiomatize universal Horn classes and quasivarieties.