 |
Short history of calculational logic |
| Teaching OO using Java |
| Calculational logic |
| festive occasions |
| ABC book |
| CS Faculty over the years |
| CS@Cornell |
| The Triple-I Administration |
| How Bush Operated |
Calculational logic was developed over the years (beginning in the early 1980's) by researchers in the formal development of programs, who felt a need for an effective style of manipulation, of calculation. Involved were people like Roland Backhouse, Edsger W. Dijkstra, Wim H.J. Feijen, David Gries, Carel S. Scholten, and Netty van Gasteren. Wim Feijen is responsible for important details of the proof format.
The axioms are similar to those use by Dijkstra and Scholten in their monograph Predicate calculus and program semantics (Springer Verlag, 1990), but our order of presentation is slightly different.
In their monograph, Dijkstra and Scholten use the three inference rules Leibniz, Substitution, and Transitivity. However, Dijkstra/Scholten system is not a logic, as logicians use the word. Some of their manipulations are based on the meanings of the terms involved, and not on clearly presented syntactical rules of manipulation.
The first attempt at making a real logic out of it
appeared in A Logical
Approach to Discrete Math. However, inference rule Equanimity is missing
there, and the definition of theorem is contorted to account for it. The
introduction of Equanimity and its use in the proof format is due to Gries
and Schneider. It is used, for example, in the proofs
of soundness and completeness, and it will appear in the second edition
of A Logical Approach
to Discrete Math.