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.

PS

Annals of Pure and Applied Logic, Vol. 113 (2002), pp. 207-224.

@article{lif01b, title={On Calculational Proofs}, author={Vladimir Lifschitz}, volume={113}, journal={Annals of Pure and Applied Logic}, pages={207-224}, url="http://www.cs.utexas.edu/users/ai-lab?lif01b", year={2002} }