Abstract interpretation based on oldt resolution

AbstractThis paper presents a unified framework for analyzing Prolog programs. The framework is based on OLDT resolution, a top-down Prolog interpreter with memo-ization. A run-time property of Prolog goals can be analyzed by executing the goals using an interpreter that is obtained by abstracting OLDT resolution according to the property. The execution never enters a nonterminating computation loop when the domain on which the abstract interpreter works is finite, and it does not waste time working on goals irrelevant to the given top-level goals. In addition, the behavior of the abstract interpreter is very close to the way human programmers usually analyze the property in their minds. The correctness and termination of the abstract interpreter are discussed as well