We present a semantic framework for sequent calculi which allows us to
reason about properties of proofs. Using this framework we try to
reconcile the proof theoretic approach to logic programming,
essentially based on the concept of uniform proof, with the older
model theoretic approach. Using abstract interpretation to model
abstractions of proofs, we are able to port well known results for
pure logic programming, in the field of abstract debugging and
analysis, to richer languages such as hereditary Harrop formulas.
While this approach is based on proof theory, there are cases of
languages, like CLP, where models play a fundamental role. Therefore,
we also propose a categorical semantic framework which is able to cope
with both the syntax, the operational semantics and the model theory
of a broad range of logic languages. A program is interpreted in an
indexed category such that the base category contains all the possible
states which can occur during the execution of the program (such as
global constraints or type informations), while each fiber encodes the
corresponding relevant logical properties. We define appropriate
notions of categorical resolution and models, and we prove the related
correctness and completeness properties.