**Automated Reasoning**

326.0AR: Lecture (VL), 326.109: Exercises (UE)

Winter Semester 2020

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

Students who take the exercises must mandatorily take the lecture too. It is recommended to take both the lecture and the exercises.

**Automated reasoning** studies methods to automate theorem proving on computers.

Automated theorem proving is the basis for **program verification**,
and for verification of complex systems (e. g. digital hardware) in
general.
As soon as the requirements of a system, as well as the system itself
are expressed in a formal way (programs are already formal!), one can
automatically generate the verification conditions.
These are logical formulae which must be proven in order to be sure that
the system satisfies its requirements.
However, even for relatively small systems these formulae can be quite
large and complex, and proving them by hand is tedious, error prone, and
boring.
Therefore it is necessary to prove them by computer.
Current methods for automated program (system) verification are very
powerful, however they are still not satisfactory for large real life
problems.
It is to be expected, on one hand, that research in this area becomes
more and more important in the future, and on the other hand, that
programmers and other professionals who design complex systems will be
more and more involved in the formalization of the problems,
specifications, and systems, and will have to make more and more use of
automatic tools for verification and proving.

Another important application of automated reasoning is **semantic information storage and retrieval**, like for instance the future **semantic web**.
There are various attempts to define exactly what this means, but our
point of view is that semantic information is stored as a collection of
logical formulae, and retrieval is a special kind of automated reasoning
(or theorem proving).
The specific feature of automated reasoning in this context is
constituted by:
the huge size of the knowledge, the relatively simple structure of the
formulae, and the necessity that retrieval (thus automated reasoning)
must be carried in real time (thus very fast).
Also in this field there is a large need for scientific research, and
also it is expected that in the future a large part of the computer
professionals (e. g. programmers) will be involved in the semantic
formalization of information and in the construction of tools for
semantic information retrieval.

The list of currently available automated reasoning systems is quite large. These are theorem provers for first-order logic or its equational fragment (e.g., Vampire, E, SPASS, Prover9, iProver, leanCoP, E-Darwin, ACL2, Waldmeister, etc.), provers for higher-order logic and mathematical assistant systems (e.g., Isabelle, HOL, Coq, Leo, Nuprl, Theorema, LambdaCLAM, etc.), model builders and SAT solvers (e.g., Mace4, Lingeling family, Boolector, Paradox, Z3, Chaff, PrecoSAT, MiniSAT, CVC3, Barcelogic, SATzilla, etc.), model checkers (e.g., BLAST, CPAchecker, PRISM, SPIN, Vereofy, etc.), termination provers (e.g., AProVE, TTT2, μ-Term, etc.) and many other tools.

Purpose

Understand the main methods and algorithms for automated reasoning, and acquire the skills for applying them on concrete examples. Know and be able to use the main systems and tools for automated theorem proving.

Organization