Logic Program Derivation for a Class of First Order Logic Relations

Abstract

Logic programming has been an attempt to bridge the gap be~en specification and programming language and thus to simplify the software deve1opment process. Even though the only d,itference between a specification and a program in a 1ogic programming frame~rlc. is that of effi.ciency, there is still some conceptual distance to be covered be~en a naive, intuitively correct specification and an effi.ciently 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 raper ~ present a general class of first-order 1ogic re1ations, which is a subset of the extended Hom c1ause subset of 1ogic, for which ~ give mechanical means for deriving Hom 1ogic programs, which are guaranteed to be correct and complete with respect to the initial specifications.