Naproche - Natural Language Proof Checking

Seminar Formale Mathematik


Zeit und Ort

Freitags 10-12 im Zimmer 006.


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. 

30 November, 16:30-18:00 at Endenicher Allee 60, room 1.007. Jeremy Avigad (Carnegie Mellon University and INRIA-Microsoft Research Joint Centre, Orsay) A formal system for Euclidean diagrammatic reasoning

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.
18 December, 15.15-16.45 at Endenicher Allee 60, room 006 Aarne Ranta (University of Gothenburg) GF and the Language of Mathematics

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.
29 January, 9:00 - 17:00 at Endenicher Allee 60, room 208 Naproche Progress Meeting

  • 9:15 - 10:00 Sebastian Zittermann: The Naproche WebInterface
  • 10:00 - 11:00 Daniel Kühlwein The Premise Selection Algorithm
  • 11:15 - 12:00 Marcos Cramer: Neue linguistische Konstruktionen in Naproche
  • 12:00 - 13:30 Mittagspause
  • 13:30 - 14:15 Diskussion zur Formelgrammatik
  • 14:30 - 15:30 Diskussion zum Gebrauch von GF in Naproche
  • 15:45 - 16:45 Diskussion zu Euklid in Naproche
  • 5 February 10:00-12:00 in room 006 at EA 60 Peter Schodl Universit├Ąt Wien

    "MoSMath -- A MOdeling System for MATHematics" by Peter Schodl, University of Vienna (Austria)

    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.
    5 February 14:00-16:00 in room 1007 at EA 60 Arnold Neumaier Universit├Ąt Wien

    Towards a Computer-Aided System for Real Mathematics by Arnold Neumaier University of Vienna (Austria)

    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.

    Former Terms


    Last changed November 26st 2009