Deriving and Applying Logic Program Transformers

We present a methodology for logic program development based on the use of verified transformation templates. We use the Isabelle Logical Framework to formalize transformation templates as inference rules. We derive these rules in higher-order logic and afterwards use higher-order unification to apply them to develop programs in a deductive synthesis style. Our work addresses the pragmatics of template formalization and application as well as which theories and semantics of programs and data we require to derive templates. Key words: program transformation, logic programs, higher-order unification, logical frameworks. 1 Introduction We investigate the transformation of logic programs based on the use of transformation templates which formalize equivalences between schemata representing logic programs. Our focus and contributions center on three problems: 1. How may we acquire and formalize useful templates? 2. What foundations are appropriate for formally demonstrating the correctn..