Proving properties of committed choice logic programs

AbstractPROLOG and its variants are based on SLD resolution, which uses “don't know” nondeterminism to explore the search space. Don't care (or committed choice) nondeterminism can be introduced by operations such as commit in Concurrent PROLOG and cut in sequential PROLOG. This prevents the whole SLD tree from being examined. The effect on completeness of programs is of major importance. This paper presents a theoretical model of guarded clauses, which exhibits don't know nondeterminism and also has a guard construct like many parallel PROLOGs. Next, we investigate proving properties concerning success and finite failure of guarded clause programs with restricted input-output modes. We present methodologies for proving completeness and weaker properties, which we call semicompleteness and failure soundness