Naproche - Seminar on Formal Mathematics 2008

Organized by Peter Koepke and Bernhard Schröder.

Friday, October 31, 10:15-12:00, Beringstr. 4 Seminarraum B
Serge Autexier, Stephan Busemann, Marc Wagner, Semantik-basierte Autorenwerkzeuge für mathematische Dokumente
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
Norbert E. Fuchs, Knowledge Representation and Reasoning in (Controlled) Natural Language
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 attempto.ifi.uzh.ch/. The demo version of RACE can be accessed at attempto.ifi.uzh.ch/race/.

Friday, December 12, 10:15-12:00, Beringstr. 4 Seminarraum B
Claus Zinn, Supporting the formal verification of mathematical texts
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
Geoff Sutcliffe, TPTP, TSTP, CASC, etc.
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.