BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
Locality of counting logics
STATUS:CONFIRMED
ATTENDEE;CN="Dietrich Kuske
":
MAILTO:no@spam.com
DESCRIPTION:
We introduce the logic FOCN(ℙ) which extends first-order log
ic by counting and by numerical predicates from a set ℙ\, an
d which can be viewed as a natural generalisation of various
counting logics that have been studied in the literature. W
e obtain a locality result showing that every FOCN(ℙ)-formul
a 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 combina
tion of formulas describing the neighbourhood around its tup
le of free variables and arithmetic sentences with predicate
s from ℙ over atomic statements describing the number of rea
lisations 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 res
ult\, we infer the following applications: The Hanf-locality
rank of first-order formulas of bounded quantifier alternat
ion depth only grows polynomially with the formula size. The
model checking problem for the fragment FOC(ℙ) of FOCN(ℙ) o
n structures of bounded degree is fixed-parameter tractable
(with elementary parameter dependence). The query evaluation
problem for fixed queries from FOC(ℙ) over fully dynamic da
tabases 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 compu
te the size of the query result and to test if a given tuple
belongs to the query result within constant time after ever
y 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. I
EEE Computer Society\, 2017.
DTSTART;TZID=Europe/Paris:20171003T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201710031
100
UID:LSVsemLSV.201710031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR