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).

WeekTitleFilesSolutions
3Exercise Sheet 1: Propositional logic and some Isabelle [pdf][thy]
4Exercise Sheet 2: First order logic and more Isabelle [pdf][thy]
5Exercise Sheet 3: Representation and reasoning in Isabelle using locales [thy]
6Exercise Sheet 4: Structured proofs in Isabelle [thy]
7Exercise Sheet 5: Reasoning about Hoare Logic, Induction [thy][pdf][thy1][thy2]
8Exercise Sheet 6:  TBC  
9Exercise 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. 
 
TitleFilesSolutions
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