QED+20, FRIDAY, JULY 18TH 2014

09:00-10:15 Session 87J
Location: FH, Hörsaal 4
QED: a grand unified theory?
How to prove the odd order from the four color theorem
10:15-10:45Coffee Break
10:45-13:00 Session 90BG
Location: FH, Hörsaal 4
25 years of the Mizar Mathematical Library

ABSTRACT. Throughout the years, the development of the Mizar Mathematical Library was stimulated by large formalization projects, of which the proof of the Jordan Curve Theorem and the encoding of "Compendium of Continuous Lattices" were most influential. In Andrzej Trybulec's (the head of the Mizar project) opinion, expressed during QED II workshop in 1995, "one of the fundamental tasks of the QED effort should focus on reconstruction of the language and technology of mathematics." We will show how Andrzej's dreams of QED are implemented.

The seL4 microkernel verification

ABSTRACT. This talk will first give a brief high-level overview of the formal verification of the seL4 microkernel before showing some of its proof techniques in more detail. The aim will be to show examples of libraries and tactics for refinement, invariant, and security proofs for operating systems.

Towards Formally Verified Theorem Provers - Part I
Towards Formally Verified Theorem Provers - Part II
13:00-14:30Lunch Break
14:30-16:00 Session 96BE
Location: FH, Hörsaal 4
Mixing proofs and computations

ABSTRACT. In order to achieve the goals of QED, it will be necessary to effectively combine calculations and proofs in the same formal and computerized representation. We discuss the obstacles to this combination, and some of the attempts to overcome those obstacles.

The Naproche system: Proof-checking mathematical texts in controlled natural language

ABSTRACT. We have developed a controlled natural language (CNL) – i.e. a subset of a natural language defined through a formal grammar – for writing mathematical texts. The Naproche system can check the correctness of mathematical proofs written in this CNL. In this talk we will highlight some interesting logical and linguistic problems that had to be solved in the development of the Naproche CNL and the Naproche system: The system uses a formalism from the linguistic theory of presuppositions in order to work with potentially undefined terms, and can handle dynamic quantification, including the phenomenon of implicit dynamic function introduction, which had previously not been discussed in the literature.

16:00-16:30Coffee Break
16:30-18:00 Session 99AZ
Location: FH, Hörsaal 4
QED and the TPTP World
MathHub.info: Active Mathematics

ABSTRACT. We present the MathHub.info system, a development environment for active mathematical documents and an archive for flexiformal mathematics. It offers a rich interface for reading, writing, and interacting with mathematical documents and knowledge. The core MathHub.info system is an archive for flexiformal mathematical documents and libraries in the OMDoc/MMT format. Content can be authored or archived in the source format of the respective system, is versioned in GIT repositories, and transformed into OMDoc/MMT for machine-support and further into HTML5 for reading and interaction.

Hammering towards QED
18:15-18:45 Session 104D
Location: FH, Hörsaal 4
Panel Discussion
Powered by EasyChair Smart Program