Monday, December 3 2018
11:30 - 12:30

First order modal logics are notoriously undecidable (in the sense that even very innocuous-seeming fragments are undecidable). We propose a fragment where modalities and quantifiers are "bundled" together, so that we have formulas like ``for some x, every successor satisfies P(x)'' but not formulas like ``for all x, y.if P(x) then every successor satisfies Q(x,y)''. This fragment is decidable over increasing domains, whereas its \$\forall x. \Box\$ sub-fragment is already undecidable over constant domains.The work is joint with R Ramanujam (IMSc) and Yanjing Wang (Peking University), and will be presented at FST&TCS 2018.

Download as iCalendar

Done