Logic Program Derivation for a Class of First Order Logic Relations

Abstract

Logic programming has been an attempt to bridge the gap betwen 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 some mechanical tools have been developed to assist in covering this distance, no fully automatic system for this purpose is yet known. In this paper v/t 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.