AIML 2024: ADVANCES IN MODAL LOGIC 2024
PROGRAM FOR MONDAY, AUGUST 19TH
Days:
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 2: Invited talk (AiML)
Location: 200
09:00
Group Epistemics, (Co-)algebraically

ABSTRACT. In the vast majority of contributions to multi-agent epistemic, doxastic, and coalition logic, a group is reduced to its extension, i.e., the set of its members. Membership in groups is common knowledge to all agents, with the counterintuitive consequence that groups change identity when their membership changes, and it precludes uncertainty about who is a member of a given group. This idealisation does not reflect the structure of groups or the structured way in which collective epistemic attitudes emerge in the intended application of logical models. Epistemic logics of intensional groups lift the extensionality assumptions above by seeing groups as given to us intensionally by a common property that can change their extension from world to world. We will outline an abstract algebraic and coalgebraic framework that replaces agent or group labels of epistemic modalities with names, and gives them an algebraic structure relevant to the types of collective epistemic attitudes in question. (The talk is based on ongoing collaborative work with Zoé Christoff, Wesley Fussner, Olivier Roy, and Igor Sedlár).

10:00-10:30Coffee Break
10:30-12:30 Session 3A: Regular talks (AiML)
Location: 200
10:30
Birkhoff style proof systems for hybrid-dynamic quantum logic

ABSTRACT. We explore a simple approach to quantum logic based on hybrid and dynamic modal logic, where the set of states is given by some Hilbert space. In this setting, a notion of quantum clause is proposed in a similar way the notion of Horn clause is advanced in first-order logic, that is, to give logical properties for use in logic programming and formal specification. We propose proof rules for reasoning about quantum clauses and we investigate soundness and compactness properties that correspond to this proof calculus. Then we prove a Birkhoff completeness result for the fragment of hybrid-dynamic quantum logic determined by quantum clauses.

11:00
Deducibility in the full Lambek calculus with weakening is HAck-complete
PRESENTER: Vitor Greati

ABSTRACT. We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level F_ω^ω of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We prove that deducibility is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).

11:30
On the Proof Theory of Apodictic Syllogistic

ABSTRACT. The success of syllogistic has been such that many of the features originally characterizing this logic have changed over decades. The present study aims at offering a faithful, possibly comprehensive, account of Aristotle's deductive logic, by extending the inherently proof-theoretical approach introduced by von Plato in 2009/16. Concretely, the main novelty consists in treating syllogistic as a natural-deduction system of rules and 'perfecting' arguments (for imperfect moods) as derivability proofs in tree form. Nothing is added to the original source but, in this way, assertoric and apodictic syllogistic are transparently reconstructed and Aristotle's perfecting proofs are proved to be always correct. This would also be a first step to make the whole modal fragment fully comprehensible and to rehabilitate syllogistic as a fertile theory in the context of natural language reasoning.

12:00
Natural Deduction, Normalization and Subformula Property for Kreisel-Putnam Logic

ABSTRACT. We introduce a new natural deduction system for Kreisel-Putnam logic. Our system is based on Schroeder-Heister's calculus of higher-level rules, an extension of ordinary natural deduction in which not only formulas, but also rules can act as assumptions that may be discharged in the course of a derivation. We will establish a normalization theorem, i.e., we will show that every deduction in our system can be converted into a deduction without "detours". The method used for this is new and might also be applied to other non-classical logics. As a consequence of this result, we will obtain an unrestricted subformula property and a separation theorem for our system.

10:30-12:30 Session 3B: Regular talks (RAMiCS)
Location: 300
10:30
A matrix-oriented view of bisimulation quotients over dioid-labeled transition systems

ABSTRACT. This work considers a special type of bisimulations between transition systems labeled with elements drawn from a dioid.In contrast to the traditional approach, all edges of the systems under consideration bear unique edge labels.Bisimulations between such systems are defined via 0-1-matrices and share some properties with common bisimulations.A particular focus is on bisimulation equivalences and their induced quotients where we show some observations regarding linear equations, eigenvectors, and eigenvalues.

11:00
Formal properties of stochastic matrices for subjective probabilistic operators in kripke frames

ABSTRACT. Availavle at https://ramics-conf.github.io/2024/08-Guallart.pdf

11:30
Developments in higher-dimensional automata theory
12:30-14:30Lunch Break
14:30-15:30 Session 4: Invited talk (RAMiCS)
Location: 200
14:30
Relation-Algebraic Approach to Qualitative Calculi

ABSTRACT. Qualitative calculi are tools intended to mimic human naive everyday reasoning, mostly about space and time. Well known examples include Allen's Interval Algebra for reasoning about intervals of time,and Region Connection Calculus for reasoning about regions of space.The very concept of a qualitative calculus is somewhat vague, and therehave been several attempts to make it precise. For example, (1) Ligozat and Renz "What is a qualitative calculus? A general framework"(2004); then (2) Jackson, Hirsch, TK "Algebraic foundations forqualitative calculi and networks" (2019); then (3) Inants and Euzenat "So, what exactly is a qualitative calculus?" (2020). Each of these generalises the previous ones in some way. I will present an extension of (2) that encompasses (3) but retains the general algebraic spirit of(2).

