Short answers, pulled from the story.
Horn clauses are named for logician Alfred Horn, who first pointed out their significance in 1951. The name honors his identification of this particular family of logical formulas and the properties that make them useful.
A Horn clause is a disjunctive clause, meaning a disjunction of literals, with at most one positive (unnegated) literal. Subtypes include definite clauses (exactly one positive literal), facts (a definite clause with no negative literals), and goal clauses (no positive literal).
HORNSAT is the problem of finding truth-value assignments to make a conjunction of propositional Horn clauses true. It is P-complete and solvable in linear time, making it far more tractable than the unrestricted Boolean satisfiability problem, which is NP-complete.
Prolog is built on Horn clause logic. Definite clauses in Prolog are written in the form "u :- p, q,..., t.", and the SLD resolution inference rule, which is the basis of Prolog's implementation, operates by resolving a goal clause with a definite clause to produce a new goal clause.
Van Emden and Kowalski showed in 1976 that every set of definite clauses D has a unique minimal model M, and that an atomic formula A is logically implied by D if and only if A is true in M. This minimal model semantics later became the basis for the stable model semantics of logic programs.
In universal algebra, definite Horn clauses are called quasi-identities. Classes of algebras definable by a set of quasi-identities are called quasivarieties, and they share some of the good properties of the more restrictive notion of a variety, which is an equational class.