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ößeFormat 
SEKI-Report-SR-92-02_Becker_Inductive-Proofs-in-Specifications-Parametrized-by-a-Built=in-Theory.pdf5,02 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.