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:

This material is copyrighted and is available only for the students of this lecture and only for the purpose of study related to it.

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.


T. Jebelean