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 Laurent Doyen and Stefan Göller.

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

Visit website for this news | Export event in iCalendar format

- 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.

- [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.

- Private Pages
- RSS
- Page maintained by Laurent Doyen and Stefan Göller.
- English
- Français