There are lot of applications of Horn clauses (notable examples include use of rules in cognitive architectures and knowledge bases, as well as use of rules in business rules programs). Are there formal methods that can help specify and verify Horn clauses. Is there semantics of Horn clauses. One can perceive Horn clauses as something similar to programming code of traditional programming languages and therefore one can expect the denotation, operational and similar semantics as well for Horn clauses.
You should have a look at Uniform Proofs as a Foudation for Logic Programming by Dale Miller, Gopalan Nadathur, Frank Pfenning and Andre Scedrov, 1991. The idea of this work and the rich area that has seen spawn from these ideas is to understand the execution of a logic program as proof search in simple and expressive logics, such as intuitionistic logic or linear logic. A particular class of formulas with good proof search properties are the Hereditary Harrop Formulas, which nicely generalize Horn Clauses.