View: session overviewtalk overview
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 PRESENTER: Melissa Antonelli 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 | 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 ABSTRACT. Available at https://ramics-conf.github.io/2024/02-Fahrenberg.pdf |
15:30 | Unification with Simple Variable Restrictions and Admissibility of Pi2-Rules PRESENTER: Rodrigo Nicolau Almeida 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 PRESENTER: Rodrigo Nicolau Almeida 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 | 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 |
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 | 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. |