Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R.J. Back, J. Grundy, and J. von Wright. Structured calculational proof. Formal Aspects of Computing, 9, 1997.
R.J. Back and J. von Wright. Structured derivations: A method for doing highschool mathematics carefully. Technical report, Turku Centre for C.S., 1999.
G. Bauer and M. Wenzel. Computer-assisted mathematics at work — the Hahn-Banach theorem in Isabelle/Isar. In T. Coquand, P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs: TYPES’99, LNCS, 2000.
Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors. Theorem Proving in Higher Order Logics: TPHOLs’ 99, LNCS 1690, 1999.
E.W. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics Texts and monographs in computer science. Springer, 1990.
G. Gentzen. Untersuchungen über das logische Schlieβen. Mathematische Zeitschrift, 1935.
J. Grundy. Window inference in the HOL system. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors, Proceedings of the International Workshop on HOL. ACM SIGDA, IEEE Computer Society Press, 1991.
J. Harrison. A Mizar mode for HOL. In J. Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: TPHOLs’ 96, LNCS 1125, 1997.
K. McMillan. Lecture notes on verification of digital and hybrid systems. NATO summer school, http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html.
K. McMillan. Symbolic Model Checking: an approach to the state explosion problem. PhD thesis, Carnegie Mellon University, 1992.
Mizar mathematical library. http://www.mizar.org/library/.
M. Muzalewski. An Outline of PC Mizar. Fondation of Logic, Mathematics and Informatics — Mizar Users Group, 1993.
L.C. Paulson. Isabelle: A Generic Theorem Prover. LNCS 828. 1994.
M. Simons. Proof presentation for Isabelle. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs’ 97, LNCS 1275, 1997.
D. Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, 1997.
D. Syme. Three tactic theorem proving. In G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors. Theorem Proving in Higher Order Logics: TPHOLs’ 99, LNCS 1690, 1999. Bertot et al. [4]}.
A. Trybulec. Some features of the Mizar language. Presented at a workshop in Turin, Italy, 1993.
R. Verhoeven and R. Backhouse. Interfacing program construction and verification. In J. Wing and J. Woodcock, editors, FM99: The World Congress in Formal Methods, volume 1708 and 1709 of LNCS, 1999.
M. Wenzel. Isar — a generic interpretative approach to readable formal proof documents. In G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors. Theorem Proving in Higher Order Logics: TPHOLs’ 99, LNCS 1690, 1999. Bertot et al. [4]}.
M. Wenzel. The Isabelle/Isar Reference Manual, 2000. Part of the Isabelle distribution, http://isabelle.in.tum.de/doc/isar-ref.pdf.
M. Wenzel. Some aspects of Unix file-system security. Isabelle/Isar proof document, http://isabelle.in.tum.de/library/HOL/Unix/document.pdf, 2001.
F. Wiedijk. Mizar: An impression. Unpublished paper, 1999. http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz.
V. Zammit. On the implementation of an extensible declarative proof language. In G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors. Theorem Proving in Higher Order Logics: TPHOLs’ 99, LNCS 1690, 1999. Bertot et al. [4]}.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bauer, G., Wenzel, M. (2001). Calculational Reasoning Revisited An Isabelle/Isar Experience. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_7
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive