Seminar Formal Mathematics (2008–2012)

Between 2008 and 2012, Prof. Dr. Peter Koepke and Prof. Dr. Bernhard Schröder organized the Seminar on Formal Mathematics. The talks were given by invited speakers on topics relevant to the Naproche project. The pages linked below list the talks given during the different semesters in this time period.

SS 2012

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

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

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.*

Stephan Schulz: The Theorem Prover E: Overview and current


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

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, analysis 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.

Andrei Paskevich: Why3, where programs meet provers

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

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.

Jesse Alama: Needed premises and multiple proofs

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

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.

General discussion about future plans

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

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.

WS 11/12

(there was only one meeting and no webpage for it)

SS 2011

Marco Caminati: Classical model theory in Mizar

Friday, April 15, 11:15-13:00 (one hour later than usual!) EA 60, Room 1.007

Abstract: I have formalized Lindenbaum lemma, satisfiability, Godel's completeness and Lowenheim-Skolem theorems in Mizar, using a simplified, unified and coherent framework to encode model theory.

I will describe this framework, focusing in particular on the simplified syntax for first-order languages (only two special symbols, and no need for constant symbols) and on the sequent derivation rules adopted (not requiring to define the concept of free occurrence).

Then I will show how those constructions were used for a new, Henkin-like, scheme to prove the results hinted above, with emphasis on the role of each single derivation rule, and on when some standard definitions (consistency, maximality, rule correctness) of model theory actually need to come into play.

If time permits, I will also discuss some aspects of the Mizar implementation of the aforementioned syntax and sequent calculus.

WS 10/11

(no seminar)

SS 2010

John Mumma: Euclid's diagrams and the primitive concepts of

elementary geometry

Friday, June 18, 10:15-12:00 EA 60, Room N0.007 (Nebengebäude)

Abstract: One thing a formalization of a mathematical theory provides is a sharp classification of the theory's concepts as either primitive or defined. In this talk, I examine how this separation is made in two formalizations of Euclid's elementary plane geometry: the axiomatization presented in Tarski's `What is elementary geometry?', and the formal system E. The latter is a system that has recently been developed to illuminate the role of diagrams in the proofs in the Elements. In accounting for Euclid's diagrams, E classifies more geometric relations as primitive than Tarski's formalization does. At the same time, the logic of E is much weaker. I show what this trade-off amounts to precisely by describing E as a formal system and sketching the proof that E is complete relative to Tarksi's theory.

WS 2009

Jeremy Avigad (Carnegie Mellon University and INRIA-Microsoft Research Joint Centre, Orsay): A formal system for Euclidean diagrammatic reasoning

30 November, 16:30-18:00 at Endenicher Allee 60, room 1.007.

This talk presents work carried out jointly with Ed Dean and John Mumma.

For more than two thousand years, Euclid's Elements was viewed as the paradigm of rigorous argumentation. But this changed in the nineteenth century, with concerns over the use of diagrammatic inferences and their ability to secure general validity. Axiomatizations by Pasch, Hilbert, and later Tarski are now taken to rectify these shortcomings, but proofs in these axiomatic systems look very different from Euclid's.

In this talk, I will argue that proofs in the Elements, taken at face value, can be understood in formal terms. I will describe a formal system with both diagram- and text-based inferences that provides a much more faithful representation of Euclidean reasoning. For the class of theorems that can be expressed in the language, the system is sound and complete with respect to Euclidean fields, that is, the semantics corresponding to ruler and compass constructions.

The system's one-step inferences are smoothly verified by current automated reasoning technology. This makes it possible to formally verify Euclidean diagrammatic proofs, and provides useful insight into the nature of mathematical proof more generally.

Aarne Ranta (University of Gothenburg) GF and the Language of Mathematics

18 December, 15.15-16.45 at Endenicher Allee 60, room 006

GF (Grammatical Framework) is a grammar formalism designed for multilingual grammars. A multilingual grammar is a system based on a shared semantic structure with reversible mappings to several languages. By means of these mappings, it is possible to translate between all the included languages. For instance, the semantic structure (Gt x y) might have the translations “x is greater than y” (English), “x ist größer als y“ (German), “x > y“ (mathematical symbolism). The format for defining semantic structures is a higher-order dependently typed lambda calculus, which is expressive enough for formalizing usual mathematical theories and logics. The format for defining translations is expressive enough for dealing with grammatical structures such as German word order, so that e.g. “x > y -> ~ y < x” gets correctly translated “wenn x größer als y ist, dann ist y nicht größer als x“.

GF has been used in many implementations of technical translation systems and natural language interfaces. One example is the European project WebALT, where mathematical exercises are automatically translated from OpenMATH specifications to seven European languages. The project developed a library of GF translation rules for hundreds of mathematical concepts, which is available as open-source software.

The talk will give a hands-on introduction to GF, working through an example grammar for mathematical language. We will also discuss the problems and limitations of the approach, in the light of previous experiences from projects on mathematical language.

Naproche Progress Meeting

29 January, 9:00–17:00, at Endenicher Allee 60, room 208

Sebastian Zittermann: The Naproche WebInterface
Daniel Kühlwein The Premise Selection Algorithm
Marcos Cramer: Neue linguistische Konstruktionen in Naproche
Diskussion zur Formelgrammatik
Diskussion zum Gebrauch von GF in Naproche
Diskussion zu Euklid in Naproche

Peter Schodl Universität Wien: MoSMath – A MOdeling System for MATHematics

5 February 10:00-12:00 in room 006 at EA 60

The goal of the MoSMath project, carried out at the University of Vienna under the supervision of Prof. Neumaier, is the creation of a software package that is able to understand, represent and interface optimization problems posed in a controlled natural language.

We developped a user-friendly representation of semantic information in a data structure called the semantic matrix. This representation is designed to be human intelligible and clear, akin to the Semantic Web. A type system was created that is suited for the typing of both usual data structures and grammatical categories in the semantic matrix. We also developped a semantic Turing machine (STM), a variant of a register machine that combines the transparency and simplicity of the action of a Turing machine with a clearly arranged assembler-style programming language and a memory in the form of a semantic matrix.

As a first step towards our controlled natural language we derived a context-free grammar from a textbook on calculus and linear algebra. We currently have an interface to and a representation of problems in the TPTP, and a representation of a number of optimization problems from the OR-Library.

An interface to the controlled natural language of Naproche (developed in Bonn and Duisburg-Essen for representing human-readable formal proofs) enables us to read and represent texts written in this language, and to recreate Naproche-texts from texts represented in the semantic matrix.

Arnold Neumaier Universität Wien: Towards a Computer-Aided System for Real Mathematics

5 February 14:00-16:00 in room 1007 at EA 60

This is joint work with Peter Schodl and Kevin Kofler, also from Vienna. We are currently working towards the creation of an automatic mathematical research system that can support mathematicians in their daily work, providing services for abstract mathematics as easily as Latex provides typesetting service, the arXiv provides access to preprints, Google provides web services, Matlab provides numerical services, or Mathematica provides symbolic services.

This is partly a vision, expected to take 50 man years to bring a system far enough that it will grow by itself in a wikipedia-like fashion. A limited part of the goals are being realized through the project ``A modeling system for mathematics'' (MoSMath), currently supported by a grant of the Austrian Science Foundation FWF.

Within this project, we attempt to create a modeling and documentation language for conceptual and numerical mathematics called FMathL (formal mathematical language), suited to the habits of mathematicians.

The goal of the FMathL project is to combine

  • the advantages of LaTeX for writing and viewing mathematics,
  • the user-friendliness of mathematical modeling systems such as AMPL for the flexible definition of large-scale numerical analysis problems,
  • the universality of the common mathematical language to describe completely arbitrary problems,
  • the high-level discipline of the CVX system for solving convex programming problems and enforcing their semantic correctness, and
  • the semantic clarity of the Z notation for the precise specification of concepts and statements.

We believe that this goal is reachable, and that an easy-to-use such system will change the way mathematical modeling is done in practice.

The project complements efforts for formalizing mathematics from the computer science and automated theorem proving perspective. In the long run, the FMathL system might turn into a user-friendly automatic mathematical assistant for retrieving, editing, and checking mathematics in both informal, partially formalized, and completely formalized mathematical form.

SS 2009

Andrei Paskevich, ForTheL: design decisions [not [yet] taken]

Friday, April 17, 10:15-12:00, EA 60, Room 006

Abstract: Historically, the best-known and most powerful proof assistants were the systems with quite specific logical foundations, input languages, and proof development tools. This created a considerable barrier for newcomers, even for those who were experienced in formal mathematics. In recent years, however, the idea to lower this barrier – by using (elements of) natural language in the input, by adopting traditional “declarative” style of proof, by abstracting over the particularities of a given verifier – gained a lot of attention, and a number of new projects have emerged.

In this talk, we present a formal language, called ForTheL, which imitates the natural language and style of “human” mathematical texts. This language is used as the input language of SAD, a proof assistant intended for automated proof verification. We demonstrate that ForTheL allows for terse and comprehensible formalizations and describe its syntax and semantics with respect to verification. We also enumerate the features that the current realization of ForTheL is lacking and discuss the ways to address these shortcomings.

Workshop VeriMathDoc – Naproche

Thursday, Mai 14, EA 60, Room 208 until 16:30 and then Room 107

9:00–11:00 Session Formalisierung Formalisierung

Es gibt i.A. mehrere Möglichkeiten, wie die beschriebenen Konzepte in Logik formalisiert werden (Beispiel: der Begriff einer “Klasse” als Sorte/Typ oder als Prädikat). Je nachdem wie man sich entscheidet, hat das Vor- und Nachteile und es scheint keine a priori bessere Art zu formalisieren zu geben. Aber, in dem Prozess nach der Textanalyse hin zum Beweissystem muss die Entscheidung getroffen werden und die Frage ist wie man sie trifft, welche Probleme es hier gibt und allgemein, wie kann man damit umgehen, dass es Alternativen gibt?

  • Vortrag “Möglichkeiten Klassen zu formalisieren”
  • Diskussion:
    • Inwieweit legen wir die Art der Formalisierung in den Systemen fest?
    • Falls wir sie nicht festlegen, wie kann der Autor sie angeben?
    • Wollen wir mit alternativen Formalisierungen umgehen können?
    • Fazit und Planung bis zum nächsten Treffen

11:00–13:00: Session Corpora of Documents

Sowohl VeriMathDoc als auch Naproche benötigen Beispieltexte um die Fähigkeiten des jeweiligen Systems zu demonstrieren. In dieser Session wollten wir erörtern inwieweit eine gemeinsame Sammlung möglich ist.

  • Vortrag Syntax Naproche (15–30 min)
  • Vortrag Syntax VeriMathDoc (15–30 min)
  • Diskussion:
    • Ist eine gemeinsame Syntax möglich? Wie müsste man die bestehenden erweitern/anpassen.
    • Welche Arten von Dokumente (vollständig/Fragmente) wollen wir annotieren und in welchen Formaten? Wie wollen wir darin suchen können? Wo bekommen wir die her?
  • Fazit und Planung bis zum nächsten Treffen

13:00–14:00 Mittagessen

14:00–16:00: Session Textanalyse

Beide Projekte verwenden sehr verschiedene Methoden zur Textanalyse. Was die Probleme der jeweiligen Methoden, und was könnten Lösungsansätze sein.

  • Vortrag Probleme Textanalyse Naproche (~15 min)
  • Vortrag Probleme Textanalyse VeriMathDoc (~15 min)
  • Diskussion: Kann man die die Methoden kombinieren um die Probleme zu lösen.
    • Wie gehen wir mit Fehlschlägen in der Textanalyse um? Wie geht man mit Texten um, die man erkennbar nur partiell analysieren kann? Sind partielle Analyseergebnisse (etwa aus einer Chart) verwendbar?
    • Domänenspezifische Semantik/Pragmatik: Können wir Meta-Aussagen (zB “Wir geben nun zwei weitere Regeln für das Rechnen mit Vektorprodukten an, von denen wir die erste gleich und die zweite im nächsten Abschnitt beweisen werden.” [1]) mit flachen Verfahren hinreichend erkennen?
  • Fazit und Planung bis zum nächsten Treffen

16:00–16:30 Kaffee

16:30–18:30 Session: Beweistechniken

Abgesehen von den angeschlossenen Beweisern ist oft auch eine Vorverarbeitung wünschenswert. Was wurde hier schon implementiert, welche Probleme sind aufgetreten.

  • Vortrag Beweistechniken Naproche (15–30 min)
  • Vortrag Beweistechniken VeriMathDoc (15–30 min)
  • Diskussion:
    • Potentielle Problemlösungen
    • Fazit und Planung bis zum nächsten Treffen

Marcos Cramer: The Naproche Project, Controlled Natural Language

Proof Checking of Mathematical Texts

Friday, May 29, 10:15-12:00 EA 60, Room 006

Abstract: This is the talk that we will give at the CNL (Controlled Natural Language) Conference in Marettimo in June. We will discuss the Semi-Formal Language of Mathematics, present the Naproche CNL that is based on it, and explain the Proof Representation Structures that can be derived from a Naproche text.

Extended Abstract of this talk

Daniel Kuehlwein: The Naproche System

Friday, June 19, 10:15-11:00, EA 60, Room 006

Abstract: This is the talk that we will give at the Calculemus Conference. We give an introduction to the Naproche System.

Extended Abstract of this talk

Sebastian Zittermann: Scheme2XML

Friday, June 19, 11:15-12:00, EA 60, Room 006

Abstract: Der Vortrag stellt das Programm Scheme2XML vor. Scheme2XML erstellt aus einer Datei des TeXmacs-Formats “SCM” anhand vorgegebener Regeln, die in der Datei Satz.dtd definiert sind, eine XML-Datei und überprüft diese auf Validität.

Zugrundeliegende Bachelorarbeit

WS 2008/09

Serge Autexier, Stephan Busemann, Marc Wagner: Semantik-basierte Autorenwerkzeuge für mathematische Dokumente

