Horn clause

Also known as a definite clause. A set of atomic literals with one positive literal. Usually written

	L <- L1, ..., Ln where n>=0.

If L is false the clause is regarded as a goal. Horn clauses can express a subset of statements of first order logic.