We propose a categorical framework which formalizes and extends the
syntax, operational semantics and declarative model theory of a broad
range of logic programming languages. A program is interpreted in an
indexed category in such a way that the base category contains all the
possible states which can occur during the execution of the program
(such as global constraints or type information), while each fiber
encodes the logic at each state.
 
  We define appropriate notions of categorical resolution and models,
and we prove the related correctness and completeness properties.