ABSTRACT. In this talk, I will discuss algorithmic problems that go beyond the problem of formula satisfiability for first-order modal logics. Examples include the following questions: is an extension of a theory a conservative extension? Does there exist an explicit definition of a relation (for logics without the Beth Definability Property)? Does there exist a formula separating a set of positive and negative examples? We will motivate these questions and formulate open problems and conjectures.

ABSTRACT. Bundled products are often offered as good deals to customers. When we bundle quantifiers and modalities together (as in ∃x◻, ◊∀x etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting fragments of FOML without any restriction on the arity of predicates, the number of variables, or the modal scope. It is well-known that finding decidable fragments of FOML is hard, so we may ask: do bundled fragments that exploit the distinct expressivity of FOML constitute good deals in balancing the expressivity and complexity? There are a few positive earlier results on some particular fragments. In this paper, we try to fully map the terrain of bundled fragments of FOML in (un)decidability, and in the cases without a definite answer yet, we show that they lack the finite model property. Moreover, whether the logics are interpreted over constant domains (across states/worlds) or increasing domains presents another layer of complexity. We also present the \textit{loosely bundled fragment}, which generalizes the bundles and yet retain decidability (over increasing domain models). （Joint work with Anantha Padmanabha, R. Ramanujam, and Yanjing Wang）

ABSTRACT. In the last few years some fragments of FOML have been shown to be decidable—e.g., the one-variable, the monodic, and some guarded fragments are decidable. Most proofs of decidability deal with the satisfiability problem and use model-theoretic techniques. This talk presents some preliminary results on terminating sequent calculi allowing to give a proof-theoretic proof of decidability for the validity problem in some fragments of FOML. This is joint work with Sara Negri (Genova) and Matteo Tesi (SNS, Pisa).

ABSTRACT. The Quantified Reflection Calculus with N modalities, or QRC_N, is a quantified and strictly positive modal logic inspired by the provability reading of the modal symbols. The non-modal language consists of a verum constant and relational symbols as atomic formulas, conjunctions, and universal quantifiers. The available modal connectives are labeled diamonds, one for each natural number n < N. QRC_N statements are assertions of the form A \vdash B, with A and B in this strictly positive language. We describe the axiomatic system for QRC_N and see that it is sound with respect to constant domain Kripke models. Then we focus on the QRC_1 fragment, which is complete with respect to finite and constant domain Kripke models, and thus decidable. The completeness and decidability of the general case with N modalities is still an open problem. (Joint work with Joost J. Joosten)

ABSTRACT. During the talk I will present a novel logic called the forward guarded fragment (FGF) that combines ideas of forward and guarded quantification. The presented logic extends the Description Logic ALC with higher-arity relations in a tamed way: both the knowledge base satisfiability problem and conjunctive query entailment problem are ExpTime-complete, thus having the same complexity as plain ALC. We provide a few intuitions behind these results and discuss an ongoing work towards model-theory and extensions of FGF.

ABSTRACT. The system of modal logic K is included—under the standard translation—in three major fragments of first-order logic for which satisfiability is decidable: the two-variable fragment, the guarded fragment, and the fluted fragment. But while the first two of these have been the focus of considerable attention in recent decades, the fluted fragment has, by contrast—and notwithstanding the promise it holds for equipping modal logic with additional quantification—suffered from relative neglect. In this talk, I shall present some recent results on the fluted fragment, focusing especially on its extension with counting quantifiers and transitive relations.

ABSTRACT. Term Modal logic (TML) is closely related to First Order Modal Logic (FOML). TML allows modal operators to be indexed by terms which is suitable to model settings where the agent set is unbounded. A typical formula in TML is of the form \forall x \exists y~\Box_x P(x,y). Similar to FOML, TML is also highly undecidable. For instance just having propositions as atoms leads to undecidability. We will discuss the close correspondence between TML and FOML and give translations that help us to identify decidable fragments of TML. As a contrast between the two logics, we show that the two variable fragment (without constants, equality) of TML is decidable, whereas the two variable fragment of FOML is known to be undecidable. (Joint work with R. Ramanujam)