Automated Reasoning
326.0AR: Lecture (VL), 326.094: Exercises (UE)
Winter Semester 2013
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, Paradox, Boolector, Z3, Chaff, PrecoSAT, MiniSAT, CVC3, Barcelogic, SATzilla, etc.), model checkers (e.g., BLAST, 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
If the lecture does not take place in a certain week, this will be announced on this page.
The schedule of the exercises will be agreed with the participants at the first lecture.
Starting from December 10, exercises with Temur Kutsia will be organized on Tuesdays, 15:30-17:00, room S2 219.
Grading
The contents of the lecture consists half in theoretical presentations and half in practical work with automated reasoning systems. There will be a written examination for the theoretical part at the last lecture. For the system related part, each student will choose a certain tool, will train with it and will make a presentation of it during the lecture. The grade for the lecture will be based 50% on the system presentation, and 50% on the solution to the written examination for the theory part.
In the exercises we will solve problems related to the lecture: for both the theoretical part and the systems part. Grading will be based on the submitted solutions and on the activity during the class.
Lectures
Literature