Logic Programming

Abstract

In this section we show that the execution of a program can be understood as the automated deduction of the empty clause from a given unsatisfiable clause set (possibly using the resolution refinements from Section 2.6). A further concept is needed: how to generate an answer, a result of the computation, from the resolution proof. A resolution proof as such shows only that the empty clause is derivable; an answer, in a sense, explains how it is obtained. The following ideas of extracting an answer from a resolution proof have their roots in the works of Green and Kowalski.