Isar - Intelligible semi-automated reasoning

The Intelligible semi-automated reasoning (Isar) approach to readable formal proof documents sets out to bridge the semantic gap between internal notions of proof given by state-of-the-art interactive theorem proving systems and an appropriate level of abstraction for user-level work. The Isar formal proof language has been designed to satisfy quite contradictory requirements, being both 'declarative' and immediately 'executable', by virtue of the Isar/VM interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings: it is based on a few basic principles only, it is quite independent of the underlying logic, and integrates a broad range of automated proof methods. Interactive proof development is supported directly as well.

The Isabelle system offers Isar as an alternative proof language interface layer, beyond traditional tactic scripts. The Isabelle/Isar system provides an interpreter for the Isar formal proof document language. Isabelle/Isar input consists either of proper document constructors, or improper auxiliary commands (for diagnostics, exploration etc.). Proof texts consisting of proper document constructors only admit a purely static reading, thus being intelligible later without requiring dynamic replay that is so typical for traditional proof scripts. Any of the Isabelle/Isar commands may be executed in single-steps, so basically the interpreter has a proof text debugger already built-in.

The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably between Isabelle-classic proof scripts and Isabelle/Isar documents. Isar is as generic as Isabelle, able to support a wide range of object-logics. The current end-user setup is mainly for Isabelle/HOL.

Together with the Isabelle/Isar instantiation of Proof General, a generic (X)Emacs interface for interactive proof assistants, we arrive at a reasonable environment for live proof document editing. Thus proof texts may be developed incrementally by issuing proper document constructors, including forward and backward tracing of partial documents; intermediate states may be inspected by diagnostic commands.

For presentation of the final outcome, Isabelle/Isar provides an integrated document preparation system based on current PDF/LaTeX hypertext technology. Thus Isabelle/Isar proof documents may be both browsed on the WWW, and printed on paper in high quality. E.g. see Miscellaneous Isabelle/Isar examples for Higher-Order Logic or Lattices and Orders in Isabelle/HOL.

Isabelle/Isar also provides a set of emulation commands and proof methods for embed traditional tactic-style proof scripts in a seamless manner. See Fundamental Properties of Lambda-calculus, for example.

Papers

1. Gertrud Bauer and Markus Wenzel. Computer-Assisted Mathematics at Work - The Hahn-Banach Theorem in Isabelle/Isar. In T. Coquand, P. Dybjer, B. Nordström, J. Smith, editors, Types for Proofs and Programs (TYPES'99). Lökeberg, Sweden. © Springer LNCS 1956, 2000.
2. Gertrud Bauer and Markus Wenzel. Calculational reasoning revisited - an Isabelle/Isar experience. In R. J. Boulton and P. B. Jackson, editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs'2001, LNCS 2152, © Springer, 2001.
3. Amine Chaieb and Makarius Wenzel. Context aware Calculation and Deduction --- Ring Equalities via Gröbner Bases in Isabelle. In M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, editors. Towards Mechanized Mathematical Assistants (CALCULEMUS 2007 and MKM 2007). © Springer LNAI 4573, 2007.
4. Florian Kammüller and Markus Wenzel and Lawrence C. Paulson. Locales - A Sectioning Concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, LNCS 1690, © Springer, 1999.
5. Tobias Nipkow. Structured Proofs in Isar/HOL. In Types for Proofs and Programs (TYPES 2002), LNCS 2646, 2003.
6. Markus Wenzel. Isar - a Generic Interpretative Approach to Readable Formal Proof Documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, LNCS 1690, © Springer, 1999. Slides available.
7. Markus Wenzel. Isabelle/Isar --- a versatile environment for human-readable formal proof documents, PhD thesis, Institut für Informatik, Technische Universität München, 2002. Official version (covers Isabelle99-2), unofficial version (covers Isabelle2002).
8. Markus Wenzel and Free Wiedijk. A comparison of the mathematical proof languages Mizar and Isar. In Journal of Automated Reasoning 29, 2002.
9. Markus Wenzel. The Isabelle/Isar Reference Manual. Part of the Isabelle distribution. TU München, October 2005.
10. Markus Wenzel. Using Axiomatic Type Classes in Isabelle. Part of the Isabelle distribution. TU München, October 2005.
11. Markus Wenzel. Some aspects of Unix file-system security. Isabelle/Isar proof document, TU München, October 2005.
12. Markus Wenzel and Larry Paulson. Isabelle/Isar. In Freek Wiedijk, editor, The Seventeen Provers of the World. Springer LNCS 3600, 2006.
13. Makarius Wenzel. Structured Induction Proofs in Isabelle/Isar. In J. Borwein and W. Farmer, editors, 5th International Conference on Mathematical Knowledge Management, MKM 2006, LNAI 4108, © Springer, 2006.
14. Makarius Wenzel. Isabelle/Isar --- a generic framework for human-readable proof documents. In R. Matuszewski and A. Zalewska, editors, From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric 10(23), University of Bialystok, 2007.

Slides

1. Isabelle/Isar: from Primitive Natural Deduction to Structured Mathematical Reasoning, June 2005.