Semantics for Logic Programs without Occur Check

摘要

A semantics of Prolog without occur check is introduced, by considering circular bindings (x/f(x)) as recursive equations (x=f(x)). The resolution, i.e., SLD-resolution without occur check, is referred to as CSLD-resolution. Important theorems such as soundness and completeness of CSLD-resolution are established. The finite failure set turns out to be precisely the complement of the greatest fixed point of a monotonic mapping on the complete Herbrand base. Soundness and completeness of the negation as failure rule can be obtained in this setting.