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.
Articles by others on the same topic
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.