Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-41002
Titel: | [Omega]-MKRP : A Proof Development Environment |
VerfasserIn: | Huang, Xiaorong Kerber, Manfred Kohlhase, Michael Melis, Erica Nesmith, Dan Richts, Jörn Siekmann, Jörg |
Sprache: | Englisch |
Erscheinungsjahr: | 1992 |
Erscheinungsort: | Saarbrücken |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | This report presents the main ideas underlying the Ω-MKRP-system, an environment for the development of mathematical proofs. The motivation for the development of this system comes from our extensive experience with traditional first-order theorem provers and aims to overcome some of their shortcomings. After comparing the benefits and drawbacks of existing systems, we propose a system architecture that combines the positive features of different types of theorem-proving systems, most notably the advantages of human-oriented systems based on methods (our version of tactics) and the deductive strength of traditional automated theorem provers. In Ω -MKRP a user first states a problem to be solved in a typed and sorted higher-order language (called POST) and then applies natural deduction inference rules in order to prove it. He can also insert a mathematical fact from an integrated database into the current partial proof, he can apply a domain-specific problem-solving method, or he can call an integrated automated theorem prover to solve a subproblem. The user can also pass the control to a planning component that supports and partially automates his long-range planning of a proof. Toward the important goal of user-friendliness, machine-generated proofs are transformed in several steps into much shorter, better-structured proofs that are finally translated into natural language. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-410021 hdl:20.500.11880/37707 http://dx.doi.org/10.22028/D291-41002 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 92,22 |
Datum des Eintrags: | 24-Mai-2024 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI-Report-SR-92-22_Huang-Kerber-Kohlhase-Melis-Nesmith-Richts-Siekmann_[Omega]=MKRP-A-Proof-Development-Environment.pdf | 1,5 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.