Seminar  Automated Reasoning
Summer Semester 2020
Overview
Title  Seminar  Automated Reasoning 
Semester  Summer Semester 2020 
Module  BachelorSeminar IN0014, MasterSeminar IN2107 
Prerequisites  Attend the kickoff 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 twohundredterabyte 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 kickoff 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 (200250 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.
Handin
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 wellstructured? 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.
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 NPhard. 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 conflictdriven 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 DRATtrim [1] and the preceding DRUPtrim [2] style certificates work and how CDCL solvers can generate them.
References: [1] Wetzler et al.  DRATtrim: Efficient Checking and Trimming Using Expressive Clausal Proofs
[2] Heule  Trimming while Checking Clausal Proofs
Advisor: Lukas Stevens
Propositional Logic  SDCL
Description: Conflictdriven 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 "satisfactiondriven clause learning (SDCL)", in which 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
FirstOrder Logic  Resolution and Superposition
Description: Resolution, as introduced by Robinson [1], is a complete theorem proving method for the unsatisfiability problem of firstorder 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 firstorder resolution. Another student should discuss extensions to firstorder with equality (paramodulation and superposition).
No formal proofs need to be given, but the most important insights and proof techniques should be elaborated.
A selfcontained, extensive summary of resolutionbased algorithms can be found in
[2] by Bachmair and Ganzinger.
References: [1] Robinson  A MachineOriented Logic Based on the Resolution Principle
[2] Bachmair, Ganzinger  Resolution Theorem Proving
Advisor: Kevin Kappelmann
FirstOrder Logic  Tableau
Description: The semantic tableau is a standard proof procedures for a variety of logics, most prominently for propositional and firstorder 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 firstorder logic anymore. Regardless, because the choice of expansions and closures are nondeterministic, 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 firstorder logic and then present implementation details of a specific Tableau Prover or report on common heuristics. Fitting's "FirstOrder Logic and Automated Theorem Proving" [1] gives a good introduction to tableau.
References: [1] Fitting  FirstOrder Logic and Automated Theorem Proving
Advisor: Maximilian P. L. Haslbeck
HigherOrder Logic  Matching and Unification of lambdaterms
Description: These two topics are concerned with solving equations between lambdaterms, called higherorder unification.
 The publication "Proving and applying program transformations expressed with secondorder 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 lambdacalculus" [2] by Huet gives an algorithm to enumerate all unifiers of two lambdaterms. It is a classic.
References: [1] Huet, Lang  Proving and applying program transformations expressed with secondorder patterns
[2] Huet  A unification algorithm for typed lambdacalculus
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 stateoftheart 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 firstorder 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 automatabased approach for deciding it works.
References:
[1] Diophantine equations, Presburger arithmetic and finite automata'
[2] Wolper, Boigelot  An AutomataTheoretic 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 FourierMotzkin elimination. For this topic, the student should give a highlevel 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 Prologstyle 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
Topic Assignment
TBD
Dates
TBD