Taclets and the KeY prover
The work
| Authors | Martin Giese |
|---|---|
| Editors | |
| Type | article |
| Year | 2004 |
| Citekey | giese2004taclets |
Where it appeared
| Published in | Electronic Notes in Theoretical Computer Science |
|---|---|
| Volume | 103 |
| Pages | 67--79 |
Identifiers
| DOI | 10.1016/j.entcs.2004.09.014 |
|---|
Related
| Distinct from | beckert2004taclets Two 2004 papers on taclets, KeY's rule-description mechanism, with overlapping authorship and different scope: 'Taclets: A New Paradigm for Constructing Interactive Theorem Provers' states the idea generally, and 'Taclets and the KeY prover' treats its use in the prover itself. Neither reprints or supersedes the other and they were not published together, but a reader who finds one is very likely to want the other, and nothing else in the corpus said so. |
|---|
Abstract
We give a short overview of the KeY prover – which is the proof system belonging to the KeY tool [1] – from a user interface perspective. In particular, we explain the concept of taclets, which are the basic building blocks for proofs in the KeY prover.
A copy is held
pdf, 207.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-14 11:32 UTC |
Cite it as
@article{giese2004taclets,
title = {Taclets and the KeY prover},
author = {Martin Giese},
year = {2004},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {103},
pages = {67--79},
doi = {10.1016/j.entcs.2004.09.014},
}
This record lives at https://refs.drheap.org/giese2004taclets/ and will keep doing so.