Spring 2015: Automated Theorem Proving (236 714)

Topics in Automated Theorem Proving (236 714): SS 2015

Homepage:
http://cs.technion.ac.il/~janos/COURSES/THPR-2015/index.html
Old Homepage 2013/14:
http://cs.technion.ac.il/~janos/COURSES/THPR/index.html

Lecturer: Prof. J.A. Makowsky
Taub 628, Tel: 4358, e-mail: janos@cs

Format: 2 hours lecture + 1 hour tirgul

Note the change!
Lecture: Wedneday 14:30-16:30 (Starting March 18)
Tirgul: Wednesday 16:30-17:30 (starting March 18)
Place: Taub 401

Last given: By J.A. Makowsky (2013/14, 2006/7, 2003, 1989/90), by Monty Newborn (1992/93)

Prerequisites: Logic for CS (234 292) or Set Theory and Logic (234 293)

Slides for 2015

NEW: : Pointers to Lagrange's Four Square Theorem and Computer Checked Mathematical Theorems.
Lecture Slides by the lecturer used in class.
On the Cruelty of Really Doing Formal Proofs. Slides by J. Harrison from 2010.
Geometric Theorem Proving. Slides by Pedro Quaresma from 2012.

Projects

The Area Method by Chou, Gao and Zhang. Paper by Janicic, Narboux and Quaresma.
Students: Sharon Ron and Adi Sosnovich
Geometry in PROLOG. Paper by Coelho and Pereira.
Highschool Geometry. Paper by Singhal, Henz and McGee.

Participants

Course material for previous Course

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. The most updated reference is:

J. Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009
A. Robinson and A. Voronkov, eds
Handbook of Automated Reasoning, vol. 1 and 2
The MIT Press and North Holland, 2001

Additional references:

Recent papers of interest, to be posted when relevant.
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