Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

On the Desirability of Mechanizing Calculational Proofs

Panagiotis Manolios and J Strother Moore.
IPL, 2001.


Dijkstra argues that calculational proofs are preferable to traditional pictorial and/or verbal proofs. First, due to the calculational proof format, incorrect proofs are less likely. Second, syntactic considerations (letting the ``symbols do the work'') have led to an impressive array of techniques for elegant proof construction. However, calculational proofs are not formal and are not flawless. Why not make them formal and check them mechanically?

Gzipped Postscript (65K)