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.