Logic Programming and the Refinement Calculus: Semantics Based ProgramTransformations

摘要

An attempt to bridge the gap between logic programming and a refinement calculusfor imperative programs is made. In order to make an embedding of logic progamming possible, the refinement calculus is extended in several ways. The result is a notion of stepwise refinement for logic programs and the advantages of the refinement calculus become available for logic programing. For example, program transformation rules for logic programming in the calculus can be justified.