KIT | KIT-Bibliothek | Impressum | Datenschutz

Interactive theorem proving with schematic theory specific rules

Habermalz, Elmar


This work presents a framework to make interactive
proving over abstract data types (first order logic
plus induction) more comfortable. A language of
schematic rules is introduced, yielding the ability to
write, to use, and even to verify these rules for any
abstract data type and its theory.

The language allows to express the functionality of a
rule easily and clearly. Nearly all potential rule
applications are coupled with the occurrence of
certain terms or formulas. One can prove with these
rules simply by mouse clicks onto these terms and
formulas. The rule language is expressive enough to
describe even complex induction rules. Nevertheless,
the correctness of a rule can be verified within the
same theory without use of explicit higher order logic
or of a translation to some kind of meta level. So, in
each state of a proof, new rules can be introduced,
whenever required, and proven.

Volltext §
DOI: 10.5445/IR/2272000
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 2000
Sprache Englisch
Identifikator ISSN: 1432-7864
KITopen-ID: 2272000
Verlag Universität Karlsruhe (TH)
Umfang 15 S.
Serie Interner Bericht. Universität Karlsruhe, Fakultät für Informatik ; 2000,19
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page