Room 327

Bundled Fragments of First Order Modal Logic: (Un)decidability

Anantha Padmanabha

IMSc

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.