Below are several ideas that can form the starting point for a student research project that I would be happy (and capable) to supervise. These ideas all have a reasonably concrete research question as starting point, and they are (likely) feasible to carry out.

These projects are suitable for, for example, an small research project or a thesis project (in the context of the MSc Logic or the MSc Artificial Intelligence at the UvA).

Please get in touch with me (Ronald de Haan) if you are interested in any of these projects, or if you have questions about any of them.

 

1. Developing a reasoning algorithm for BSML

Bilateral state-based modal logic (BSML) is a modal logic that has been used, for example, in recent work by colleagues on pragmatics.

I have built a (rough) prototype for a reasoning algorithm for BSML that is based on answer set programming. This prototype can reason about small formulas in a reasonable amount of time. In terms of how well this algorithm (and variants of it) scales to larger formulas, much remains to be explored.

There are a lot of directions for improving this reasoner, and many of them are very much suitable for a small research project or a thesis. For some suggestions for research directions, see the demonstration of the prototype.

  • The project requires a solid understanding of answer set programming. Students that have taken the course Knowledge Representation and Reasoning at the UvA are well prepared for this.
  • The project also requires a basic understanding of modal logic.
  • The project is algorithmic in nature, and involves some programming in Python.

 

2. Testing a declarative method to specify CEGAR-algorithms

Counterexample-guided Abstraction Refinement (CEGAR) algorithms often provide a productive method for solving problems at higher levels of the Polynomial Hierarchy (PH). In the context of SAT solving or answer set solving (for problems at the second level of the PH), this type of algorithm typically looks as follows. One solver is given an encoding of candidate solutions to the problem (the abstraction), and it starts the search process and iterates over candidate solutions. There is a second solver that is running, which is given an encoding that expresses what counterexamples for candidate solutions should satisfy. Each candidate solution produced by the first solver is given to the second solver, in the form of assumptions. If the second solver does not find a counterexample, the candidate solution is returned as an actual solution. If the second solver does find a counterexample, this counterexample is used to produce a new constraint (a refinement) that is added to the first solver, and the first solver's search process continues.

The encodings given to the first and second solver in this architecture are typically specified declaratively, using propositional logic or logic programs. The way in which refinements are produced from counterexamples are mostly given in a procedural way—e.g., in the form of a subalgorithm that produces a constraint from a counterexample. If these refinements were also specified declaratively—e.g., by just stating the properties that define them—the entire algorithm specification could be more readable and easier to modify.

This research project involves studying to what extent solving search problems at the second level of the PH by declaratively specified CEGAR-style algorithms leads to more readable (and more easily adaptable) encodings, while not giving up too much in terms of algorithmic efficiency.

There is a prototype system available, based on answer set programming, that can be used as a starting point.

  • This project requires a solid understanding of answer set programming. Students that have taken the course Knowledge Representation and Reasoning at the UvA are well prepared for this.
  • The project is algorithmic in nature, and involves some programming in Python.

 

3. Arbitrary propositional formulas under answer set semantics

Disjunctive answer set programming (dASP) is expressive enough to model search problems at the second level of the Polynomial Hierarchy (PH). Intuitively, these problems can be expressed using an "∃∀"-quantified statement. However, expressing such problems in dASP typically leads to unnatural (and unreadable) encodings.

Answer set (or stable model) semantics has also been defined for arbitrary (propositional) logic formulas—instead of just for disjunctive logic programs, that can be seen as conjunctions of implications of a particular form. In terms of expressive power and succinctness, disjunctive logic programs and general propositional formulas are equivalent under answer set semantics.

This research project involves studying to what extent expressing natural search problems at the second level of the PH using general propositional formulas (under answer set semantics) leads to easier-to-understand and more natural encodings.

Optionally, the project can also include developing (ASP-based) algorithms for general propositional formulas under answer set semantics, and studying whether problems can be solved (more) efficiently using the developed problem encodings.

  • This project requires a solid understanding of answer set programming. Students that have taken the course Knowledge Representation and Reasoning at the UvA are well prepared for this.
  • This project also requires a basic understanding of computaitonal complexity theory. Students that have taken the course Computational Complexity at the UvA are well prepared for this.
  • This project is mostly theoretical in nature, and affinity with logic is recommended.
  • This project can also have an algorithmic aspect, which would involve some programming in Python.