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.
  • Doing the proof at this point can be challenging.
    • It highly depends on your definitions and your knowledge of the proof system.
    • You should be able to do it at the end of the semester the latest.

Sheet 3

Exercise 1

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

Exercise 2

  • Get used to the idea of using existing types to define new ones.
  • Get used to the idea that sets and predicates are pretty much equivalent.

Exercise 3

  • More exercise in writing, understanding and modifying functional programs and datatypes.
  • Get familiar with proofs, proof commands and proof states in a very simple setting.
  • In general, understand how provers work and how one could implement one.

Sheet 4

  • Basic theory questions you should be able to answer about the HOL core, universes, models, conservative extensions, etc.
  • Exercise 2 (d/e) More and more advanced questions where you can get more familiar with using Isabelle/HOL, proofs, finding and applying theorems, etc.

Sheet 5

Exercise 1

  • Be able to apply methods to rules and do proofs.
  • Get to know the different methods.
  • Get to know more and more rules.
  • Be able to do arbitrary proofs on propositional and predicate logic theorems.

Exercise 2

  • Get familiar with designing and defining both syntax and semantics of languages.
  • First steps towards formulating and proving properties relating models, in this case two language semantics and a compiler.

Sheet 6

  • First steps in finding needed theorems from the library, using the Find Theorems function.
  • First case study about specifying models, properties and proving their consistency.
official/goals.1337852168.txt.gz · Last modified: 2012/05/24 11:36 by paddy