Horn clauses form of logic: algebraic static semantics of programs

We give an algebraic static semantics far logic programs in the Horn Clauses Form of Logic. The semantics is expressed by means of set expressions derived from the static analysis of the clausal definition of programs. Static semantics is derived from a case analysis of the semantics of clauses as defined according to fixpoint semantics and the operational semantics associated to hyperresolution and instantiation rules, so that consistency between the various semantics is ensured. For each predicate a set expression is generated (pattern) which can be, in the end, computed by computing the union and intersection of sets in the set expression. A notation is introduced to represent sets of data, built by means of function, i.e data constructors. We have considered a logic language with monadic predicates and functions symbols, as a first approach to the study of static semantics for logic programs in general.