Seminar - Automated Reasoning
Summer Semester 2020
Overview
| Title | Seminar - Automated Reasoning |
| Semester | Summer Semester 2020 |
| Module | Bachelor-Seminar IN0014, Master-Seminar IN2107 |
| Prerequisites | Attend the kick-off meeting, send us a short motivation letter (details below) and have a strong interest in formal methods. |
| Workload | Expected coursework:
|
| Organization | Maximilian P. L. Haslbeck, Kevin Kappelmann, Tobias Nipkow |
Content
Picture by Ilya Yodovsky Jr.
(taken from Decision Procedures by D. Kroening and O. Strichman)
Broadly speaking, automated reasoning is concerned with building computer systems that infer new knowledge and valid inferences in a given environment. For example,
- SAT solvers were used to find the first proof for the Boolean Pythagorean triples problem. The two-hundred-terabyte proof certificate is the biggest proof in existance.
- SMT solvers are commonly used to automatically verify computer software (e.g. see Dafny).
- Interactive Theorem Provers (ITPs) are routinely used to mechanically check proofs (e.g.: the Kepler Conjecture was formalized in the Flyspeck project). Automated theorem provers (ATP) are an integral part of ITPs that allow for these large scale formalizations.
Automated reasoning has matured into one of the most advanced areas of computer science. It is used in many areas of the field, including software and hardware verification, logic and functional programming, formal methods, knowledge representation, deductive databases, and artificial intelligence. This seminar gives an overview of the fundamental ideas, techniques, and methods in automated reasoning and its applications.
In this seminar every participant will receive a topic. The student is expected to write a paper about the topic and give a presentation to the other participants about it. Also, every participant will be required to give a short written review of the papers of two other participants. The precise schedule will be made available below.
Application
The application will be through the Matching Platform. There will be a kick-off meeting Thursday January 30 at 1 pm in 00.09.038 (Turing) explaining details about the seminar. Priority will be given to students that attended the meeting and provide the following information.
The seminar can be attended by both Bachelor's and Master's students. Each topic below has a few subtopics. A student shall select one of those subtopics for his/her seminar.
Required Short Text
Please send a short explanation (200-250 words) why you wish to attend the seminar, which topics you are interested in and why. If you already have some experience with ATPs let us know as well. Send it to Maximilian P.L. Haslbeck by February 13.
Language
This seminar is held in English. The scientific paper, the review as well as the presentation should be held in English.
Hand-in
All the documents due should be sent to Maximilian P.L. Haslbeck.
Formal requirements
Participants must hand in
- a complete (!) paper draft three weeks before their presentation to both Maximilian P.L. Haslbeck and their advisor; this will be reviewed by other students and the advisor
- a draft version of their presentation slides to their advisor one week before their talk
- the final versions of their paper and presentatio to both Maximilian P.L. Haslbeck and their advisor on the day of the presentation.
- reviews of the two papers they were assigned within one week before the respective presentation to Maximilian P.L. Haslbeck
Furthermore:
- The length of the paper should be roughly 10 pages.
- The length of the talk between 35 and 45 minutes (excluding Q&A session) and must not exceed 45 minutes.
- Reviews, presentations, and papers should be in English.
- There are no strict requirements on the form of the paper or slides. No template will be provided.
- All submissions are to be sent to Maximilian P.L. Haslbeck.
As for the reviews:
- Reviewers receive the drafts of their assigned topics as soon as they are handed in.
- The main focus of the reviews should be the content and the presentation of the papers. Does it make sense? Is it well-structured? Is it understandable to someone who has not read the source material?
- Reviewers are not expected to read the cited source material.
- Spelling and grammar may also be mentioned, but are less important.
- A summary of the reviewed topic is not required.
- Reviews should be roughly one page long
- Reviewers may freely decide whether to use full sentences or bullet points.
The final grade is composed as follows: 20% Reviews written + 40% Presentation + 40% Paper
Assignment of Seminar Topics
The assignment of seminar topics will be based on students' preferences. Details will be announced later.
Topic Assignment
| # | Name | Topic | Advisor | Paper |
|---|---|---|---|---|
| 1 | Alexander Schlenga | SAT - CDCL | Mohammad Abdulaziz | [pdf] |
| 2 | Mira Trouvain | FOL - Tableaux | Lukas Stevens | [pdf] |
| 3 | Ralitsa Dardjonova | FOL - Resolution and Superposition | Kevin Kappelmann | [pdf] |
| 4 | Johannes Neubrand | Knowledge Representation - Prolog systems | Jonas Rädle | [pdf] |
| 5 | Fabian Huch | HOL - Matching and Unification of lambda-terms | Tobias Nipkow | [pdf] |
| 6 | Lukas Koller | SMT - EUF | Simon Wimmer | [pdf] |
| 7 | Florian Märkl | SMT - Bit Vectors | Julian Brunner | [pdf] |
| 8 | Florian Sextl | SMT - A decidable fragment of Separation Logic | Max Haslbeck | [pdf] |
| 9 | Nhat Minh Hoang | Presburger Arithmetic | Manuel Eberl | [pdf] |
Dates
Deadlines for The Paper Drafts
Date: 19.05.2020 (topics 1, 2)
Date: 26.05.2020 (topics 3, 4)
Date: 02.06.2020 (topics 5, 6)
Date: 09.06.2020 (topic 7)
Date: 16.06.2020 (topics 8, 9)
Deadlines for The Slide Drafts
Date: 02.06.2020 (topics 1, 2)
Date: 09.06.2020 (topics 3, 4)
Date: 16.06.2020 (topics 5, 6)
Date: 23.06.2020 (topic 7)
Date: 30.06.2020 (topics 8, 9)
Deadlines for The Reviews
Every student will get two papers to review between 19.05. and 16.06. and will be supposed to submit each review within two weeks.
Deadlines for The Video Presentations
Date: 07.06.2020 (topics 1, 2)
Date: 14.06.2020 (topics 3, 4)
Date: 21.06.2020 (topics 5, 6)
Date: 29.06.2020 (topic 7)
Date: 05.07.2020 (topics 8, 9)
Presentations and Deadlines for The Final Paper Versions
Date: 09.06.2020 (topics 1, 2)
Date: 16.06.2020 (topics 3, 4)
Date: 23.06.2020 (topics 5, 6)
Date: 30.06.2020 (topic 7)
Date: 07.07.2020 (topics 8, 9)
Time: 12:00 - 14:00
Place: MI 00.09.038 (Turing) or online
Topics
Propositional SAT - DPLL
Description: Searching and backtracking is a standard way to solve combinatorial problems. For SAT, DPLL is a successful search and backtracking techniques that has special optimisations geared towards proprositional satisfiability. These include
- special handling of unit clauses,
- different special data structures that enable literal watching and lazy evaluation, etc., and
- lookahead search and different heuristics to select propositions on which to branch, such as VSIDS.
In this topic, the student will need to present the details of a DPLL optimisation.
References: [1] Biere et al. - Handbook of Satisfiability
[2] Knuth - The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6
Advisor: Mohammad Abdulaziz
Propositional SAT - Resolution
Description: Resolution is refutation technique that can be used for propositional logic. Although plain resolution is not practically the most successful method for solving propositional satisfiability problems, ideas from it were used to improve other SAT solving techniques. However, an interesting set of results concerning resolution show lower bounds on sizes of resolution proofs for different sets of clauses. In a classical paper, it was shown that the pigeon hole problem has no tractably short resolution proofs. Also, it was shown that, for pigeon hole problems, resolution proofs can be made much shorter by adding clauses to the given SAT problem, as in the case of extended resolution or symmetry breaking clauses. Another interesting recent result shows that finding the a resolution proof that is at most polynomially longer than the shortest proof is NP-hard. In this topic, the student will need to present the details of a lower bound for a class of clauses, a method that improves that lower bound, or the complexity of finding shortest resolution proofs.
References: [1] Biere et al. - Handbook of Satisfiability
[2] Knuth - The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6
Advisor: Mohammad Abdulaziz
Propositional SAT - CDCL
Description: A successful class of SAT solvers is based on clause learning. It merges ideas from DPLL, like literal watching, as well as from resolution, like the fact that adding clauses can make the proofs of unsatisfiability shorter. The most famous of those algorithms is Conflict Driven Clause Learning (CDCL). In this topic, the student needs to present the basic ideas used in a CDCL solver.
References: [1] Biere et al. - Handbook of Satisfiability
[2] Knuth - The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6
Advisor: Mohammad Abdulaziz
Propositional Logic - DRAT/DRUP
Description: A SAT solver searches for a variable assignment that makes the given formula true.
It can therefore easily certify a successful proof search by outputting the assignment.
But what if the formula is unsatisfiable?
In the case of conflict-driven clause learining (CDCL), which is the leading paradigm in SAT solving, unsatisfiability can be certified by emitting all clauses that were learned until the empty clause was derived from a conflict.
For certain formulas, however, it is known that this certificate requires exponentially many clauses in the number of input clauses.
Therefore, it is important to consider the problem of generating certificates that are short, easy for the solvers to emit, and efficiently checkable.
The student should explain how DRAT-trim [1] and the preceding DRUP-trim [2] style certificates work and how CDCL solvers can generate them.
References: [1] Wetzler et al. - DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
[2] Heule - Trimming while Checking Clausal Proofs
Advisor: Lukas Stevens
Propositional Logic - SDCL
Description: Conflict-driven clause learning (CDCL) relies resolution to learn new clauses that preserve satisfiability; however, any clause that is redundant, i.e. preserves satisfiability, could, in principle, be added to the formula.
For this to be efficient, we have to restrict clause learning to a class of clauses where the redundancy is polynomially decidable.
The publication "Short Proofs Without New Variables" [1] introduces a such a redundancy criterion leading to a proof system that is strong even without the introduction of new variables.
This proof system also gave rise to a new paradigm in SAT solving, namely "satisfaction-driven clause learning (SDCL)", in the solver uses blocking clauses to aggressively prune the search space.
The student should explain the PR proof system and how clauses that are learned via PR can be used for pruning.
References: [1] Heule - Short Proofs Without New Variables
[2] Heule - PRuning Through Satisfaction
Advisor: Lukas Stevens
First-Order Logic - Resolution and Superposition
Description: Resolution, as introduced by Robinson [1], is a complete theorem proving method for the unsatisfiability problem of first-order logic, and undeniably, it builds the foundation of some of the most successful automated theorem proving procedures.
One student is expected to give an overview of propositional and binary first-order resolution. Another student should discuss extensions to first-order with equality (paramodulation and superposition).
No formal proofs need to be given, but the most important insights and proof techniques should be elaborated.
A self-contained, extensive summary of resolution-based algorithms can be found in
[2] by Bachmair and Ganzinger.
References: [1] Robinson - A Machine-Oriented Logic Based on the Resolution Principle
[2] Bachmair, Ganzinger - Resolution Theorem Proving
Advisor: Kevin Kappelmann
First-Order Logic - Tableau
Description: The semantic tableau is a standard proof procedures for a variety of logics, most prominently for propositional and first-order logic. The procedure expands the goal and clears away the inessential details of its logical structure. It maintains and expands a tableau, essentially a tree where nodes are labelled with subformulas, until no further operation can be applied or a contradiction in every branch is found.
While in propositional logic the tableau method could be used as decision procedure, this will certainly not work in first-order logic anymore. Regardless, because the choice of expansions and closures are non-deterministic, there is lots of room for heuristics and the method performs well in practice.
The student should first explain the tableau approach for propositional logic, then its extension to first-order logic and then present implementation details of a specific Tableau Prover or report on common heuristics. Fitting's "First-Order Logic and Automated Theorem Proving" [1] gives a good introduction to tableau.
References: [1] Fitting - First-Order Logic and Automated Theorem Proving
Advisor: Maximilian P. L. Haslbeck
Higher-Order Logic - Matching and Unification of lambda-terms
Description: These two topics are concerned with solving equations between lambda-terms, called higher-order unification.
- The publication "Proving and applying program transformations expressed with second-order patterns" [1] considers a simple form of the problem where function types are restricted and only the variables on one side of the equation, the pattern, are instantiated.
- The paper "A unification algorithm for typed lambda-calculus" [2] by Huet gives an algorithm to enumerate all unifiers of two lambda-terms. It is a classic.
References: [1] Huet, Lang - Proving and applying program transformations expressed with second-order patterns
[2] Huet - A unification algorithm for typed lambda-calculus
Advisor: Tobias Nipkow
SMT - Equality Logic with Uninterpreted functions
Description: An effective implementation of the theory of equalities with uninterpreted functions (EUF) lies at the heart of any of today's successful SMT solvers.
Chapter 4 of the book "Decision Procedures" [1] by Kroening and Strichmann provides a gentle introduction to the topic.
This seminar talk should present the basics of the theory,
the essential congruence closure algorithm,
and at least one advanced topic, such as practical implementations in
today's state-of-the-art SMT solvers or applications in hardware verification.
References: [1] Kroening, Strichmann - Decision Procedures
Advisor: Simon Wimmer
SMT - A decidable fragment of Separation Logic
Description: Separation logic is an important approach to reasoning about programs that manipulate pointer structures. Berdine et al. present "a decidable fragment of Separation Logic" [1] and study decision procedures for validity of entailments.
References: [1] Berdine et al. - A decidable fragment of Separation Logic
Advisor: Maximilian P. L. Haslbeck
SMT - Bit Vectors
Description: In software, arithmetic is often performed on binary
number representations of fixed length. As such, reasoning about this
is an important part of software verification. Chapter 6 of the book
"Decision Procedures" [1] by Kroening and Strichman provides an
introduction to the topic of bit vectors in SMT solvers. The student
should give an overview of the basic concepts and outline the
associated decision procedure as well as how it can be extended and
improved upon.
References: [1] Kroening, Strichmann - Decision Procedures
Advisor: Julian Brunner
Presburger Arithmetic
Description: Presburger arithmetic consists of all formulae that can be made from linear constraints on integers (e.g. 2x ≤ 3y or x + y ≤ z) and first-order predicate logic (∧, ∨, ¬, ∀, ∃). This is a decidable theory, i.e. there are decision procedures that decide in finite time if a given such formula is true or not. One particularly intuitive method for this uses finite automata.
The student should explain what Presburger arithmetic is and how the automata-based approach for deciding it works.
References:
[1] Diophantine equations, Presburger arithmetic and finite automata'
[2] Wolper, Boigelot - An Automata-Theoretic Approach to Presburger Arithmetic Constraints
[3] Esparza - Automata Theory (lecture notes)
Advisor: Manuel Eberl
Linear Arithmetic
Description: Various methods exist to decide the feasibility of systems of linear equations over real or integer numbers, such as the simplex method or Fourier-Motzkin elimination. For this topic, the student should give a high-level overview of the different methods and explain one or two of them in greater detail. A good resource for this topic is the book on Decision Procedures [1] by Kroening and Strichman.
References: [1] Kroening, Strichmann - Decision Procedures
Advisor: Manuel Eberl
Knowledge Representation - Prolog systems
Description: Prolog is the name of a family of logic programming systems. This talk should explain how these systems work by introducing the SLD calculus (a restricted form of resolution) and its extension to negation as failure, the SLDNF calculus. Negation as failure introduces nonmonotonicity to logic programs, which means that - in contrast to classical logics - adding new axioms to a theory may force the retraction of conclusions that were obtained using a more limited set of axioms. The student should explain nonmonotonicity and why it is useful in knowledge representation, for instance by introducing the frame problem [1].
Possible source material: Harrison's "Handbook of Practical Logic and Automated Reasoning" [2] has a short section on Prolog and the SLD calculus. "Foundations of Logic Programming" [3] by Lifschitz is a detailed survey of the semantics of Prolog-style systems. It includes a description of the SLDNF calculus. Another survey is "Knowledge Representation with Logic Programms" [4] by Brewka and Dix, which also includes more advanced discussions of the connection between knowledge representation and logic programming.
References: [1] Lifschitz - The Dramatic True Story of the Frame Default
[2] Harrison - Handbook of Practical Logic and Automated Reasoning
[3] Lifschitz - Foundations of Logic Programming
[4] Brewka, Dix - Knowledge Representation with Logic Programms
Advisor: Jonas Rädle