Semantics for logic programs without occur check

AbstractFor reasons of efficiency, in almost all implementations of Prolog the occur check is left out. This a mechanism should protect the program against introducing circular bindings of variables. In practice the occur check is very expensive, however, and it is left to the skills of the user, to avoid these circular bindings in the program. In this paper a semantics of Prolog without occur check is introduced. The new kind of resolution, i.e. SLD-resolution without occur check, is referred to as CSLD-resolution. Important theorems such as soundness and completeness of both CSLD-resolution and the “negation as failure” rule, are established