First-order theories for pure Prolog programs with negation (Q1892097)

The paper is the extended version of that one which appeared in the proceedings of the Ninth Symposium on Logic in Computer Science (1994). It introduces a new form of completion, called \(\ell\)-completion, which provides a sound and complete axiomatization of the Prolog depth-first strategy under some natural conditions. A method based on \(\ell\)- completion is then investigated to prove termination and equivalence of (pure) Prolog programs with negation. The basic idea is to use three operators \(S\), \(F\) and \(T\) to construct first order formulas \(SG\), \(FG\) and \(TG\) expressing success, failure and (universal) termination of the goal \(G\), respectively. Given a program \(P\), the \(\ell\)-completion is obtained as the first order theory axiomatized by some axioms for the previous operators together with CET (Clark equality theory) and some formulas derived from \(P\). The main result then shows that a goal \(G\) succeeds (resp. fails) under Prolog resolution in the program \(P\) iff \(SG\) (resp. \(FG)\) is provable from the \(\ell\)-completion (some conditions are needed for the ``if'' part). The paper is accurate and clear, and the results obtained are certain relevant. In particular, they furnish a logical semantics for Prolog which is much more elegant than many other existing semantics based on ad-hoc, often very complicate, constructions.