Conference Proceedings

AN APPLICATION OF ABSTRACT INTERPRETATION OF LOGIC PROGRAMS - OCCUR CHECK REDUCTION

H SONDERGAARD

LECTURE NOTES IN COMPUTER SCIENCE | SPRINGER VERLAG | Published : 1986

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.