Till KTH:s startsida Till KTH:s startsida

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!

Thomas Tuerk created page 6 April 2017

Administrator Thomas Tuerk changed the permissions 19 April 2017

Kan därmed läsas av alla och ändras av alla inloggade användare.
Thomas Tuerk edited 5 May 2017

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!¶