On the desirability of mechanizing calculational proofs
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? (C) 2001 Elsevier Science B.V. All rights reserved.
calculational proofs mechanical reasoning automatic theorem proving formal methods