A Horn clause is a disjunction of literals containing at most one positive literal. It can be read as an implication whose antecedent is a conjunction of variables.
Horn-SAT asks whether a conjunction of Horn clauses is satisfiable.
The Horn-SAT forward-chaining algorithm starts with every variable false and repeatedly makes the conclusion of any enabled implication true. It reports failure if it enables a clause with no positive conclusion; otherwise the fixed point is the least satisfying assignment.
Articles by others on the same topic
A Horn clause is a special type of logical expression used in propositional logic and predicate logic that has important applications in computer science, particularly in logic programming and automated theorem proving. A Horn clause is defined as a disjunction of literals (which can be either a positive or negative atomic proposition) with at most one positive literal.