Kom ihåg att gruppwebben som samarbetsyta stängs 1 oktober 2026. Du som administratör behöver nu exportera gruppens innehåll och/eller radera gruppen.
Mer information och instruktioner hittar du i nyheten: Gruppwebben som samarbetsyta stängs 1 oktober 2026.
Software needed
In the Interactive Theorem Proving course, the HOL theorem prover is used. For the practical part, you will need to have HOL installed. A description of what you need and how to install it can be found in Exercise 1.
Andreas Linder (andili@kth.se) created a Docker container for HOL. It can be found on https://github.com/andreaslindner/HOL4docker. I myself am unable to help with getting it running, but Andreas can help if you want to use it and have trouble! Thanks Andreas!