We discuss the general concept of calculational reasoning within Isabelle/Isar, which provides a framework for high-level natural deduction proofs that may be written in a human-readable fashion. Setting out from a few basic logical concepts of the underlying meta-logical framework of Isabelle, such as higher-order unification and resolution, calculational commands are added to the basic Isar proof language in a flexible and non-intrusive manner. Thus calculational proof style may be combined with the remaining natural deduction proof language in a liberal manner, resulting in many useful proof patterns. A case-study on formalizing Computational Tree Logic (CTL) in simply-typed set-theory demonstrates common calculational idioms in practice.
CITATION STYLE
Bauer, G., & Wenzel, M. (2001). Calculational reasoning revisited: An isabelle/isar experience. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 75–90). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_7
Mendeley helps you to discover research relevant for your work.