Seminars

Many natural computational problems, such as satisfiability and
systems of equations, can be expressed in a unified way as constraint
satisfaction problems (CSPs). In this talk I will show that the usual
reductions preserving the complexity of the constraint satisfaction
problem preserve also its proof complexity. As an application, I will
present two gap theorems, which say that CSPs that admit small size
refutations in some classical proof systems are exactly the constraint
satisfaction problems which can be solved by Datalog.

This is joint work with Albert Atserias.

As an extension of word transformations, tree transformations have numerous applications in computer science : XSLT transformations, Unix packages installation and removal, databases queries... Likewise, there are many formal models to describe these transformations. However, the proof of formal properies on these models is often difficult, or even undecidable.
In this talk, I will be interested in one of the simplest model for tree transformations, namely deterministic top-down tree transducers (DTOP). It has been known for a while that the equivalence problem of DTOPs can be solved via an earliest normal form comparison algorithm, that is in 2EXPTIME. However, when applying this algorithm to practical cases, it seemed that the worst case was not bound to happen often, if ever.
I will present a new algorithm for the problem, based on the search of counterexamples via the expansion and unification of a set of rules over states of DTOPs. The most interesting feature of this algorithm is that it runs in exponential time, thus proving that the equivalence problem of DTOPs is in fact EXPTIME-complete.