Selected Topics in Automated Reasoning

Exercises

  • Exercise sheet 1: [pdf] (due on May 5, 2009, 9:00)
    Note: Typo in Exercise 1.6 corrected on Thu., April 30, 2009, 17:30.

  • Exercise sheet 2: [pdf] (due on May 14, 2009, 18:00)

  • Exercise session on Monday, May 11, 2009:
    The following proofs needed in the lecture were presented:
  • Theorem 1.11. Let FMS(M) be the family of all finite multisets with elements in the set M. Let > be a strict partial order on M, and let >mul be its multiset extension:
  • >mul is a strict partial order on FMS(M).
  • if > is total then >mul is total.
  • if > is well-founded then >mul is well founded.
  • Proposition 1.12 (i),(ii),(iii)
  • Theorem 1.14.
  • A full proof of the model existence theorem (including proofs of Prop. 1.12) can be found in:

    Bachmair, L. and Ganzinger, H.:
    Resolution Theorem Proving,
    Handbook of Automated Reasoning, North Holland, 2001. [.ps.gz]

  • Exercise sheet 3: [pdf] (due on May 22, 2009, 18:00)

  • Exercise sheet 4: [pdf] (due on June 4, 2009, 18:00)

    Errata to exercise 4: In the supplementary exercise we have to
    assume that the set of constants in Omega is finite, and that the
    clauses do not contain any Skolem functions of arity greater than 0
    (otherwise a finite set of clauses may have infinitely many ground instances).
    Corrected on Fri., June 5 at 20:00; solutions are still accepted until Monday, June 15.

  • Exercise sheet 5: [pdf] (due on June 12, 2009, 17:00)

  • Exercise sheet 6: [pdf] (due on June 19, 2009, 17:00)

  • Exercise sheet 7: [pdf] (due on June 26, 2009, 17:00)

  • Exercise sheet 8: [pdf] (due on July 3, 2009, 17:00)

  • Exercise sheet 9: [pdf] (due on July 10, 2009, 17:00)

  • Exercise sheet 10: [pdf] updated July 12, 2009 (due on July 17, 2009, 17:00)

  • Exercise sheet 11: [pdf] (due on July 24, 2009, 17:00)

    •
    News
  • 20 July 2009 The exercise class is held by Swen Jacobs.
  • 6 July 2009 The exercise class is held by Swen Jacobs.
  • 14 May 2009 The lecture takes place in Room 21, MPI building.
  • 11 May 2009 New time and place for the exercises: Mo.12:30-14:10, Room 21, MPI building.
  • 7 May 2009 Next exercise session: May 11, 12:30-14:10.
  • 23 April 2009
  • Wednesday, 29 April 2009: no exercises
  • Next exercise sheet: Thursday, 30 April 2009.
  • Homework submission:
    • Deadline: Tuesday, 5 May 2009, 9:00 in the morning (at latest)
    • Put your solution into the mail box at the door of room 607 in the MPI building. Please write your name on the solution.
  • Next exercise class: Wednesday, 6 May 2009.