The Logic of U ·(TP)2
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.
KeywordsTheorem Prover Sequential Composition Program Variable Proof Obligation Proof Assistant
Unable to display preview. Download preview PDF.
- [But12]Butterfield, A.: U. (TP) 2 reference manual (draft, ongoing). Technical report, School of Computer Science and Statistics, Trinity College Dublin (July 2012), https://www.scss.tcd.ie/Andrew.Butterfield/Saoithin/
- [GS93]Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, Berlin (1993)Google Scholar
- [HH98]Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall (1998)Google Scholar
- [Ros97]rOSCOE, A.W.: The Theory and Practise of Concurrency. Prentice-Hall, Pearson (1997); revised to 2000 and lightly revised to 2005Google Scholar
- [The08]The Coq Development Team. The coq proof assistant, reference manual, version 8.2. Technical report, INRIA, Roquencourt, France (2008)Google Scholar