Category Archives: Science

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.

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.

HOL4 workshop at CADE-25

The HOL4 workshop will happen on Sunday 02-Aug-2015 and Monday 03-Aug-2015 in Berlin, as an associated event of the 25th International Conference on Automated Deduction (CADE-25). The main theme are future directions and visions on HOL4 development: both users and developers are invited to participate in the discussion.

Even though I am myself not an HOL4 person, I will give a presentation about Isabelle/PIDE/jEdit as integrated development environment for Standard ML. The abstract is as follows:

After more than 7 years of development, Isabelle/PIDE/jEdit is today the standard way to interact with that particular proof assistant. In Isabelle2015 (May 2015) the TTY-based REPL and its wrapper for Proof General / Emacs have already been dismantled. This radical move might be taken as an opportunity of the HOL4 community to attract former Isabelle users who really do want to use plain TTY interaction. Or as an opportunity to discuss possibilities for HOL4 users and developers to make their own moves towards full-scale IDE support.

As a very modest start, I would like to present various possibilities of Isabelle/PIDE to operate as IDE for Standard ML, which happens to be the underlying language platform of HOL4 as well. This touches various facilities of Poly/ML that David Matthews provides specifically to tool builders: run-time compiler invocation with IDE feedback, toplevel environment management, structured toplevel printing (with markup and hyperlinks), and potentially also run-time debugging of SML (still unused in Isabelle2015).

Beyond that it is also possible to integrate any other languages that are related or unrelated to the prover platform, using PIDE libraries either on the ML or Scala side of that IDE framework.

Isabelle Tutorial at CADE-25

A full-day tutorial on Isabelle will happen Saturday 01-Aug-2015 in Berlin, as an associated event of the 25th International Conference on Automated Deduction (CADE-25). Here is some further organizational information about tutorials at CADE-25. Important materials for the tutorial are available at the bottom of this post.

More than 25 years ago, Isabelle was initiated by Larry Paulson as a logical framework for rapid prototyping of Natural-Deduction proof systems. Today, Isabelle is one of the major platforms for Interactive Theorem Proving (ITP), with notable support for automated reasoning tools (ATPs and SMTs). Isabelle/HOL is the main environment for applications; it is accompanied by the Archive of Formal Proofs (AFP) as repository for user-contributions. Isabelle supports logical tool development in Isabelle/ML and Isabelle/Scala, but it is also possible to connect external tools; this works routinely on Linux, Windows, and Mac OS X. The system presents itself to the end-user by an advanced Prover IDE: Isabelle/jEdit.

The purpose of the tutorial is to get acquainted with Isabelle, using the latest release Isabelle2015 (May 2015). Topics cover specifications in HOL, proofs in Isar, use of automated provers via Sledgehammer etc. The target audience are doctoral students or researchers with an interest in formalized reasoning, application of reasoning tools for interactive and automated proof development, maybe even with an interest to develop their own tools with/for Isabelle.

There will be presentations by Makarius Wenzel and Christian Sternagel, with hands-on tutoring and exercises done by the participants on their own computers (at least 2 cores and 4 GB memory).

Materials

More on Alexander Grothendieck

After the death of Alexander Grothendieck (13-Nov-2014) the Grothendieck Circle has recommenced its project to collect material from and about this great and unusual man. It remains to be seen how much we can understand from someone who isolated himself from the world so radically.

Book available: “All about Proofs, Proofs for All”

As a result of the APPA workshop at Vienna Summer of Logic 2014, there is now a book available with the collected contributions by the invited experts (including myself). It is edited by Bruno Woltzenlogel Paleo and David Delahaye, and is published by College Publications. Here is a copy of the abstract from it:

The development of new and improved proof systems, proof formats and proof search methods is one of the most essential goals of Logic. But what is a proof? What makes a proof better than another? How can a proof be found efficiently? How can a proof be used? Logicians from different communities usually provide radically different answers to such questions. Their principles may be folklore within their own communities but are often unknown to outsiders.

This book provides a snapshot of the current state of the art in proof search and proof production as implemented in contemporary automated reasoning tools such as SAT-solvers, SMT-solvers, first-order and higher-order automated theorem provers and proof assistants. Furthermore, various trends in proof theory, such as the calculus of inductive constructions, deduction modulo, deep inference, foundational proof certificates and cut-elimination, are surveyed; and applications of formal proofs are illustrated in the areas of cryptography, verification and mathematical proof mining.

Experts in these topics were invited to present tutorials about proofs during the Vienna Summer of Logic and the chapters in this book reflect their tutorials. Therefore, each chapter is intended to be accessible not only to experts but also to novice researchers from all fields of Logic.