15:30-16:30 Session 5A: Regular talks (AiML)
Location: 200
15:30
Unification with Simple Variable Restrictions and Admissibility of Pi2-Rules

ABSTRACT. We develop a method to recognize admissibility of Pi2-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called here "unification with simple variable restriction". It is shown that for logical systems enjoying an appropriate algebraic semantics and a finite approximation of left uniform interpolation, this unification with simple variable restriction can be reduced to standard unification. As a corollary, we obtain the decidability of admissibility of Pi2-rules for many logical systems.

16:00
Coalgebraic Semantics for Intuitionistic Modal Logic

ABSTRACT. We give a new coalgebraic semantics for intuitionistic modal logic with $\Box$. In particular, we provide a colagebraic representation of intuionistic descriptive modal frames and of intuitonistic modal Kripke frames based on image-finite posets. This gives a solution to an implicit problem in the area of coalgebaic logic, albeit for these classes of frames, raised explicitly by Litak (2014) and de Groot and Pattinson (2020). Our key technical tool is a recent generalization of a construction by Ghilardi, in the form of a right adjoint to the inclusion of the category of Esakia spaces in the category of Priestley spaces. As an application of these results, we study bisimulations of intuitionistic modal frames, describe dual spaces of free modal Heyting algebras, and provide a path towards a theory of coalgebraic intuitionistic logics.

15:30-16:30 Session 5B: Regular talks (RAMiCS)
Location: 300
15:30
Variety of pointed Abelian l-groups

ABSTRACT. Available at https://ramics-conf.github.io/2024/03-Jankovec.pdf

16:00
Right-orders on free groups
PRESENTER: Simon Santschi

ABSTRACT. Available at https://ramics-conf.github.io/2024/04-Santschi.pdf

16:30-17:00Coffee Break
17:00-18:00 Session 6A: Regular talks (AiML)
Location: 200
17:00
Point-Set Neighborhood Logic
PRESENTER: Yanjing Wang

ABSTRACT. In this paper, we propose Point-set Neighborhood Logic (PSNL) to reason about neighborhood structures. The bimodal language of PSNL is defined via a mutual induction of point-formulas and set-formulas. We show that this simple language is equally expressive as the language of Instantial Neighborhood Logic (INL). As the main results, we first give two complete proof systems, one in Hilbert-style and one in Gentzen sequent-style, each featuring two intertwined $\mathsf{K}$-like systems. The proof of strong completeness of the Hilbert-style system is based on a direct canonical model construction without relying on a normal form. Based on the sequent calculus, we establish constructively the uniform interpolation property of PSNL, from which that of INL follows.

17:30
Lovász Theorems for Modal Languages

ABSTRACT. A famous result due to Lovasz states that two finite relational structures M and N are isomorphic if, and only if, for all finite relational structures T, the number of homomorphisms from T to M is equal to the number of homomorphisms from T to N. Since first-order logic (FOL) can describe finite structures up to isomorphism, this can be interpreted as a characterization of FOL-equivalence via homomorphism-count indistinguishability with respect to the class of finite structures. We identify classes of labeled transition systems (LTSs) such that homomorphism-count indistinguishability with respect to these classes, where "counting" is done within an appropriate semiring structure, captures equivalence with respect to positive-existential modal logic, graded modal logic, and hybrid logic, as well as the extensions of these logics with either backward or global modalities. Our positive results apply not only to finite structures, but also to certain well-behaved infinite structures. We also show that equivalence with respect to positive modal logic and equivalence with respect to the basic modal language are not captured by homomorphism-count indistinguishability with respect to any class of LTSs, regardless of which semiring is used for counting.

17:00-18:00 Session 6B: Regular talks (RAMiCS)
Location: 300
17:00
On the structure of balanced residuated partially-ordered monoids
PRESENTER: Peter Jipsen

ABSTRACT. A \emph{residuated poset} is a structure $\pair{A,\le,\cdot,\ld,\rd,1}$ where $\pair{A,\le}$ is a poset and $\pair{A,\cdot,1}$ is a monoid such that the residuation law $x\cdot y\le z\iff x\le z/y\iff y\le x\backslash z$ holds. A residuated poset is \emph{balanced} if it satisfies the identity $x\backslash x \approx x/x$. By generalizing the well-known construction of P\l{}onka sums, we show that a specific class of balanced residuated posets can be decomposed into such a sum indexed by the set of positive idempotent elements. Conversely, given a semilattice directed system of residuated posets equipped with two families of maps (instead of one, as in the usual case), we construct a residuated poset based on the disjoint union of their domains. We apply this approach to provide a structural description of some varieties of residuated lattices and relation algebras.

17:30
Frames and spaces for distributive quasi relation algebras and involutive FL-algebras
PRESENTER: Peter Jipsen

ABSTRACT. Analogous to atom structures for relation algebras, we define partially ordered frames and prove they are duals for complete perfect distributive quasi relation algebras and distributive involutive FL-algebras. We then extend this dual representation to all algebras and their corresponding frames with a Priestley topology.

For relation algebras up to size 16 it has been determined which algebras are representable by binary relations. We compute all finite distributive quasi relation algebras up to 8 elements and provide representations for some of them.