Seminar - Automated Reasoning

Summer Semester 2020

Overview

TitleSeminar - Automated Reasoning
SemesterSummer Semester 2020
ModuleBachelor-Seminar IN0014, Master-Seminar IN2107
PrerequisitesAttend the kick-off meeting, send us a short motivation letter (details below) and have a strong interest in formal methods.
WorkloadExpected coursework:
  • 10-page seminar paper
  • two 1-page reviews of other participants' papers
  • 45-minute presentation
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,

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

Furthermore:

As for the reviews:

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

  1. special handling of unit clauses,
  2. different special data structures that enable literal watching and lazy evaluation, etc., and
  3. 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 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

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.

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

Topic Assignment

TBD

Dates

TBD