# Taclets: a new paradigm for constructing interactive theorem provers.

Bernhard Beckert; Martin Giese; Elmar Habermalz; Reiner Hähnle; Andreas Roth; Philipp Rümmer; Steffen Schlager

RACSAM (2004)

- Volume: 98, Issue: 1, page 17-53
- ISSN: 1578-7303

## Access Full Article

top## Abstract

top## How to cite

topBeckert, Bernhard, et al. "Taclets: a new paradigm for constructing interactive theorem provers.." RACSAM 98.1 (2004): 17-53. <http://eudml.org/doc/41034>.

@article{Beckert2004,

abstract = {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.},

author = {Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Hähnle, Reiner, Roth, Andreas, Rümmer, Philipp, Schlager, Steffen},

journal = {RACSAM},

keywords = {meta languages; KeY system},

language = {eng},

number = {1},

pages = {17-53},

title = {Taclets: a new paradigm for constructing interactive theorem provers.},

url = {http://eudml.org/doc/41034},

volume = {98},

year = {2004},

}

TY - JOUR

AU - Beckert, Bernhard

AU - Giese, Martin

AU - Habermalz, Elmar

AU - Hähnle, Reiner

AU - Roth, Andreas

AU - Rümmer, Philipp

AU - Schlager, Steffen

TI - Taclets: a new paradigm for constructing interactive theorem provers.

JO - RACSAM

PY - 2004

VL - 98

IS - 1

SP - 17

EP - 53

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

LA - eng

KW - meta languages; KeY system

UR - http://eudml.org/doc/41034

ER -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.