KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Schönegge, Arno


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).

Open Access Logo

Volltext §
DOI: 10.5445/IR/38594
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1994
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA385947
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