Topics in Automated Theorem Proving (236 714):
Homepage:
http://cs.technion.ac.il/~janos/COURSES/THPR/announcement.html
or
http://cs.technion.ac.il/~janos/COURSES/THPR/A-thpr.htm
Course material:
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
Lecture: Monday 16:30-18:30
Tirgul: Monday 15:30-16:30
Place: To be announced
Last given:
By J.A. Makowsky (1989/90), by Monty Newborn (1992/93)
Prerequisites:
Logic for CS (234 292) or Set Theory and Logic (234 293)
Course outline:
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.
-
Theorem proving and computer aided mathematics.
General problem solvers vs Special problem solvers.
Guiding problem: Classical geometry.
-
Propositional theorem proving: Solving SAT
Resolution methods:
Analysis of worst case, average case, heuristics.
Other methods
-
First Order Logic and Theorem proving.
Resolution and Unification.
-
Equational logic.
-
Classical geometry.
Course goal:
Exploring the achievements of automated theorem proving.
Introducing topics for
M.Sc. and Ph.D. theses.
Course requirements:
Four homework assignements.
Projects or take home exam.
Literature:
No single textbook covers our approach.
Our course takes material from:
-
Dingzhu Du, Jun Gu and Panos M. Pardalos (eds),
Satisfiability Problem: Theory and Applications, DIMACS Series, vol. 35,
American mathematical Society, 1997
-
David Duffy, Principles of Automated Theorem Proving,
Wiley 1991
-
Shang-Ching Chou, Mechanical Geometry Theorem Proving,
Reidel, 1988
-
Wen-Tsuen Wu, Mechanical Theorem proving in Geometries, Springer 1994
-
B.F. Caviness and J.R. Johnson (eds),
Quantifier Elimination and Cylindrical Algebraic Decomposition,
Springer 1998