Computational Complexity of  Fragments of Halpern-Shoham Logic

Halpern-Shoham logic (HS) is an elegant interval-based temporal logic that introduces one modal operator for each of the well-known Allen relations. The Allen relations form a jointly exhaustive and pairwise disjoint set of binary relations between nonidentical intervals, namely: begins, during, ends, overlaps, adjacent to, later than, and their inverses. The logic is highly expressive, in particular it is strictly more expressive than any point-based temporal logic over linear orders of underlying time structure. On the other hand, HS is undecidable for the most interesting linear orders.

My research is focused on computational complexity of a satisfiability problem in sub-propositional HS languages such as Horn and core fragments. Moreover, I am interested in hybridizing such fragments, i.e., adding the second sort of expressions to the language (the so-called nominals), i.e., primitive formulas each of which is true at exactly one interval, and satisfaction operators indexed by nominals that enable to access a particular interval denoted by this nominal. 

Computational Spatial Reasoning Framework

This is a joint work with M. Bhatt and C. Schultz on spatial and spatio-temporal reasoning framework based on a paradigm of Answer Set Programming Modulo Theories. Our, so-called ASPMT(QS) framework enables to perform hybrid qualitative-quantitative reasoning in contexts of nonmonotonic spatial and spatio-temporal reasoning. It is able to compute indirect and counterfactual effects, use default rules and perform spatial planning. Spatial (and spatio-temporal) relations are encoded as polynomial constraints and as a result the framework enables to express a number of relations from the well-known qualitative spatial reasoning (QSR) approaches (e.g., Interval Algebra, Rectangle Algebra, Region Connection Calculus, Cardinal Directions Calculus).

ASPMT(QS) and other spatial frameworks are vailable at

Artificial Intelligence in Computer Games

The work on an AI program autonomously playing Angry Birds computer game has been accomplished together with M. Zawidzki and T. Lechowski. The program represents objects from a gameplay scene by means of such qualitative relations as "X touches Y", "X lies on Y", "X is a shelter for Y", etc. The main part of the reasoning algorithm consists of a method that enables to compute effects of disappearing objects. In particular, it predicts which blocks will become unstable and will fall down. As a result, the program is able to chose the most valuable shots and successfully play new (never seen before) Angry Birds levels.

The program competed with teams from 12 different countries from 3 continents during Angry Birds AI Competition and won the 5th place.

The developed algorithms are described in a IEEE journal paper Qualitative Physics in Angry Birds.

For a description of AI in Angry Birds Competition see a short movie.