My contribution to the book is a chapter on “Interactive Theorem Proving — from the perspective of Isabelle/Isar”, with the following abstract:

Interactive Theorem Proving (ITP) has a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 20–30 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of add-on tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and open-endedness in the combination of logical tools: typical interactive provers use automated provers and disprovers routinely in their portfolio.

The subsequent exposition of ITP takes Isabelle/Isar as the focal point to explain concepts of the greater “LCF family”, which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to end-users, without requiring self-assembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its architecture and extra-logical infrastructure.

The Isar aspect of Isabelle refers first to the structured language for human-readable and machine-checkable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus Isabelle/Isar provides extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its Prover IDE (PIDE).

Isabelle Tutorial at CADE-25

(See also updated version with more details.)

A full-day tutorial on Isabelle is scheduled as associated event of the 25th International Conference on Automated Deduction (CADE-25), which will take place in Berlin at the start of August 2015.

More than 25 years ago, Isabelle was initiated by Larry Paulson as a logical framework for rapid prototyping of Natural-Deduction proof systems. Today, Isabelle is one of the major platforms for Interactive Theorem Proving (ITP), with notable support for automated reasoning tools (ATPs and SMTs). Isabelle/HOL is the main environment for applications; it is accompanied by the Archive of Formal Proofs (AFP) as repository for user-contributions. Isabelle supports logical tool development in Isabelle/ML and Isabelle/Scala, but it is also possible to connect external tools; this works routinely on Linux, Windows, and Mac OS X. The system presents itself to the end-user by an advanced Prover IDE: Isabelle/jEdit.

The purpose of the tutorial is to help participants to get acquainted with Isabelle: topics will cover specifications in HOL, proofs in Isar, use of automated provers via Sledgehammer etc. The target audience are doctoral students or researchers with an interest in formalized reasoning, application of reasoning tools for interactive and automated proof development, maybe even with an interest to develop their own tools with/for Isabelle.

There will be presentations by myself and one or two colleagues, with hands-on tutoring and exercises done by the participants on their own computers (with at least 2 cores and 4 GB memory).

Further organizational details will emerge sooner or later, as summer 2015 approaches. Watch this space, as well as the main CADE-25 website.

CICM 2015 at Washington DC

The Conferences on Intelligent Computer Mathematics (CICM) — with the distinctive sub-conferences Calculemus, DML, MKM — may be seen as a gathering of fringe groups, but a very interesting one. Traditionally, it may serve as a forum for experimentation and unorthodox contributions that are difficult to publish elsewhere.

I have served several times on the PC of Calculemus or MKM, and once as PC chair of MKM. For CICM 2015, I am PC member for Calculemus.

Don’t be confused by the website that is somewhat difficult to navigate! Don’t miss the start of the submission process: 16-Feb-2015 for abstracts, followed by actual papers, followed the  rebuttal phase. The latter is particularly important to readjust the initial verdict by the reviewers, going upwards or downwards, depending on careful reactions of the authors to what was said about their papers.

Alexander Grothendieck

Born 28-Mar-1928 (Berlin, Germany), died 13-Nov-2014 (Saint-Lizier, France).

In my own studies, I have occasionally encountered the famous name of Grothendieck in lectures about functional analysis and logic. From a bit later, I remember discussions with Helmut Schwichtenberg about Tarski-Grothendieck set theory as the foundation of the formal mathematical language of Mizar.

In 2010, I came again across the name of Alexander Grothendieck several times, when searching the web about my new hometown Bures-sur-Yvette, where I lived until August 2014 only a few hundred meters from the famous IHÉS institute. That was the place where Grothendieck worked for some time at the peak of his mathematical life (until 1970). Afterwards he removed himself more and more from public and scientific life.

Winfried Scharlau has started to publish material about the life of Grothendieck some years ago, with this notable article from 2006/2008. There was also some activity on the web to collect more information, but this was stopped abruptly in 2010 with this angry letter from Grothendieck himself, speaking to the world from a secret place in the Pyrenees.

At least we now know that his last residence was in Lasserre (l’Ariège); see also this article of La Depeche.

Here is another blog with many more links.

UITP 2014 proceedings with Isabelle/jEdit paper

On 29-Oct-2014, EPTCS has published the proceedings of UITP 2014, which was a workshop at VSL 2014, Vienna, July 2014. The volume includes my contribution System description: Isabelle/jEdit in 2014. The paper has been updated to the current official release Isabelle2014 (August 2014).