In the field of logic languages, we try to reconcile the proof
theoretic tradition, characterized by the concept of uniform proof,
with the classic approach based on fixpoint semantics.  Hence, we
propose a treatment of sequent calculi similar in spirit to the
treatment of Horn clauses in logic programming. We have three
different semantic styles (operational, declarative, fixpoint) that
agree on the set of all the proofs for a given calculus.  Following
the guideline of abstract interpretation, it is possible
to define abstractions of the concrete semantics,
which model well known observables such as correct answers or
groundness. This should simplify the process of extending important
results obtained in the case of positive logic programs to the new
logic languages developed by proof theoretic methods. As an example
of application, we present a top-down static analyzer for properties
of groundness which works for full intuitionistic first order
logic.