Isar - Intelligible semi-automated
Theorem proving system supporting both interactive proof development
and some degree of automation have become quite successful in sizable
applications in recent years (e.g. Isabelle/Bali or VerifiCard). Typical
examples of this kind of semi-automated reasoning systems
PVS, HOL, and
Despite this success in actually formalizing parts of mathematics and
computer science, there are still obstacles in addressing a broad
range of people. Paradoxically, none of the existing semi-automated
reasoning systems have an adequate primary notion of proof
that is amenable to human understanding (for communication, or just
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
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.
- 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.
- 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,
© Springer, 2001.
- 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,
- Florian Kammüller and Markus Wenzel and Lawrence C. Paulson.
- 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.
- Tobias Nipkow. Structured
Proofs in Isar/HOL. In Types for Proofs and Programs (TYPES
2002), LNCS 2646, 2003.
- 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
- 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.
version (covers Isabelle99-2), unofficial
version (covers Isabelle2002).
- Markus Wenzel and Free Wiedijk. A
comparison of the mathematical proof languages Mizar and
Isar. In Journal of Automated Reasoning 29,
- Markus Wenzel. The
Isabelle/Isar Reference Manual. Part of the Isabelle
distribution. TU München, October 2005.
- Markus Wenzel. Using Axiomatic
Type Classes in Isabelle. Part of the Isabelle
distribution. TU München, October 2005.
- Markus Wenzel.
Some aspects of Unix file-system security. Isabelle/Isar
proof document, TU München, October 2005.
- Markus Wenzel and Larry Paulson. Isabelle/Isar. In Freek
Wiedijk, editor, The Seventeen Provers of the World.
Springer LNCS 3600, 2006.
- 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, ©
- 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.
- Isabelle/Isar: from Primitive Natural
Deduction to Structured Mathematical Reasoning, June 2005.