|
Organizers |
Calculational Proofs
by
Vladimir Lifschitz
University of Texas
This paper is about the 'calculational proof format' introduced by Dijkstra and Scholten on the basis of ideas due to Feijen. Their work has had an impact on the presentation of proofs in computer science research, and even on undergraduate education in computer science. These ideas can be also viewed as an interesting discovery in logic, although this fact has so far remained largely unnoticed.
Inventing proofs of predicate formulas in a Hilbert style deduction system is known to be an unpleasant task unless one uses metamathematical tools, such as the deduction theorem. On the other hand, proving formulas in a natural deduction system is relatively easy. The role of the deduction theorem and of natural deduction is determined by the fact that they provide a mechanism for discharging assumptions. We argue, however, using the work done by Dijkstra and Scholten, that the importance of assumptions in formal proofs is overrated: with the right choice of inference rules, proving predicate formulas is easy even without introducing assumptions (and without the use of auxiliary derivable objects such as sequents).
To this end, 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 deductive system for predicate logic. Any proof tree in this system can be represented as a sequence of calculations. This fact shows that any logically valid predicate formula has a calculational proof.
Date received: February 27, 1999
Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-08.