# LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue).
If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

## Past Seminars

### Locality of counting logics

- Date
- Tuesday, October 03 2017 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Dietrich Kuske (TU Ilmenau)

We introduce the logic FOCN(ℙ) which extends first-order logic by counting
and by numerical predicates from a set ℙ, and which can be viewed as a
natural generalisation of various counting logics that have been studied in the
literature.

We obtain a locality result showing that every FOCN(ℙ)-formula can be
transformed into a formula in Hanf normal form that is equivalent on all finite
structures of degree at most *d*.
A formula is in Hanf normal form if it is a Boolean
combination of formulas describing the neighbourhood around its tuple of free
variables and arithmetic sentences with predicates from ℙ over atomic statements
describing the number of realisations of a type with a single centre. The
transformation into Hanf normal form can be achieved in time elementary in
*d* and the size of the input formula.
From this locality result, we infer the following applications:

- The Hanf-locality rank of first-order formulas of bounded quantifier
alternation depth only grows polynomially with the formula size.
- The model checking problem for the fragment FOC(ℙ) of
FOCN(ℙ)
on structures of bounded degree is fixed-parameter tractable (with
elementary parameter dependence).
- The query evaluation problem for fixed queries from FOC(ℙ) over fully
dynamic databases of degree at most
*d* can be solved efficiently: there is a
dynamic algorithm that can enumerate the tuples in the query result with
constant delay, and that allows to compute the size of the query result
and to test if a given tuple belongs to the query result within constant
time after every database update.

References

- [1] Dietrich Kuske and Nicole Schweikardt. First-order logic with counting. In
*32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*, pages 1–12. IEEE Computer Society, 2017.