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.

Abstract:

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.