AIML 2024: ADVANCES IN MODAL LOGIC 2024
PROGRAM FOR TUESDAY, AUGUST 20TH
Days:
previous day
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 7: Invited talk (AiML)
Location: 200
09:00
Efficient Theorem-Proving for Modal Logics

ABSTRACT. Modal logics have been extensively studied, as they are able to express non-trivial problems ranging from domains in Mathematics and Philosophy to representation of computational systems. The implementation of reasoning engines for those logics is, therefore, highly desirable. However, the satisfiability problem for even the most basic of the multimodal logics, the modal logic Kn, is not tractable: local and global reasoning in the multiagent set are PSPACE-complete and EXPTime-complete, respectively. We are, thus, interested in calculi that can be effectively employed for reasoning within those logics in an efficient way.In this talk we will discuss two different resolution-based calculi for the multimodal Kn with particular focus on the characteristics that have impact on theorem-proving. We will report on experimental results and the influence of proof strategies and processing techniques for both calculi. Finally we will discuss how both calculi can be extended to deal with other interesting modal logics, and how different techniques for achieving those extensions impact the efficiency of theorem-proving in practice.

10:00-10:30Coffee Break
10:30-12:30 Session 8: Regular talks (AiML)
Location: 200
10:30
Towards Dynamic Distributed Knowledge

ABSTRACT. We propose a novel notion of distributed knowledge called dynamic distributed knowledge that corresponds to what a group of agents know after they share their knowledge. Its interpretation in Kripke models therefore combines static (modal accessibility) with dynamic (update) aspects. In prior work the static and dynamic aspects were also investigated, but separately, where the latter was called resolution. Unlike the usual distributed knowledge, in this work called static distributed knowledge, if a group of agents have dynamic distributed knowledge of a proposition, then they have dynamic distributed knowledge that the proposition is common knowledge. We report on its expressivity, axiomatization, and bisimulation characterization.

11:00
Varieties of Distributed Knowledge

ABSTRACT. Distributed knowledge is one of the better known group knowledge modalities. While its intuitive idea is relatively clear, there is ample room for interpretation of details.

We investigate 12 definitions of distributed knowledge that differ from each other in the kinds of information sharing the agents can perform in order to achieve shared knowledge of a proposition.

We then show which kinds of distributed knowledge are equivalent, and which kinds imply each other, i.e., for any two variants t1 and t2 of distributed knowledge we show whether a proposition phi being distributed knowledge under definition t1 implies that phi is distributed knowledge under definition t2.

11:30
Bisimulation for Impure Simplicial Complexes

ABSTRACT. As an alternative to Kripke models, simplicial complexes are a versatile semantic primitive on which to interpret epistemic logic. Given a set of vertices, a simplicial complex is a downward closed set of subsets, called simplexes, of the vertex set. A maximal simplex is called a facet. Impure simplicial complexes represent that some agents (processes) are dead. It is known that impure simplicial complexes categorically correspond to so-called partial epistemic (Kripke) models. In this contribution we define a notion of bisimulation to compare impure simplicial complexes and show that it has the Hennessy–Milner property. These results are for a logical language including atoms that express whether agents are alive or dead. Without these atoms it is unclear to us whether such a notion of bisimulation exists, that we amply justify by counterexamples. The restricted language may well be insufficiently expressive.

12:00
Logics for Data Exchange and Communication

ABSTRACT. We present a new family of dynamic logics that can model complex scenarios of data exchange and communication. In the context of multi-agent systems, these are acts by which individual agents or groups of agents can publicly or privately access all the information stored at specific locations. In addition to having the full power of standard dynamic epistemic logics (DEL) to model acts of propositional communication, our logics can handle the type of information exchanges in which the data that is being communicated is not explicitly captured by a proposition. The examples in the full paper show how our logics expand the application domain of DEL in distributed computing. To axiomatize these logics, in the presence of common and distributed knowledge modalities, we first have to enrich them with polyadic modalities that express various complex levels of conditional group knowledge. While expressible in the extension of PDL with intersection (which is decidable but does not have FMP), these logics are better behaved: we use an innovative method to show that they do have FMP. We axiomatize these static logics using PDL-type systems, then axiomatize the corresponding dynamic data-exchange logics and prove their decidability, by reducing them to their static base via Recursion/Reduction Axioms.

