Andrei Koltsov (Mar 26 2023 at 15:35): Andrei Koltsov (Mar 26 2023 at 15:35):I have begun with "Programming and Proving in Isabelle/HOL". I can see that Isabelle/HOL language looks like SML but it is not SML anyway. Where to find a description of Isabelle/HOL language and simple working exemples to test my understanding of it? Without them I'm going through tutorial rather intuitivly and can't use Isabelle/HOL language without lots of simple sintaxic errors. Maybe there is some better ways to study Isabelle?
waynee95 (Mar 26 2023 at 15:49):Not affiliated with the course or anything and neither did I take it in person, but I found the slides to be very helpful as they provide a bit more in-depth information about Isabelle and Isabelle/HOL: http://cl-informatik.uibk.ac.at/teaching/ss19/itp/content.php
To better understand natural deduction proofs in Isabelle/Isar I found this to be very useful https://ap5.fas.nus.edu.sg/fass/phibrkb/document.pdf
Here you can find a lot of exercises with solutions (although it uses an older version of Isabelle but for the most part, they seemed to work fine) https://isabelle.in.tum.de/exercises/
Last updated: Apr 20 2024 at 04:19 UTC