Colloquium Logicum 2020 (sic!), Konstanz, 26–28 September 2022
talks by Bernhard Fisseni, Deniz Sarikaya, and Bernhard Schröder
Text-Driven Approaches to the Philosophy of Mathematics (TDPhiMa 3): Philosophical and Linguistic Approaches to Computational Mathematics, Duisburg-Essen (hybrid), 7–8 September 2022
organized by Bernhard Fisseni, Juan Luis Gastaldi, Deborah Kant,
Deniz Sarikaya, Bernhard Schröder
talks by Bernhard Fisseni, Deniz Sarikaya, and Bernhard Schröder as well
as Marcos Cramer
Formalize!(?) 2, Online/Zurich, 15 January 2022
organized by Deniz Sarikaya,
talks by Deniz Sarikaya and Bernhard Schröder
Thinking about Proofs. Formal, Philosophical, Linguistic and Educational Perspectives, Online/Passau, 27 September 2021
organized by Deniz Sarikaya,
talk by Bernhard Schröder
Affiliated Minisymposium to the DMV and ÖMG annual meeting 2021
Text-Driven Approaches to the Philosophy of Mathematics (TDPhiMa 2), Online/Duisburg-Essen, 1–3 September 2021
organized by Bernhard Fisseni, Deborah Kant, Deniz Sarikaya, Bernhard
Schröder
talks by Bernhard Fisseni, Peter Koepke, Deniz Sarikaya, and Bernhard
Schröder
Formalize!(?) 1, Online/Zurich, 16 January 2021
organized by Deniz Sarikaya,
talk by Peter Koepke
Mathematical Language and Practical Type Theory, Bonn, 1–4 February 2020
organized by Peter Koepke,
talks by Bernhard Fisseni, Deniz Sarikaya, and Bernhard
Schröder
Text-Driven Approaches to the Philosophy of Mathematics (TDPhiMa 1), Prague, 05–10 August 2019
organized by Deborah Kant and Deniz Sarikaya,
talks by Marcos Cramer, Bernhard Fisseni, Deniz Sarikaya, and Bernhard
Schröder
Contributed symposium to the Congress of Logic, Methodology and Philosophy of Science and Technology 2019
Unfehlbarkeit durch Formalismus?, Bonn, 13–15 March 2015
organized by Deborah Kant and Deniz Sarikaya,
panel discussion with participation of Peter Koepke
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.
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.*
developments
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.
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.
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.
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.
(there was only one meeting and no webpage for it)
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.
(no seminar)
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.
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.
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.
29 January, 9:00–17:00, at Endenicher Allee 60, room 208
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.
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
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.
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.
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?
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.
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.
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.
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.
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.
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.
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.
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/.
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.
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.