Affiliated workshop of LICS at FLOC 2022

Location: Haifa (or hybrid)

Date:  July 31 2022

Organizers:

• R. Ramanujam (IMSc, India): jam@imsc.res.in
• Yanjing Wang (Peking University, China): y.wang@pku.edu.cn

Background

Propositional Modal Logic has found major applications in computer science in the formal specification and verification of finite-state systems in general, and multi-agent systems in AI. In the last two decades, researchers have been attempting to extend verification techniques to infinite-state systems that arise in distributed computing, database theory, and security theory. Reasoning about such systems typically involves both modalities (to express state transitions and1 reachability) and quantifiers (to refer to unbounded data, dynamically created processes, etc). This naturally leads us to the realm of first-order modal logic (FOML).

Indeed, early formulations of programming logics in the 1980s like Dynamic logic, Hoare logic, etc were first-order modal logics. However, unlike propositional modal logics which are robustly decidable(in the sense that natural ex-tensions of many kinds are decidable), FOML is notoriously undecidable. That is, it is very hard to find non-trivial decidable fragments of FOML. The thorough knowledge that we have obtained in the past decades about decidable fragments of first-order logic and decidable extensions of modal logic seems to help very little. For example, the two-variable fragment of FOML is already undecidable. The combination of modalities and quantifiers causes new problems that occur neither in the first-order case nor in the propositional modal case.

Despite such discouragement, this century has seen some small steps with positive results on new fragments, such as the monodic fragments which restrict the appearance of variables in the scope of modalities [Hodkinson, Wolter, Zakharyaschev 2000]. Another recent idea is to bundle the quantifiers and modalities together in certain forms, inspired by applications in non-standard epistemic logic [Wang 2017] [Padmanabha, Ramanujam and Wang 2018]. Developments in Term-modal logics, a close cousin of FOML suggest that more fragments may be hiding beneath the surface: for instance, the two-variable fragment of Term-modal logic is decidable and constitutes an as-yet uncharacterized fragment of FOML.

This workshop aims to bring the leading researchers on this evolving direction of research and identify both potentially useful fragments of FOML and techniques for constructing decision procedures.

Format

We will have three invited talks that present surveys of what has been achieved, highlighting the difficulties arising from combining quantification and modalities. There will be up to 5 contributed talks, and an open problem session at the end of the day.

Invited Speakers

Eugenio Orlandelli (University of Bologna)

Ian Pratt-Hartmann (University of Manchester)

Frank Wolter (University of Liverpool)

Tentative Programme (Updated)

8:30 – 9:00 (IDT time) Coffee and Opening remarks

9:00 – 10:00   Frank Wolter: Decidability Questions beyond Satisfiability for First-order Modal Logics

10:00-10:30  Mo Liu: Are Bundles Good Deals for FOML?

10:30 ~ 11:00 Coffee break

11:00-12:00 Eugenio Orlandelli: Terminating sequent calculi for decidable fragments of FOML

12:00-12:30 Ana Borges: The Quantified Reflection Calculus as a Modal Logic

12:30-14:00 Lunch break 

14:00-14:30 Bartosz Bednarczyk: Forward Guarded Fragment: A tamed higher-arity extension of ALC 

14:30-15:30 Ian Pratt-Hartman: From Modal Logic to Fluted logic

15:30-16:00 Coffee break

16:30-16:30  Anantha Padmanabha: Decidable Fragments of Term Modal Logic

 16:30 ~ 17:00  Open Problem Session

Abstracts

Decidability Questions beyond Satisfiability for First-order Modal Logics

Frank Wolter (University of Liverpool)

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.

From Modal Logic to Fluted logic

Ian Pratt-Hartmann (University of Manchester)

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, focussing especially on its extension with counting quantifiers and transitive relations.

Are Bundles Good Deals for FOML?

Mo Liu (Loria), Anantha Padmanabha (ENS), R. Ramanujam (IMSc), Yanjing Wang (Peking University)

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).

The Quantified Reflection Calculus as a Modal Logic

Ana de Almeida Borges & Joost J. Joosten (Universitat de Barcelona)

The Quantified Reflection Calculus with N modalities, or , 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 . statements are assertions of the form , with and in this strictly positive language. We describe the axiomatic system for and see that it is sound with respect to constant domain Kripke models. Then we focus on the 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.

Forward Guarded Fragment: A tamed higher-arity extension of ALC

Bartosz Jan Bednarczyk (TU Dresden and at University of Wrocław)

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.

Decidable Fragments of Term Modal Logic

Anantha Padmanabha (ENS) and R. Ramanujam (IMSc)

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 . 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.

Terminating sequent calculi for decidable fragments of FOML

Eugenio Orlandelli (University of Bologna)

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).