KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-AAA22720000

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.

Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Forschungsbericht
Jahr 2000
Sprache Englisch
Identifikator ISSN: 1432-7864
KITopen ID: 2272000
Verlag Karlsruhe
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