Types and declarative static type checking in logic programming

We define a type structure for Horn clause logic, with tbe emphasis on the definition of the model theoretic semantic. The other issue which is faced in the paper is related to the static verification of type correctness. We define two operational semantics. The first one, which is shown to be equivalent to The Model Theoretic semantics, is defined in terms of dynamic type cheching. The second semantics which consists of static type cheecking and standard Horn clause operational semantics is shown to give a denotation (equivalent to the one defined by the model theoretic semantics) only to the set of statically cheeckable programs, a reasonable subset of the set of type correct programs. An interesting feature of our approach is that type cheecking simply consistists of program execution in a specific Horn clause theory, the theory of types.