CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Taclets and the KeY Prover

Martin Giese (Institutionen för datavetenskap, Formella metoder)
Electronic Notes in Theoretical Computer Science (1571-0661). Vol. 103 (2004), p. 67-79.
[Artikel, refereegranskad vetenskaplig]

We give a short overview of the KeY prover---which is the proof system belonging to the KeY tool---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.

Nyckelord: logic, theorem proving, interactive theorem proving, graphical user interface

Denna post skapades 2006-09-28. Senast ändrad 2013-08-12.
CPL Pubid: 2344


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap, Formella metoder (2002-2004)


Information Technology

Chalmers infrastruktur