Automated Theorem Proving B: Advanced Proving Methods

Introduction

• Time and place: Thursday 10:15 - 11:45, HT 177F, First lecture on March 9.
• Text Book: Symbolic Logic and Mechanical Theorem Proving (Academic Press, Boston, 1973) by Chin-Liang Chang and Richard Char-Tung Lee
• Additional material will be provided during the lectures and on this home page.
• Prerequisites: In principle, students coming to this lecture should have taken Automatic Theorem Proving A. However, I will also accept other students provided they already have sufficient knowledge or that they are willing to study part A from the textbook.
• Some material will be provided as Mathematica notebooks, which can be visualised using MathReader (free software).
• Some lectures from previous years may help you to get an idea about the contents of the course.

Lectures

• Lecture 1: Mar 9:
  • Motivation: the importance of automated reasoning for the design of complex systems, in particular for program verification and synthesis.
  • Overview of the course:
    • refinements of the resolution method,
    • methods for natural style proving,
    • combining automated reasoning and algebraic computations.
  • Summary of the logical basis: propositional logic, predicate logic.
  • Summary of the resolution method.
• Mar 16: No lecture.
• Lecture 2: Mar 23:
  • Summary of natural style proving.
  • Refining the resolution method.
• Lecture 3: Mar 30:
  • Example of natural style proving zip file.
• Lecture 4: Apr 6:
  • Examples showing the parallelism between resolution and natural style proving.
  • Refining the resolution method: PI resolution.
  • Example from natural style proving where a similar refinement is applied zip file.
• Apr 13: No lecture.
• Apr 20: No lecture.
• Lecture 5: Apr 27: Robert Vajda: The use of Cilindrical Algebraic Decomposition for proofs in Elementary Analysis.
• May 4: No lecture.
• Lecture 6: May 11.
• ...
• Last Lecture: June 29.

  Linear resolution: Cornelius Nevrinceanu zip file.