Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40440
Titel: | Towards a Framework to Integrate Proof Search Paradigms |
VerfasserIn: | Autexier, Serge Benzmüller, Christoph Hutter, Dieter |
Sprache: | Englisch |
Erscheinungsjahr: | 2003 |
Erscheinungsort: | Saarbrücken |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | Research on automated and interactive theorem proving aims at the mechanization of logical reasoning. Aside from the development of logic calculi it became rapidly apparent that the organization of proof search on top of the calculi is an essential task in the design of powerful theorem proving systems. Different paradigms of how to organize proof search have emerged in that area of research, the most prominent representatives are generally described by the buzzwords: automated theorem proving, tactical theorem proving and proof planning. Despite their paradigmatic differences, all approaches share a common goal: to find a proof for a given conjecture. In this paper we start with a rational reconstruction of proof search paradigms in the area of proof planning and tactical theorem proving. Guided by similarities between software engineering and proof construction we develop a uniform view that accommodates the various proof search methodologies and eases their comparison. Based on this view, we propose a unified framework that enables the combination of different methodologies for proof construction to take advantage of their individual virtues within specific phases of a proof construction. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-404401 hdl:20.500.11880/36416 http://dx.doi.org/10.22028/D291-40440 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 2003,2 |
Datum des Eintrags: | 18-Sep-2023 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - Sonstige Einrichtungen |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI_Report-SR-2003-02_Autexier-Benzmüller-Hutter_Towards-a-Framework-to-Integrate-Proof-Search-Paradigms.pdf | 17,17 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.