A completeness result for allowed semi-strict programs with respect to well-behaved and allowed query clauses (Q1193863)

The use of 3-valued logic leads to a good approximation of the intended meaning of a logic program. In [Signed data dependencies in logic programs, J. Logic Program. 7, 231-245 (1989)], \textit{K. Kunen} proved that completeness of SLDNF-resolution and NAF-rule holds (in a 3-valued setting) for any allowed program and any allowed query clause. Moreover, every 3-valued completeness result can be 2-valued rephrased whenever we deal with a class of logic programs for which the 3-valued and the 2- valued logical consequence coincide on sentences of the form \(\forall\varphi\) and \(\neg\exists\varphi\), where \(\varphi\) is a finite conjunction of literals. A condition under which the above situation holds is strictness. Strictness enables Kunen to improve the 2-valued completeness theorem [On the completeness of SLDNF-resolution, Technical Rep. 88/17, Dep. of Comput. Sci., Univ. of Melbourne (1988)], \textit{L. Cavedon} by dropping the additional hypothesis of stratification of the program. We notice that neither strictness implies stratification nor vice versa, as can be easily proved. The purpose of this paper is to give a sufficient condition (well- behavedness) which the atoms which violate strictness in a semi-strict and allowed program must satisfy in order to ensure completeness of SLDNF-refutation and NAF-rule with respect to 2-valued logic.