AR: Self-help Exercises
These are self-help weekly exercises that generaly match the pace of the course. Solutions for each exercise sheet will usually be added one week later.
Note: You should rename the Isabelle files to match the name of their corresponding theories (and remove the .txt file extension).
Week | Title | Files | Solutions |
---|---|---|---|
3 | Exercise Sheet 1: Propositional logic and some Isabelle | [pdf][thy] | |
4 | Exercise Sheet 2: First order logic and more Isabelle | [pdf][thy] | |
5 | Exercise Sheet 3: Representation and reasoning in Isabelle using locales | [thy] | |
6 | Exercise Sheet 4: Structured proofs in Isabelle | [thy] | |
7 | Exercise Sheet 5: Reasoning about Hoare Logic, Induction | [thy] | [pdf][thy1][thy2] |
8 | Exercise Sheet 6: TBC | ||
9 | Exercise Sheet 7: TBC |
Additional Isabelle Exercises
These are additional self-help exercises for you to familiarize yourself with theorem proving in Isabelle. Note that some of the statements that you're asked to prove may overlap with those in the tutorials. You're strongly encouraged to attempt these during the first few Isabelle lab sessions to get some hands-on help.
Acknowledgement: Some of these originate from an annual Isabelle/HOL lab course taught at the Technische Universität München.
Acknowledgement: Some of these originate from an annual Isabelle/HOL lab course taught at the Technische Universität München.
Title | Files | Solutions |
---|---|---|
Propositional logic | [pdf][thy] | [pdf][thy] |
Predicate logic | [pdf][thy] | [pdf][thy] |
A riddle: The rich grandfather | [pdf][thy] | [pdf][thy] |
A Bad Axiomatization | [pdf][thy] | [thy] |
License
All rights reserved The University of Edinburgh