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)

Ämnesområden

Information Technology

Chalmers infrastruktur