Naproche - Natural Language Proof Checking

Seminar Formale Mathematik


Zeit und Ort

Freitags 10-12 im Zimmer 0.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. 

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


Last changed 19th April 2012