An application of abstract interpretation of logic programs: Occur check reduction

Abstract

The occur check in Robinson unification is superfluous m most unifications that take place in practice. The present paper is concerned with the problem of determining circumstances under which the occur check may be safely dispensed with. The method given draws on one outlined by David Plaisted. The framework, however, differs in that we systematically apply the abstract interpretation principle to logic programs. The aim is to give a clear presentation and to facilitate justification of the soundness of the method.