Friday, October 31, 10:15-12:00, Beringstr. 4, Seminarraum B

Abstract: Die Erstellung von Dokumenten mit mathematischen Inhalten stellt höchste Ansprüche an die typographische Qualität, denen in existierenden Autorenwerkzeugen Rechnung getragen wird, etwa in TeX-basierten Systemen und neuerdings auch in Word 2007. Dahingegen bieten diese nur mangelhafte Unterstützung für die Überprüfung der Inhalte – etwa die konsistente Verwendung von Notationen oder Zyklenfreiheit und ggf. Verifikation definitorischer und argumentativer Strukturen – sowie für darauf aufbauende erweiterte Editier-Operationen, wie die Eingliederung von Teildokumenten in ein Gesamtdokument oder die Umgestaltung eines Dokuments. Ziel des VerimathDoc-Projektes ist die Entwicklung von Methoden und Techniken, um semantik-basierte Assistenzwerkzeuge in existierende Autorenwerkzeuge zu integrieren. Grundprinzip hierbei ist der Einsatz computerlinguistischer Textanalyse-Verfahren, um den Inhalt eines Dokuments in semi-formale und schließlich auch formallogische Strukturen zu überführen, auf deren Grundlage entsprechende Unterstützung bereitgestellt werden kann, wie sie zum Teil bereits in interaktiven Beweisassistenzsystemen existiert. Daraus resultierende Modifikationen und Erweiterungen der Strukturen sollen anschließend mit Hilfe von Textgenerierungs-Verfahren wieder in das Dokument integriert werden können.

Dieser Vortrag gibt einen Überblick über die allgemeinen Ziele und den aktuellen Stand des VerimathDoc-Systems, welches derzeit das Beweisassistenzsystem OMEGA mit Hilfe des Mediators Plato transparent mit dem Texteditor TeXmacs verbindet. Weiterhin gibt er einen Überblick, wie die verschiedenen Themenkomplexe aus den Gebieten der Computerlinguistik, Informatik, und interaktiven Beweisassistenzsysteme im Speziellen behandelt wurden bzw. künftig behandelt werden sollen.

Norbert E. Fuchs: Knowledge Representation and Reasoning in (Controlled) Natural Language

Friday, November 21, 10:15-12:00, Beringstr. 4, Seminarraum B

Abstract: Attempto Controlled English (ACE) – a subset of English that can be unambiguously translated into first-order logic – is a knowledge representation language. To support automatic reasoning in ACE we have developed the Attempto Reasoner (RACE). RACE proves that one ACE text is the logical consequence of another one, and gives a justification for the proof in ACE. If there is more than one proof, RACE will find all of them. Variations of the basic proof procedure permit query answering and consistency checking. Reasoning in RACE is supported by auxiliary first-order axioms and by evaluable functions. The current implementation of RACE is based on the model generator Satchmo. As a consequence, RACE cannot only be used for theorem proving but also for model generation.

More information on ACE and its tools can be found at http://attempto.ifi.uzh.ch/. The demo version of RACE can be accessed at http://attempto.ifi.uzh.ch/race/.

Claus Zinn: Supporting the formal verification of mathematical texts

Friday, December 12, 10:15-12:00, Beringstr. 4, Seminarraum B

Abstract: The formal verification of mathematical texts is one of the most interesting applications for computer systems. In fact, we argue that the expert language of mathematics is the natural choice for achieving efficient mathematician-machine interaction. Our empirical approach, the analysis of carefully authored textbook proofs, forces us to focus on the language and the reasoning pattern that mathematician use when presenting proofs to colleagues and students. Enabling a machine to understand and follow such language and argumentation is seen to be the key to usable and acceptable math assistant systems. In this talk, I will first perform an analysis of an example textbook proof by hand; I will then describe a computational framework, based on Discourse Representation Theory and Proof Planning, that aims at mechanising such an analysis. The resulting proof-of-concept implementation is capable of processing simple textbook proofs and constitutes promising steps towards a natural mathematician-machine interface for proof development and verification.

Geoff Sutcliffe: TPTP, TSTP, CASC, etc.

Friday, January 9, 10:15-12:00, Beringstr. 4, Seminarraum B

Abstract: This talk gives an overview of activities and products that stem from the Thousands of Problems for Theorem Provers (TPTP) problem library for Automated Theorem Proving (ATP) systems. These include the TPTP itself, the Thousands of Solutions from Theorem Provers (TSTP) solution library, the TPTP language, the CADE ATP System Competition (CASC), tools such as my semantic Derivation Verifier (GDV) and the Interactive Derivation Viewer (IDV), meta-ATP systems such as the Smart Selective Competition Parallelism (SSCPA) system and the Semantic Relevance Axiom Selection System (SRASS), and applications in various domains.