The course covers interactive theorem proving in higher-order logic and
automated theorem proving in first-order logic. Proofs increase our believe
that some useful property is true. In order to exclude the possibility of
human mistake, it is useful to check proofs by a computer.
Higher-order logic is needed when the proof contains induction, invariants, or
sets. Since automated theorem proving in higher-order logic is very difficult,
implementations of higher-order logic are usually interactive. This means that
such systems can only check the correctness of proofs that the user already
knows. I explain the standard approaches to interactive theorem proving in
higher-order logic, their underlying theory, and existing implementations.
First-order logic is weaker than higher-order logic, but it is easier to
automatically find proofs in it. In fact, existing implementations are quite
succesful in finding difficult proofs. I will explain the most succesful
approaches to automated theorem proving, which are resolution (when there is
no equality) and superposition (when there is equality). I explain the theory,
and implementation techniques. We try out various existing systems, and look
at their implementation.
Automated theorem provers are very complicated pieces of software. Theorem
proving is not only academic exercise. It is used by industry to verify
protocols, parts of safety critical software design, and low level programs.
Grade will be based on an exam and a practical task with equal weight. If you
want to do a master thesis project with me, then this course is a good
preparation.
