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

• Time: Wed 8:30 to 10:00
• Place: BA 9907
• Language: English
• Lecturers: Tudor Jebelean and Temur Kutsia
• First lecture: Oct 9 (There is no lecture on Oct 2.)
• 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.

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. 2: No lecture.
• Oct. 9: 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.
• Exercise 1: ar-hw-1.pdf, ar-hw-1.tex.
• Oct. 16: Lecture 2:
• Resolution in Propositional Logic:
• Equivalence, rewriting, normal forms.
• The resolution principle for propositional logic, correctness.
• Exercise 2: ar-hw-2.pdf, ar-hw-2.tex.
• Oct. 23: Lecture 3:
• Predicate Logic:
• The syntax of first order predicate logic: terms and formulae.
• The semantics of first order predicate logic: interpretations, computing the truth value.
• Material: slides, examples.
• Exercise 3: ar-hw-3.pdf, ar-hw-3.tex.
• Oct. 30: Lecture 4:
• Predicate Logic:
• Equivalences of quantified formulae.
• Normal forms: prenex, Skolem, standard.
• Nov. 6: Lecture 5:
• Resolution in Predicate Logic:
• Substitutions, unification.
• The resolution principle for predicate logic, correctness.
• Material: slides, examples.
• Nov. 13: Lecture 6:
• Completeness of Resolution. SAT solving.
• Herbrand universe, Herbrand interpretations, semantic tree, Herbrand theorem.
• Completeness of resolution in predicate logic.
• The DPLL method for SAT solving.
• Nov. 20: Lecture 7:
• Equality:
• Reasoning with equality.
• Paramodulation.
• Nov. 27: Lecture 8:
• Equality:
• Reasoning with equality.
• Paramodulation.
• Material: slides.
• Dec. 4: Lecture 9: :
• Dec. 11: Lecture 10:
• Jan. 8: Lecture 11:
• Systems:
• SAT/SMT solvers. Presentation by Klaus Reisenberger.
• Jan. 14: Exercise session. Room S2 219. 15:30-17:00:
• Systems:
• Termination provers. Presentation by René de Alvarado
• Jan. 15: Lecture 12:
• Systems:
• Theorem prover Vampire. Presentation by Stefan Amberger
• Jan. 21: Exercise session. Room S2 219. 15:30-17:00:
• Systems:
• Mathematical Assistants. Presentation by Wolfgang Stockinger
• Jan. 22: Lecture 13:
• Systems:
• Mathematical Assistants.
• Jan. 29: Examination.

Literature

• Chin-Ling Chang, Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press. 1973.
• Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press. 1998.
• Robert Nieuwenhuis and Albert Rubio. Paramodulation-Based Theorem Proving. In: Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning. Volume 1, pp. 371-443.
• L. Bachmair and H. Ganzinger, Equational Reasoning in Saturation-Based Theorem Proving, Chapter 11 of vol. I of Automated Deduction - A Basis for Applications, W. Bibel and P. Schmitt, eds., pp. 353-397, Kluwer, 1998.

T. Jebelean, T. Kutsia.