Hinweis zum Urheberrecht | Allgemeine Informationen | FAQ
Beim Zitieren dieses Dokumentes beziehen Sie sich bitte immer auf folgende URN: urn:nbn:de:hbz:5n-33909

 

Mathematisch-Naturwissenschaftliche Fakultät - Jahrgang 2013

 

Titel Proof-checking mathematical texts in controlled natural language
Autor Marcos Cramer
Publikationsform Dissertation
Zusammenfassung Die Forschung, die für diese Dissertation durchgeführt wurde, basiert auf der Vision eines Computerprogramms, das die Korrektheit von mathematischen Beweisen, die in der gewöhnlichen mathematischen Fachsprache verfasst sind, überprüfen kann. Da die zuverlässige automatische Bearbeitung von uneingeschränktem natürlich-sprachlichen Input außer Reichweite der gegenwärtigen Technologie ist, haben wir uns auf das erreichbare Ziel fokussiert, eine kontrollierte natürliche Sprache (eine Teilmenge der natürlichen Sprache, die durch eine formale Grammatik definiert ist) als Eingabesprache für ein solches Programm zu verwenden. Wir haben einen Prototypen eines solchen Computerprogramms, das Naproche-System, entwickelt. Die vorliegende Dissertation beschreibt die neuartigen logischen und linguistischen Theorien, die benötigt werden, um die kontrollierte natürliche Sprache und den Beweisprüfungs-Algorithmus des Naproche-Systems zu definieren und zu motivieren. Diese Theorien stellen Methoden zu Verfügung, die dazu verwendet werden können, die weite Kluft zwischen natürlichen und formalen mathematischen Beweisen zu überbrücken. weiter...
Abstract The research conducted for this thesis has been guided by the vision of a computer program that could check the correctness of mathematical proofs written in the language found in mathematical textbooks. Given that reliable processing of unrestricted natural language input is out of the reach of current technology, we focused on the attainable goal of using a controlled natural language (a subset of a natural language defined through a formal grammar) as input language to such a program. We have developed a prototype of such a computer program, the Naproche system. This thesis is centered around the novel logical and linguistic theory needed for defining and motivating the controlled natural language and the proof checking algorithm of the Naproche system. This theory provides means for bridging the wide gap between natural and formal mathematical proofs. more...
Inhaltsverzeichnis pdf-Dokument Hier können Sie den Adobe Acrobat Reader downloaden
Komplette Version pdf-Dokument (2,5 MB) Hier können Sie den Adobe Acrobat Reader downloaden
© Universitäts- und Landesbibliothek Bonn | Veröffentlicht: 30.10.2013