11:00-12:30 Session 9: Regular talks (RAMiCS)
Location: 300
11:00
Fuzzy and crisp binary relation reduction: applications for data summarization and anomalies detections

ABSTRACT. Available at https://ramics-conf.github.io/2024/09-Jaoua.pdf

11:30
Monotone Ω-sup-fuzzy relations: converse and complementation

ABSTRACT. $L$-fuzzy relations on a set $X$ are functions from $X \times X$ to the lattice $L$ and act on the $L$-fuzzy subsets of $X$. When $L$ is the lattice of sup-preserving endomaps on a complete lattice $\Omega$, the relations act also on the $\Omega$-fuzzy subsets of $X$. We call these relations equipped with this action, $\Omega$-sup-fuzzy relations. When X is a preorder, monotone relations of this form act on the lattice of monotone functions from X to $\Omega$.The motivation comes from mathematical morphology in image processing. Grey-scale images are modelled as functions on sets of pixels with $\Omega$ as the set of grey levels. More generally, graphs and hypergraphs labelled by grey levels can be handled. Enriching the lattice of $\Omega$-sup-fuzzy relations with a multiplication operation provides a unital quantale that acts on the lattice of grey-scale images via the morphological operations of dilation and erosion. We study the quantale of Ω-sup-fuzzy relations, with particular attention to the concepts of converse and complementation for these relations.

12:00
Lifting star-autonomy

ABSTRACT. For a functor $\Q$ from a category $\C$ to the category $\Pos$ of ordered sets and order-preserving functions, we study liftings---from the base $\C$ to the total category $\iQ$---of \SM, \SMC, \saut structures. Our systematic study relies on a bijection between liftings of functors to the total categories and some kind of lax-natural transformations, and yields exact conditions for these liftings. When $\Q$ factors as a monoidal functor through $\SLatt$, the category of complete lattices and \sp functions, we obtain, as a corollary of these conditions, that $\iQ$ is closed. For such a $\Q$, we also describe a method, analogous to the double negation nucleus from quantale theory, making it possible to quotient $\Q$ into a functor $\Qnn$ such that $\int \Qnn$ is \saut. We prove then a representation theorem for those $\Q$ monoidal to $\SLatt$ for which $\iQ$ is \saut. The theory developed, originally motivated from the categories $\QSet[P]$ of \SdP, yields a generalization of \HS construction of \saut categories by means of orthogonality structures.

12:30-14:30Lunch Break
14:30-15:30 Session 10A: Regular talks (AiML)
Location: 200
14:30
Logics of Knowability

ABSTRACT. Knowability has a significant history in the field of epistemic logic dating back to the introduction of Fitch's paradox in 1963. More recently it has received attention from the perspectives of dynamic epistemic logic and epistemic temporal logic. However, existing treatments of knowability either address a knowability-like concept that deviates from an intuitive understanding of knowability in some important way or take knowability to be a complex notion merely definable in the language. In this paper, we take `it is knowable that' as a primitive modality and offer axiomatizations of two knowability logics—one of knowledge and knowability and one of pure knowability. We prove that these logics are sound and complete with respect to a distinguished subclass of birelational frames. These proofs are of technical interest, as well; because knowability is, we argue, best understood as a non-normal modality, the completeness proofs require novel constructions.

15:00
A modal logic for reasoning in contexts

