On the Desirability of Mechanizing Calculational Proofs

---

Panagiotis Manolios and J Strother Moore.
IPL, 2001.

Abstract

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)