Automated Reasoning

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

Winter Semester 2015

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

• Language: English
• Lecturers: Tudor Jebelean and Temur Kutsia
• Main lecture: Wed 8:30 to 10:00 in S3 057, weekly from Oct 7.
• Exercises: Tue 12:00 to 13:30 in MT 327, Oct 13, Oct 27, in HT 177F Dec 15, in K 223B Jan 12 19, Jan 26.
• If the lecture does not take place in a certain week, this will be announced on this page.

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

• Oct. 7: Lecture 1:
• Introduction.
• Automated reasoning and its role in the intellectual problem solving cycle.
• Important applications of automated reasoning.
• Overview of the lecture.
• Propositional logic:
• Syntax, semantics.
• Homework 1: ar-hw-1.pdf, ar-hw-1.tex.
• Oct. 13 Exercises 1:
• Computing the truth value: truth tables.
• Semantic based notions: valid, invalid, satisfiable, unsatifiable.
• Oct 14: Lecture 2:
• Semantical logical consequence, semantic equivalence.
• Interesting equivalences, rewriting.
• Normal forms. CNF, the SAT problem.
• Resolution for propositional logic, the DPLL algorithm.
• Homework 1: ar-hw-2.pdf, ar-hw-2.tex.
• Oct 20: no exercises.
• Oct 21: Lecture 3:
• Oct 27: Exercises 2.
• Oct 28: Lecture 4:
• Implementation of the DPLL algorithm.
• Predicate logic: semantics, validity.
• Nov 3: no exercises
• Nov 4: Lecture 5:
• Nov 10: Exercises 3.
• Nov 11: Lecture 6:
• Nov 17: Exercises 4. Overview of the material, questions.
• Nov 18: Lecture 7 - Examination.
• Nov. 25: Lecture 8:
• Reasoning with equality, paramodulation: slides.
• Dec. 2: Lecture 9:
• Reasoning with equality, paramodulation: slides.
• Dec. 9: Lecture 10:
• Dec. 15: Exercises 5.
• Dec. 16: Lecture 11:
• Rewriting-Based Deduction. Completion.