Intelligible semi-automatic reasoning in December 2015

A presentation on old and new aspects of Isabelle/Isar will happen 04-Dec-2015 10:00 at Univ. Bonn (Workgroup of Prof. Koepke). See also the web page of Oberseminar mathematische Logik.


Isabelle was introduced in 1989 (by L. Paulson) as a generic logical framework for higher-order natural deduction. Intelligible semi-automated reasoning (Isar) was introduced in 1999 (by M. Wenzel) as a structured proof language for human-readable formal proof documents. Today, in December 2015, we see large applications of Isabelle/Isar in the Isabelle/HOL object-logic, e.g. in the Archive of Formal Proofs with more than 240 entries.

After so many years, development of Isar is still not finished. Recent refinements of old concepts and additions of new concepts include: structured rule statements (Eigen-contexts), multi-branch elimination (case-splitting), structured backwards refinement. The new Eisbach language (by D. Matichuk et al) allows to define complex proof methods in their usual syntax, instead of traditional Isabelle/ML. Sledgehammer (by J. Blanchette et al) allows to generate semi-intelligible Isar proofs from machine-generated proofs (via external ATPs and SMTs).

The ultimate aim of Isabelle/Isar is to turn the results of formal proof production into mathematical documents with nice type-setting. Document source was mainly written in LaTeX in the past, but is now moving towards Markdown, with specific GUI support in the Prover IDE (Isabelle/jEdit).

The Slides are available.

Isabelle Tutorial at Bonn

A tutorial on Isabelle for students of mathematics will happen 03/04-Dec-2015 at Univ. Bonn (Workgroup of Prof. Koepke). The detailed schedule is available on the web page of Praktikum Mathematische Logik. The main language of the tutorial is German; materials are in English.

Notable topics

  • Isabelle/Pure as logical framework for Natural Deduction
  • Isabelle/Isar as proof language for formalized mathematics
  • Isabelle/ML as environment for developing tools for logic applications (including Prover IDE support)


The tutorial uses the following snapshot of the emerging winter release: Isabelle_01-Dec-2015.

Moreover, a full installation of LaTeX is required (Linux: TeX Live via package manager, Windows: MiKTeX, Mac OS X: MacTeX).