Concise - a synthesis of types, grammars, semantics

Add to your list(s) Download to your calendar using vCal

• Arnold Neumaier (Universität Wien)
• Wednesday 26 July 2017, 11:00-12:00
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact info@newton.ac.uk.

BPR - Big proof

(joint work with Peter Schodl, Ferenc Domes, Kevin Kofler, Andreas Pichler, and David Langer, Vienna)

This talk features the design and implementation of tools that my research group in Vienna has created to pave the way towards automatically or interactively extracting from standard mathematical literature (such as the latex source of mathematics textbooks) a formal version of all  (correct and incorrect) mathematical claims contained in it, including all claims in the proofs and all implicit information needed for their understanding. We have very encouraging performance results for certain low level partial goals in this direction.

Completing this program (which I believe to be feasible with Thus it would bridge the mathematicians' side of the current gap between mathematics and formal theorem proving.

Central to everything are the working implementation of

• (i) a very flexible type system that merges types, grammars, and semantics into an organic unity, and
• (ii) a dynamic parser for languages that change while reading a document – one of the key features present in mathematical documents.

Background (and, in the near future, more results) can be found on the project web page: neum/FMathL.html">http://www.mat.univie.ac.at/neum/FMathL.html

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.