ABSTRACT. We provide a semantics for a language containing indicatives and epistemic modals, which are elusive in formal semantics. The main idea is to evaluate a formula at a world in a context. An indicative is true at a world in a context if its consequent is true at the world in the new context updated by its antecedent in the old context. A epistemic necessity is true at a world in a context if it is true at all worlds in the context. Armed with the semantics, we define a ternary notion of validity, by which an inference is not valid per se, but valid under a set of assumptions, which are used to specify the context. The ternary notion of validity are meant to give a unified solution to several puzzles concerning indicatives and epistemic modals.

14:30-15:30 Session 10B: Regular talks (RAMiCS)
Location: 300
14:30
Varieties of BL-algebras with the amalgamation property: an exhaustive classification
PRESENTER: Wesley Fussner

ABSTRACT. Available at https://ramics-conf.github.io/2024/01-RAMiCS2024_Fussner_Santschi.pdf

15:00
Tabular and pretabular varieties of MTL-algebras
PRESENTER: Matteo Bianchi

ABSTRACT. Tabular logics have been studied since the sixties, while the notion of pretabular (PT) variety was firstly introduced in the seventies by A.V. Kuznetsov and L. Maksimova, for Heyting algebras. A variety is tabular whenever it is generated by one finite algebra. A variety $\mathbb{L}$ is PT whenever $\mathbb{L}$ is not tabular but every variety $\mathbb{M}\subsetneq\mathbb{L}$ is tabular. In this paper we study the same notion for the case of MTL-algebras. We show that a variety of MTL-algebras is PT if and only if it is generated by each of its infinite chains, and we study some general properties of PT varieties of MTL-algebras.  Also, we provide a full classification of tabular and PT varieties of BL and WNM-algebras.

15:30-16:30 Session 11A: Short talks (AiML)
Location: 200
15:30
Epistemic Positions: Towards a Formal Theory of Epistemic Injustice
PRESENTER: Huimin Dong

ABSTRACT. Cases of bias and unfair decisions in automated decision-making are heavily discussed. When unfair decision outcomes can be attributed to an unjust difference in the knowledge of various groups of subjects, we can speak of epistemic injustice (Fricker). In this paper, we analyse various kinds of epistemic injustice, such as testimonial, hermeneutical, distributional, and content-focused epistemic injustice, and show how they can be conceptualised. We then provide a formalisation of the difference in group knowledge, in a version of epistemic logic. After that, we analyse the key properties of epistemic injustice in a case study of information systems for government decision-making.

15:45
Simplicial Belief

ABSTRACT. Recently, much work has been carried out to study simplicial interpretations of modal logic. While notions of (distributed) knowledge have been well investigated in this context, it has been open how to model belief in simplicial models. We introduce polychromatic simplicial complexes, which naturally impose a plausibility relation on states. From this, we can define various notions of belief.

16:00
Substitution as Modality
PRESENTER: Yanjing Wang

ABSTRACT. In the expositions of axiomatizations of first-order logic, the (admissible) substitution played an important role. However, it is usually defined only in the meta-language. In this paper, inspired by dynamic epistemic logic and modal logic with the assignment operators, we take syntactic substitutions as (dynamic) modalities in the logical language. Adding this operator to the first-order language complicates the logic, but we can avoid the meta-language notion of substitution in the axiomatizations. As the main result, we axiomatize first-order logic with equality enriched with such substitution modalities.

16:15
An Aretaic Approach to Deontic Logic

ABSTRACT. We present a new approach to the semantics of deontic logic, based on Aristotelian virtue ethics and Hursthouse's Criterion of Right Action. This allows us to define notions of strong, weak, and composite obligation, as well as permission and prohibition operators that are basic and not interdefinable with obligation. Through this, we introduce a distinction between two types of agent-virtue interactions: instantaneous and cultivative. This provides us with a richly expressive, robust semantics for expressing deontic distinctions in logic, and a formal bridge between two realms of moral discourse previously considered to be incompatible.

16:30-17:00Coffee Break
17:00-19:00 Session 12: Regular talks (AiML)
Location: 200
17:00
Positive modal logic over finite MV-chains

