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:
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.