Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle,
Andreas Roth, Philipp Rümmer, and Steffen Schlager
Frameworks for interactive theorem proving give the user explicit
control over the construction of proofs based on meta languages that
contain dedicated control structures for describing proof
construction. Such languages are not easy to master and thus
contribute to the already long list of skills required by prospective
users of interactive theorem provers. Most users, however, only need a
convenient formalism that allows to introduce new rules with minimal
overhead. On the the other hand, rules of calculi have not only purely
logical content, but contain restrictions on the expected context of
rule applications and heuristic information. We suggest a new and
minimalist concept for implementing interactive theorem provers called
taclet. Their usage can be mastered in a matter of hours, and they
are efficiently compiled into the GUI of a prover. We implemented the
KeY system, an interactive theorem prover for the full Java Card
language based on taclets.