On the desirability of mechanizing calculational proofs |
| |
| Affiliation: | 1. Department of Biomedical Engineering, Amirkabir University of Technology (Tehran polytechnic), Iran;2. Centre for Nonlinear Systems, Chennai Institute of Technology, Chennai, India;3. Health Technology Research Institute, Amirkabir University of Technology (Tehran polytechnic), Iran;4. Faculty of Natural Sciences and Mathematics, University of Maribor, Koroška cesta 160, 2000 Maribor, Slovenia;5. Department of Medical Research, China Medical University Hospital, China Medical University, Taichung 404332, Taiwan;6. Alma Mater Europaea, Slovenska ulica 17, 2000 Maribor, Slovenia;7. Complexity Science Hub Vienna, Josefstädterstraße 39, 1080 Vienna, Austria |
| |
| 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? |
| |
| Keywords: | |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
