A Horn clause is a logical formula of the form
where the 's and are literals.
Horn clauses are traditionally written the other way around, i.e.
Horn clauses are of central importance in logic programming.
If , i.e. there are no 's, then the clause is of the form
(where is truth).
This is referred to as a fact or ground truth, as it forces to be true.
If (where is falsity), then the clause is of the form
This is referred to as a goal. This is because Horn clauses are usually used with proof systems that are refutation complete, such as resolution. Such systems are able to prove from a set of contradictory clauses, if such a thing is possible.
We can add a goal clause to a set of clauses, and then try to find a proof of . Then, if we find one, we must have proved all the 's in the process.
Horn clauses were introduced by Alfred Horn in a 1951 JSL paper:
Horn, Alfred. “On Sentences Which Are True of Direct Unions of Algebras.” Journal of Symbolic Logic 16, no. 1 (1951): 14–21. doi:10.2307/2268661.
@article{horn_1951,
title = {On sentences which are true of direct unions of algebras},
volume = {16},
doi = {10.2307/2268661},
number = {1},
journal = {Journal of Symbolic Logic},
publisher = {Cambridge University Press},
author = {Horn, Alfred},
year = {1951},
pages = {14–21}
}