This note is about the "calculational style" of presenting proofs introduced by Dijkstra and Scholten and adopted in some books on theoretical computer science. We define the concept of a calculation, which is a formal counterpart of the idea of a calculational proof. The definition is in terms of a new formalization DS of predicate logic. Any proof tree in the system DS can be represented as a sequence of calculations. This fact shows that any logically valid predicate formula has a calculational proof.
View:
PS
Citation:
Annals of Pure and Applied Logic, Vol. 113 (2002), pp. 207-224.
Bibtex:

Vladimir Lifschitz Faculty vl [at] cs utexas edu