~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[seminaires:laag:index|Logique, automates, algèbre et jeux]]\\
Jeudi 16 juin 2016, 10 heures 30, 4033\\
**Florent Capelli** (Liafa) //Lyndon’s theorem//
<button type="link" size="xs" collapse="b23-3777">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b23-3777" collapsed="true">
<well size="sm">
A first-order formula is positive if it does not contain any negations. It is not so difficult to prove that such formulas are preserved under surjective homomorphism, meaning that if some model M satisfies it, and there is a surjective homomorphism from M onto M′, then M′ also satisfies the formula. Lyndon’s theorem states that all first-order formulae preserved in this way are equivalent to a positive formula. Hence, Lyndon’s theorem characterizes syntactically this preservation property. Statement of similar forms are usually called ‘preservation theorems’. This theorem, as it is often the case for preservation theorems for first-order is not true in the finite: this signifies that there are first-order formulae which are preserved under surjective homomorphism between finite models, but are not equivalent to any positive formula.

In this presentation, we will give a panorama of various classical preservation theorems for first-order logic. We will then present a proof of Lyndon’s theorem, and a proof that it does not hold in the finite case (this last construction is a joint work with Arnaud Durant, Amélie Gheerbrant and Cristina Sirangelo).
</well>
</collapse>


[[seminaires:laag:index|Logique, automates, algèbre et jeux]]\\
Jeudi 4 février 2016, 10 heures 30, 4033\\
**Christoph Haase** (LSV) //A Survey on Classical and Novel Results on Presburger Arithmetic//
<button type="link" size="xs" collapse="b23-3778">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b23-3778" collapsed="true">
<well size="sm">
Presburger arithmetic is the first-order theory of the natural numbers with addition and order. This theory was shown decidable by M. Presburger in 1929. In the 1960s, Presburger arithmetic was studied in the context of formal language theory. Two of the main results from this period are that the sets of natural numbers definable in Presburger arithmetic are the so-called semi-linear sets, and that Parikh images of languages generated by context-free grammars are semi-linear and hence Presburger-definable. Subsequently, from the 1970s onwards the computational complexity of Presburger arithmetic received interest. The landmark results from this period are a doubly exponential lower bound shown by Fischer and Rabin in 1974 and a triply-exponential upper bound shown by Oppen in 1978. The 1980ies brought a more fine-grained complexity analysis of (fragments of) Presburger arithmetic by Fürer, Grädel and Scarpellini. In this talk, I will survey those classical results and show the relevant proofs or proof ideas for most of them. I will in depth discuss a recent result that shows that Presburger arithmetic with a fixed number of quantifier alternations is complete for every level of the weak EXP hierarchy. If time permits, I will discuss some recent work in which Presburger arithmetic has been used for showing new lower bounds for equivalence problems for commutative grammars.
</well>
</collapse>


[[seminaires:laag:index|Logique, automates, algèbre et jeux]]\\
Jeudi 21 janvier 2016, 10 heures 30, 4033\\
**Christoph Haase** (LSV) //A Survey on Classical and Novel Results on Presburger Arithmetic//
<button type="link" size="xs" collapse="b23-3779">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b23-3779" collapsed="true">
<well size="sm">
First part
</well>
</collapse>


[[seminaires:laag:index|Logique, automates, algèbre et jeux]]\\
Jeudi 7 janvier 2016, 10 heures 30, 4033\\
**Sylvain Schmitz** (LSV) //Ideals in VAS Reachability//
<button type="link" size="xs" collapse="b23-3780">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b23-3780" collapsed="true">
<well size="sm">
The decidability of the reachability problem for vector addition systems is a notoriously difficult result. First shown by Mayr in 1981 after a decade of unsuccessful attempts and partial results, its proof has been simplified and refined several times, by Kosaraju, Reutenauer, and Lambert, and re-proven by very different techniques by Leroux in 2012. The principles behind the original proof remained however obscure.

In this seminar, I will present the ideas behind the algorithms of Mayr, Kosaraju, and Lambert (the KLM algorithm) in the light of ideals of well-quasi-orders. The interest here is that ideals provide a semantics to the structures manipulated in the KLM algorithm, bringing some new understanding to its proof of correctness.

Joint work with Jérôme Leroux (LaBRI) presented at LICS’15; see http://arxiv.org/abs/1503.00745
</well>
</collapse>