ATP 1

Automated Theorem Proving 1

Winter Semester 2007 - 2008

The course is an introduction to automated reasoning for students in Computer Science and Mathematics. Useful reading:

• Theorema demo (gzipped directory with Mathematica notebooks).
• demo propositional logic (Mathematica notebook).

For viewing the Mathematica notebooks one may use the Mathematica Player (free of charge),

Users of Mathematica can download the Theorema system in order to try out the examples.

A version of propositional logic used for the verification of the propositional prover of Theorema propositional.pdf.

A case study in using level saturation in natural style proving: Case-Study-Irrationality.nb, proof version 0, proof version 1, proof version 2.