User Tools

Site Tools


official:goals

This is an old revision of the document!


Goals of the Exercises

This page is intended to give you an idea of what you should have learned from the exercises. Please be sure to check all the goals and spend additional time on the exercises if you do not meet them yet.

The exercise meetings are intended to give you time to solve the exercises under supervision and often also introduce new things. You should at least prepare the exercises which are marked accordingly and send in the solutions. Eventually, you should be able to solve all the exercises and you should spend as much additional time at home as you need to finish them. You are encouraged to ask questions either in person or per email at any point in time.

Sheet 1

  • Get familiar with the calculi, axioms, rules and what a proof is.
  • Be able to do pen and paper proofs.
  • Be able to translate your proofs to Isabelle/HOL, using a fixed pattern.
  • Make first steps with the tool/editor Isabelle/HOL/Emacs.

Sheet 2

Exercise 1

  • Be able to write basic Isabelle/HOL functions and recursive functions.
  • Get familiar with functional programs, so you can at least read more complex programs.

Exercise 2

  • Be able to specify properties of functions in Isabelle/HOL.
  • Be able to prove many of these properties with a simple proof pattern.
  • First steps in finding missing lemmas from proofs which are not working yet.

Exercise 3

  • More advanced example.
  • Be able to define the algorithm and specify its correctness.
official/goals.1335361864.txt.gz · Last modified: 2012/04/25 15:51 by paddy