KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
URN: urn:nbn:de:swb:90-AAA385947

Valid extensions of introspective systems: a foundation for reflective theorem provers

Schönegge, Arno

Abstract:

Introspective systems have been proved ueful in several
applications, especially in the area of automated reasoning.
In this paper we propose to use structured algebraic
specifications to describe the embedded account of introspective
systems. Our main result is that extending such an introspective
system in a valid manner can be reduced to development of correct
software. Since sound extension of automated reasoning systems
again can be reduced to valid extension of introspective systems,
our work can be seen as a foundation for extensible
introspective reasoning systems, and in particular for
reflective provers. We prove correctness of our mechanism and
report on first experiences we have made with its realization in
the KIV system (Karlsruhe Interactive Verifier).


Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 1994
Sprache Englisch
Identifikator KITopen ID: 38594
Erscheinungsvermerk Karlsruhe 1994. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1994,26.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page