Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-24942
Titel: | Parameterized abstractions used for proof-planning |
VerfasserIn: | Autexier, Serge Hutter, Dieter |
Sprache: | Englisch |
Erscheinungsjahr: | 1997 |
Quelle: | Kaiserslautern ; Saarbrücken : DFKI, 1997 |
Kontrollierte Schlagwörter: | Künstliche Intelligenz |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | In order to cope with large case studies arising from the application of formal methods in an industrial setting, this paper presents new techniques to support hierarchical proof planning. Following the paradigm of difference reduction, proofs are obtained by removing syntactical differences between parts of the formula to be proven step by step. To guide this manipulation we introduce dynamic abstractions of terms. These abstractions are parameterized by the individual goals of the manipulation and are especially designed to ease the proof search based on heuristics. The hierarchical approach and thus the decomposition of the original goal into several subgoals enables the use of different abstractions or different parameters of an abstraction within the proof search. In this paper we will present one of these dynamic abstractions together with heuristics to guide the proof search in the abstract space. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291-scidok-38219 hdl:20.500.11880/24998 http://dx.doi.org/10.22028/D291-24942 |
Schriftenreihe: | Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x] |
Band: | 97-04 |
Datum des Eintrags: | 29-Jun-2011 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
RR_97_04.pdf | 233,93 kB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.