Interactive Theorem Proving with Schematic Theory Specific Rules

Elmar Habermalz


This paper 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. It is planned to integrate this
schematic rules into the theorem prover that will be used in the KeY
project.
  
The language of schematic theory specific rules 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 on 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.