Samuel's Tech Blog

The Wikipedia article on Horn clauses states the following: "Horn clauses are relevant to theorem proving by first-order resolution, in that the resolution of two Horn clauses is itself a Horn clause"

That seems to explain why horn clauses are so foundational for prolog, since in prolog one can compose goal functions as compounds of other goals.

(I realize my lack of basic knowledge of Prolog, heavily regretting not having been able to have any formal training in logic programming / prolog at my uni :( (they removed the prolog part of the course where I hoped to learn it, just before I entered that course) ).