Selected Topics in Automated Reasoning

News
  • 23.07.2009: Lecture will be held by Swen Jacobs.
  • 20.07.2009: Exercise session led by Swen Jacobs.
  • 17.07.2009:Exercise sheet 11: available online.
  • 12.07.2009:Exercise sheet 10: available online.
  • 6.07.2009: Exercise session led by Swen Jacobs.
  • 05.07.2009:Exercise sheet 9: available online.
  • 28.06.2009:Exercise sheet 8: available online.
  • 25.06.2009:
  • d IMPORTANT:
     Due to the Scientific Review of the MPI,
    the lecture on Thursday, 25.06.09 starts
    at 16:30 (15 minutes later than the usual schedule).
  • 20.06.2009:Exercise sheet 7: available online.
  • 13.06.2009:Exercise sheet 6: available online.
  • 05.06.2009:Exercise sheet 5: available online.
  • 29.05.2009:Exercise sheet 4: available online.
  • 16.05.2009:Exercise sheet 3: available online.
  • 14.05.2009: The lecture takes place in Room 21, MPI building.
  • 7.05.2009:Exercise sheet 2: available online (Fri. 8 May 2009).
  • 7.05.2009: New time for the exercises: Mondays, 12:30 - 14:10, Room 21, MPI building.
  • 4.05.2009: Next exercise class: Wednsday, May 6th, 10:00 - 12:00, Room 22, MPI Building.
  • 4.05.2009: The time for the exercises remains for the moment Wednesday, 10:00-12:00.
    (The alternative time slot (Wed, 16:00 - 18:00) discussed on April 30 collides with the Senior Researcher Talks Series at MPI.)
  • 30.04.09 Next lecture: Thursday, May 7th, 16:00 - 18:00, Rotunda 6th floor, MPI Building.
  • 30.04.09 New time for the lecture: Thursdays, 16:00 - 18:00, Room 21, MPI building .
  • 30.04.09 Exercise sheet 1: typo in Exercise 1.6 corrected on Thu., April 30, 2009, 17:30
  • 30.04.09 Exercise sheet 1: available online (Thu. 30 April 2009)
  • Wednesday, 29 April 2009: no exercises
  • Preparatory meeting: Thursday, April 23, 2009, in room 24, MPI building

    • Schedule
  • 23.04.2009: Introductory lecture (motivation, examples, organizatoric issues)
  • 30.04.2009: Propositional logic (syntax; semantics; models, validity, satisfiability, entailment, equivalence; translation to CNF/DNF; checking unsatisfiability: truth tables, resolution)
  • 7.05.2009: Propositional logic (propositional resolution: soundness and completeness; the DPLL method, part I)
  • 11.05.2009: During the exercise session 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]

  • 14.05.2009: The DPLL method, part II; First-order logic (syntax, semantics: models and assignments).
  • 28.05.2009: Models, validity, satisfiability; Entailment and equivalence; Validity vs. unsatisfiability; The theory of a structure; Logical theories (syntactic/semantics view); Algorithmic problems; Normal forms and Skolemization; Herbrand interpretations.
  • 4.06.2009: General resolution (resolution for ground clauses, Robinson's idea; unification, lifting lemma, saturation of sets of general clauses, Herbrand's theorem, the theorem of Löwenheim-Skolem, refutational completeness of resolution, ordered resolution with selection, redundancy).
  • 18.06.2009: Undecidability and decidability results: Goedel's theorem (only statement); some decidable fragments for first-order logic without equality (variable-free formulae, the Bernays-Schoenfinkel class, the Ackermann class); tractability (Horn fragments of the above fragments of FOL). Satisfiability w.r.t. a theory (introduction)
  • 25.06.2009: Satisfiability w.r.t. a theory: Convex theories, T-validity vs. T-satisfiability. Theory of uninterpreted function symbols (motivation, example, Ackermann's reduction)
  • 2.07.2009: Theory of uninterpreted function symbols (optimized satisfiability check using DAGs). Decision procedures for numeric domains: Difference logic (SAT checking expressed as a problem of checking of there are negative cycles in a graph). Survey of methods for reasoning in linear arithmetic, Presburger arithmetic, real numbers. Combinations of theories (introduction).
  • 9.07.2009: The Nelson/Oppen procedure for reasoning in combinations of theories over disjoint signatures.