Logic programming has been an attempt to bridge the gap between specification and programming language and thus to simplify the software development process. Even though the only difference between a specification and a program in a logic programming framework is that of efficiency, there is still some conceptual distance to be covered between a naive, intuitively correct specification and an efficiently executable version of it. And even though there have been developed some mechanical tools in the form of formal inferences that assist in covering this distance, no fully automatic system for this purpose is yet known. In this paper we present a general class of first-order logic relations, which is a subset of the extended Horn clause subset of logic, for which we give mechanical means for deriving Horn logic programs, which are guaranteed to be correct and complete with respect to the initial specifications.
This paper is not available online