BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:033936b3-2365-47a1-b87b-e67aa98970cb
X-WR-CALNAME:[LX] Vincent Michielini
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20261025T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
RDATE:20251026T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20250330T020000
RDATE:20260329T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:033936b3-2365-47a1-b87b-e67aa98970cb
DTSTAMP:20260419T173403Z
CLASS:PUBLIC
DESCRIPTION:Maslov’s class K-bar is a fragment of First-Order Logic consist
 ing of formulae in NNF whose variables occurring in the different atoms ob
 ey a certain pattern. It embeds many well-known fragments\, such as the tw
 o-variable fragment\, the Gödel fragment (∀∀∃*)\, some extensions of modal
  logic...\nThe satisfiability problem for K-bar (does a given formula admi
 t a model?) was shown to be decidable by Maslov in the 60's. Yet its exact
  complexity has not been established so far\, although we know that it is 
 NExpTime-hard (as it captures FO2). In the talk\, we complete the picture 
 by showing the following result: every satisfiable formula in K-bar of siz
 e n admits a finite model of size at most 2^{O(n log n)}\, and therefore t
 he problem is NExpTime-complete. Our approach involves a use of satisfiabi
 lity games tailored to K-bar and a novel application of paradoxical tourna
 ment graphs.\n\nThis is a joint work with Oskar Fiuk and Dr Hab Emanuel Ki
 eroński\, both from Wrocław.
DTSTART;TZID=Europe/Paris:20241003T130000
DTEND;TZID=Europe/Paris:20241003T140000
LOCATION:LaBRI
SEQUENCE:0
SUMMARY:[LX] Vincent Michielini
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
