Synopsis for programmers

The theoretical results in this paper show you can establish that a program

1. returns no wrong answers, and
2. misses no answers in all solutions computations which terminate normally,

using the following verification method:

1. You must decide whether each ground atomic goal is true (should succeed), false (should fail) or inadmissible (should not occur; any behaviour is acceptable).
2. For each true atom there must be a ground matching clause instance with a true body (all conjuncts are true).
3. For each false atom, all ground matching clause instances must have false bodies (at least one conjunct is false).

Note that separate reasoning must be used to show the program terminates normally (answers may be missed due to non-termination or runtime errors). Also, there are several assumptions about the program/system:

1. Only ``pure'' Prolog is used -- there are no uses of cut, var/1, et cetera.
2. Negated calls are ground when they are selected (this is checked at runtime or compile time in some logic programming systems; others provide no support for checking).
3. The execution doesn't violate the ``occurs check'' (again, some systems provide support for this but most do not -- occurs check violations are very rare).