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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.