Taclets and the KeY Prover

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

Subject headings

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Keyword

interactive theorem proving

theorem proving

logic

graphical user interface

Publication and Content Type

art (subject category)

ref (subject category)