Automated Reasoning, Spring 2007

Slides

• Slides to propositional resolution, either as ps or pdf .
• Slides for resolution in predicate logic, either as ps or pdf .
• Slides on superposition, either as ps or pdf .
• Slides on the transformation from first-order logic to clause logic, either as ps or pdf .
• Slides on propositional logic (DPLL), either as ps or pdf .

Exercises

• Excersice for May 24th, as ps or pdf .
• Exercise for May 31st, as ps or pdf .
• Exercises for June 14th, as ps or pdf .
• Exercises for June 21st, as ps or pdf .

Schedule

• 7 June, no lecture. (also not on 4th of June)
• 14 June, 16.00, lifting, superposition.
• 15 June, 14.00, examples of superposition, completeness proof.
• 21 June, 16.00, clause transformations, system demonstration.
• 22 June, 14.00, propositional logic, DPLL with learning. Applications in finite model search.

Literature

• Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov, North Holland Publishing Company, Chapters 2,5,6,7. (The other chapters are also interesting, but they do not stand in close relation with the topics of the lecture)
• Symbolic Logic and Mechanical Theorem Proving, C.-L. Chang and R.C.-T. Lee, Academic Press, 1973. (A bit old, but very readable)
• William McCune, Prover 9. Manual and Download .
• Hans de Nivelle, Marc Bezem, reader for ESSLLI 2006, Introduction to Automated Reasoning, ps or pdf .
• Niklas Een, Niklas Soerensson, The MiniSat Page . Minisat is one of the best propositional provers, and it is very well documented. The paper 'An existensible SAT-solver' is excellent.