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.

Ämnesord

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

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

Nyckelord

interactive theorem proving

theorem proving

logic

graphical user interface

Publikations- och innehållstyp

art (ämneskategori)

ref (ämneskategori)