## Seminar Formale Mathematik

### Dozenten

- Prof. Dr. Peter Koepke
- Prof. Dr. Bernhard Schröder

### Zeit und Ort

Freitags 10-12 im Zimmer 0.006.

### Inhalt

Vorträge von internen und externen Referenten über Formale Mathematik, d.h., über die axiomatische Durchführung von Mathematik in strikt formalen Sprachen mit strikt formalen Ableitungsregeln. Im Zusammenhang mit dem lokalen Projekt NaProChe (Natural language Proof Checking) wird besonders die Frage diskutiert, inwieweit durch den Einsatz von Softwaresystemen strikt formale Systeme aufgebaut werden können, die für den Benutzer "natürlich" im Sinne des gewöhnlichen mathematischen Arbeitens sind. Das bezieht sich auf Benutzerschnittstellen, verwendete Sprache, Theorien und Beweismethoden.

Die Vorträge finden etwa 14-tägig statt.

**Friday, April 27, 10:15-12:00**, EA 60, Room 0.006

**Uwe Waldmann**, Saturation-based Theorem Proving with Built-in Theory Knowledge

Abstract:
*
We start by giving a short overview of saturation-based proof
systems for first-order logic, such as resolution and superposition.
Then we discuss various methods to integrate (arithmetical) theory
knowledge into such systems. Finally, we have a look at concrete
theorem prover implementations, in particular SPASS and SPASS+T.
*

**Friday, May 4, 10:15-12:00**, EA 60, Room 0.006

**Stephan Schulz**, The Theorem Prover E: Overview and current developments

Abstract:
*
E is a high-performance theorem prover for first-order logic with
equality. E is available free under the GNU GPL and is fairly widely
used and distributed.
The prover consists of several stages: clausification, analyis and
preprocessing, proof search, and, optionally, proof
postprocessing. The heart of the system is an efficient implementation
of the refutational superposition calculus.
The proof procedure is implemented using the DISCOUNT variant of the
given-clause algorithm. Most heuristic choice points can be controlled
using a wide range of fixed or programmable heuristics. Part of the
development process is the automatic adaption of such search
heuristics based on large-scale experimental results.
Recent improvements in E include the ability to focus search on
certain symbols, and much improved indexing techniques to quickly find
inference partners for any given clause.
*

**Friday, May 18, 10:15-12:00**, EA 60, Room 0.006

**Andrei Paskevich**, Why3, where programs meet provers

Abstract:
*
Why3 is a platform for deductive program verification. It features a
rich logical language with polymorphism, algebraic data types, and
inductive predicates. Why3 provides an extensive library of proof task
transformations which can be chained to produce a suitable input for a
large set of theorem provers, including SMT solvers, TPTP provers, as
well as interactive proof assistants. In this talk, we show how this
technology is used to combine interactive and automated theorem
provers in, though not limited to, the context of program verification.
*

**Friday, June 8, 10:15-12:00**, EA 60, Room 0.006

**Jesse Alama**, Needed premises and multiple proofs

Abstract:
*
From a formal standpoint, everyday mathematical proofs are full of
logical gaps. Sometimes the gaps are "mere details": we don't care
how they are filled, so long as they can be filled. Even if we accept
that there can be many formal derivations of a conclusion from a set
of premises, the ways in which the derivations differ (e.g.,
some premises can be permuted) might be immaterial to us. At other
times, though, logical gaps can be filled in notably different ways,
and we may want to be sensitive to such differences. When we fill
gaps in proofs with the help of external tools, as Naproche and SAD do
with powerful automated theorem provers, we may find that a formal
(Naproche, SAD) text expresses not one but multiple proofs. In this
talk we explore how the notion of "needed premise" can be used to
bring out such potential multiplicity of proofs, and their value for
the Naproche project.
*

**Friday, July 6, 10:15-12:00**, EA 60, Room 0.006

**General discussion about future plans**

*
We meet for a rather informal general discussion about plans for future developments of the Naproche project. Marcos Cramer will start the discussion by presenting some of his ideas for possible future developments of the project.
*

### Former Terms

- WS 08/09
- SS 09
- WS 09/10
- SS 10
- WS 10/11 (no seminar)
- SS 11
- WS 11/12 (there was only one meating and no webpage for it)