Program synthesis in predicate logic
C. J. Hogger · 1978
Research in automatic theorem proving has led to an interpretation of predicate logic as a high-level procedural programming language. Logic 'programs' can be executed by interpreters based on the resolution principle. Logic offers a single formalism in which programs can be specified, derived and finally expressed using the same tool (theorem proving) as is used for executing them. This paper describes the derivation of logic programs from specifications written in standard logic.