Protected completions of first-order general logic programs

Minker and Perlis [15] have made the important observation that in certain circumstances, it might be desirable to prevent the inference of {top right corner}A when A is in the finite failure set of a logic program P. In this paper, we investigate the model-theoretic aspects of their proposal and develop a Fitting-style [5] declarative semantics for protected completions of general logic programs (containing function symbols). This extends the Minker-Perlis proposal which applies to function-free pure logic programs. In addition, an operational semantics is proposed and it is proven to be sound for existentially quantified positive queries and negative ground queries to general, canonical protected logic programs. Completeness issues are investigated and completeness is proved for positive existential queries and negative ground queries for the following classes of programs: (1) function-free general protected logic programs (the Minker-Perlis operational semantics apply to function-free pure protected logic programs), (2) pure protected logic programs (with function symbols) and (3) protected general logic programs that do not contain any internal variables (though they may contain function symbols).