We propose a generalization of the Miller's definition of abstract
logic programming language. The new definition keeps in account the
fact that computing in logic languages is a process of searching for
proofs that gives a result: it can be a correct answer, a call
pattern, a resultant, according to the observable we are interested
in. In the meanwhile, we provide a fixpoint semantics for sequent
calculi and we show that our generalization of completeness of
uniform proofs corresponds to particular compositionality properties
of the semantics. Hereditarily Harrop formulas are used trough the
paper as a working example.