Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40775
Titel: | Inductive Proofs in Specifications Parametrized by a Built-in Theory |
VerfasserIn: | Becker, Klaus |
Sprache: | Englisch |
Erscheinungsjahr: | 1992 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | We consider the problem of proving hypotheses to be valid in all canonical term models of some parametrized positive/negative conditional equational specification that are induced by the actualizations of the given parameter theory. In a first part we develope a method to operationally handle as well the parameter actualizations as the body specification and here in particular the negative conditions occuring possibly in the conditional equations. By introducing restrictions on the conditional equations the induced canonical term algebras become in a certain sense initial models of the specification. In a second part we present a proof by consistency method to deal with hypotheses formulated as clauses over the body and (formal) parameter language. If some syntactical premises are fulfilled and if a (built-in) algorithm is available that decides whether clauses over the parameter language only are logical consequences of the parameter theory or not, then the proof method becomes refutationally complete. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-407758 hdl:20.500.11880/37694 http://dx.doi.org/10.22028/D291-40775 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 92,2 |
Datum des Eintrags: | 23-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-02_Becker_Inductive-Proofs-in-Specifications-Parametrized-by-a-Built=in-Theory.pdf | 5,02 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.