The logic of U • (TP)2

Abstract

U • (TP)2 is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and "programs as predicates" style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He onwards. In this paper we focus on the underlying logic of the prover, emphasising those aspects that are tailored to support the style of proof so often used for UTP foundational work. These aspects include support for alphabets, type-inferencing, explicit substitution notation, and explicit meta-notation for general variable-binding lists in quantifiers. The need for these features is illustrated by a running example that develops a theory of UTP designs. We finish with a discussion of issues regarding the soundness of the proof tool, and linkages to existing "industrial strength" provers such as Isabelle, PVS or CoQ. © Springer-Verlag 2013.