Topics in Automated Theorem Proving (236 714): WS 2013/14
Old Homepage 2006/7:
NEW: Course material for 2013/14:
Notes on logic
Slides of Lecture 2 (revised October 24, 2013)
Slides of Lecture 3 (posted November 1, 2013)
Slides of Lecture 4 and 6 (posted November 23, 2013), without Lecture 5
Slides of Lecture 7 (posted November 23, 2013, on Geometry)
Slides of Lecture 8 (posted December 23, 2013, on QE in ACF_0)
Course material from 2003:
Old Lecture notes
Chapter 3 of the book
with proof of Tarski's theorem.
Lecturer: Prof. J.A. Makowsky
Taub 628, Tel: 4358, e-mail: janos@cs
Format: 2 hours lecture + 1 hour tirgul
NEW TIME AND LOCATION
Lecture: Thursday 10:30-12:30 (Starting October 17)
Tirgul: Thursday 09:30-10:30 (starting October 24)
Place: Taub 4
By J.A. Makowsky (2006/7, 2003, 1989/90), by Monty Newborn (1992/93)
Logic for CS (234 292) or Set Theory and Logic (234 293)
Automated theorem proving is used in two rather different ways.
Universal formalisms are used in Artificial Intelligence
and Databases to automatize deductive systems in general data and
knowledge processing. The Highly specialized formalisms are used
in well structured applications such as computational geometry
and other branches of computer aided mathematics.
We shall study both approaches in a certain depth.
Exploring the achievements of automated theorem proving.
Theorem proving and computer aided mathematics.
General problem solvers vs Special problem solvers.
Guiding problem: Classical geometry.
Propositional theorem proving: Solving SAT
Analysis of worst case, average case, heuristics.
First Order Logic and Theorem proving.
Resolution and Unification.
Introducing topics for
M.Sc. and Ph.D. theses.
Four homework assignements.
Projects or take home exam.
No single textbook covers our approach.
The most updated reference is:
Our course takes material from volume 1:
A. Robinson and A. Voronkov, eds
Handbook of Automated Reasoning, vol. 1 and 2
The MIT Press and North Holland
Chapters 1, 2, 8, 9, 11, 12
Recent papers of interest, to be posted when relevant.
Shang-Ching Chou, Mechanical Geometry Theorem Proving,
Wen-Tsuen Wu, Mechanical Theorem proving in Geometries, Springer 1994
B.F. Caviness and J.R. Johnson (eds),
Quantifier Elimination and Cylindrical Algebraic Decomposition,