ABSTRACT. In this paper, we introduce and study the positive (i.e., the negation-free and implication-free) fragment of many-valued modal logic based on a finite MV-chain as algebra of truth-degrees. Besides the usual Kripke semantics, we introduce richer relational semantics based on partially ordered sets with local constraints on admissible valuations. We study this logic algebraically via the varieties of modal n-valued positive MV-algebras. Utilizing prior work on natural dualities for n-valued positive MV-algebras and the close relationship between these algebras and their distributive skeletons, we prove an algebraic completeness theorem. Furthermore, by means of an example regarding canonicity, we illustrate how the richer relational semantics presented in this paper are `better-behaved' with respect to the positive many-valued modal logic than Kripke (or other intermediate) semantics are.

17:30
Towards an Algebraic Theory of KD45-like Logics
PRESENTER: George Metcalfe

ABSTRACT. Algebraic semantics are introduced for a family of ‘KD45-like’ modal substructural logics as a generalization of Bezhanishivili’s pseudomonadic algebras for the modal logic KD45. It is shown that these structures correspond to ordered pairs consisting of an FLe-algebra (or commutative pointed residuated lattice) and a subalgebra with a suitable lattice filter, extending a similar result for ‘S5-like’ logics. It is then shown that if the FLe-algebra reduct belongs to a variety that has the superamalgamation property, then the structure equipped with an additional constant is representable as an algebra of functions from a set of worlds to an FLe-algebra of the same variety.

18:00
Modal logic, fundamentally

ABSTRACT. Non-classical generalizations of classical modal logic have been developed in the contexts of constructive mathematics and natural language semantics. In this paper, we discuss a general approach to the semantics of non-classical modal logics via algebraic representation theorems. We begin with complete lattices $L$ equipped with an antitone operation $\neg$ sending $1$ to $0$, a completely multiplicative operation $\Box$, and a completely additive operation $\Diamond$. Such lattice expansions can be represented by means of a set $X$ together with binary relations $\vartriangleleft$, $R$, and $Q$, satisfying some first-order conditions, used to represent $(L,\neg)$, $\Box$, and $\Diamond$, respectively. Indeed, any lattice $L$ equipped with such a $\neg$, a multiplicative $\Box$, and an additive $\Diamond$ embeds into the lattice of propositions of a frame $(X,\vartriangleleft,R,Q)$. Building on our recent study of \textit{fundamental logic}, we focus on the case where $\neg$ is dually self-adjoint ($a\leq \neg b$ implies $b\leq\neg a$) and $\Diamond \neg a\leq\neg\Box a$. In this case, the representations can be constrained so that $R=Q$, i.e., we need only add a single relation to $(X,\vartriangleleft)$ to represent both $\Box$ and $\Diamond$. Using these results, we prove that a system of fundamental modal logic is sound and complete with respect to an elementary class of bi-relational structures $(X,\vartriangleleft, R)$.

18:30
Goldblatt-Thomason Theorems for Fundamental (Modal) Logic

ABSTRACT. Holliday recently introduced a non-classical logic called Fundamental Logic, which intends to capture exactly those properties of the connectives "and", "or" and "not" that hold in virtue of their introduction and elimination rules in Fitch's natural deduction system for propositional logic. Holliday provides an intuitive relational semantics for fundamental logic which generalizes both Goldblatt's semantics for orthologic and Kripke semantics for intuitionistic logic. In this paper, we further the analysis of this semantics by providing a Goldblatt-Thomason theorem for Fundamental Logic. We identify necessary and sufficient conditions on a class K of fundamental frames for it to be axiomatic, i.e., to be the class of frames satisfying some logic extending Fundamental Logic. As a straightforward application of our main result, we also obtain a Goldblatt-Thomason theorem for Fundamental Modal Logic, which extends Fundamental Logic with standard Box and Diamond operators.