Proof theory and semantics of logic programs

The authors develop a resolution logic that is based on direct proofs rather than on proofs by refutations. The deductive system studied has clauses as its formulas and resolution as the sole inference rule. They analyze this deductive system using a novel representation of resolution proofs, called resolution graphs, and obtain a general completeness theorem: a clause is a logical consequence of a set of clauses if and only if it is either tautological or subsumed by a clause derivable from that set. In a previous paper (proc. 16th ACM Symp. on Principles of Prog. Lang., pp.134-42, 1989), the authors developed a model-theoretic compositional semantics for logic programs and investigated the fully abstract equivalences induced by various notions of composition. They continue that study here using the proof theory of resolution logic. This proof theory gives rise to various semantics for logic programs that reflect more operational details than does the model-theoretic semantics