Česká společnost pro kybernetiku a informatiku

Pozvánka na seminář

Pozvánka na přednášku Chun Yu Lin : On some non-classical cylindric algebras

@Seminář aplikované matematické logiky10.12.2025 16:00

Cylindric algebras, introduced by A. Tarski, J. D. Monk, and L. Henkin, provide an algebraic framework for classical first-order logic. The investigations of structures of cylindric algebras by R. Maddux, H. Andréka, I. Németi, I. Sain, R. Hirsch, and I. Hodkinson have led to deep results on representability, finite axiomatizability, game-theoretic constructions, and more. The close connection between logic and cylindric algebras naturally raises the question of how to algebraize non-classical first-order logics. In this talk, we study cylindric ortholattices and weakening cylindric algebras, with particular emphasis on their construction and representability. We also investigate their connections with polyadic ortholattices and weakening polyadic algebras. This talk is based on joint work with Joseph MacDonald and Peter Jipsen.

Pozvánka na přednášku Han Gao : A Natural Intuitionistic Modal Logic: calculi, decidability and countermodels

@Seminář aplikované matematické logiky26.11.2025 16:00

The field of intuitionistic modal logic (IML), originating in the 1940s, has evolved into two primary traditions: one (often called "intuitionistic modal logic") focused on meta-logical properties, and another (often called "constructive modal logic") driven by applications in computer science. In this talk we will first briefly survey this developmental landscape and then introduce and investigate a new variant in the IML family called FIK, that is a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We present a sound and complete Hilbert-style axiom system for FIK, then propose a proof-theoretic framework called bi-nested sequent calculus that provides both a decision procedure and a direct counter-model extraction from any failed derivation. With this calculus, we obtain decidability and finite model property of FIK. Furthermore, we demonstrate how to restrict the nesting level of the bi-nested calculus to obtain a "shallow" (1-level nested, single type of nesting), label-free sequent calculus for the logic. The shallow calculus enjoys the cut-elimination property and provides a good complexity bound for the logic's decision problem. Time permitting, we will also discuss how the bi-nested calculus serves as a unified and modular proof-theoretic framework for many other variants of IML. This talk is mainly based on joint work with Philippe Balbiani, Çiğdem Gencer and Nicola Olivetti.

Pozvánka na přednášku Isabel Hortelano : The connection between amalgamation and deductive interpolation

@Seminář aplikované matematické logiky12.11.2025 16:00

The relationships between various forms of interpolation for propositional logics and amalgamation for classes of algebraic structures have received considerable attention in the literature in the frameworks of model theory, abstract algebraic logic, universal algebra, and residuated structures. A well-known theorem states that a variety with the congruence extension property (CEP) has the amalgamation property (AP) if and only if it has the deductive interpolation property (DIP). This “bridge theorem” provides a powerful technique for establishing the deductive interpolation property via the amalgamation property, and vice versa. However, for varieties that lack the congruence extension property, failure of the amalgamation property does not necessarily imply failure of the deductive interpolation property. For example, the varieties of ℓ-groups and residuated lattices do not have the AP, but since they also lack the CEP, the status of the DIP is open for these cases.
To provide a route to developing a more systematic understanding of deductive interpolation, we will review the different solutions found in the literature to the problem of describing an algebraic property that corresponds directly to the DIP. We will also introduce a property weaker than the congruence extension property that, when combined with the deductive interpolation property, is equivalent to the amalgamation property. Finally, we will present an effective algorithm for deciding whether a congruence-distributive variety, generated by a given finite set of finite algebras, has the DIP.
This is joint work with Wesley Fussner, George Metcalfe and Simon Santschi.

Pozvánka na přednášku Krysztof Krawczyk : Maehara interpolation in extensions of R-mingle

@Seminář aplikované matematické logiky05.11.2025 16:00

This is a joint work with Wesley Fussner. We show that there are exactly five quasivarieties of Sugihara algebras with the amalgamation property, and that all of these have the relative congruence extension property. As a consequence, we obtain that the amalgamation property and transferable injections property coincide for arbitrary quasivarieties of Sugihara algebras. These results provide a complete description of arbitrary (not necessarily axiomatic) extensions of the logic R-mingle that have the Maehara interpolation property, and further demonstrates that the Robinson property and Maehara interpolation property coincide for arbitrary extensions of R-mingle.

Pozvánka na přednášku Roman Kossak : The Tennenbaum phenomenon in a general setting

@Seminář aplikované matematické logiky22.10.2025 16:00

In 1959, Stanley Tennenbaum proved that there are no computable nonstandard models of Peano Arithmetic. In 1964, John Shepherdson showed that there are computable nonstandard models of Peano axioms with the induction schema restricted to quantifier-free formulas. In the 1980s and 90s, much work in the model theory of arithmetic was devoted to the problem of determining the limits Tennenbaum's theorem. In my talk, I will discuss some of these developments and present a general model-theoretic framework for studying the Tennenbaum phenomenon based on applications of the notions recursive saturation and resplendence.

Pozvánka na přednášku Fabio De Martin Polo : Reflecting on the proof theory of first-order relevant logics and relevant modal logics

@Seminář aplikované matematické logiky15.10.2025 16:00

In contemporary developments of first-order relevant logics and (propositional) relevant modal logics, several limitations and challenges have emerged, both from a semantic standpoint (particularly concerning relational models) and from a proof-theoretic one (especially in sequent calculi). The aim of this talk is threefold.
(i) To outline the current state of the debate on first-order relevant logics and relevant modal logics, highlighting, on the one hand, significant proof-theoretic limitations and, on the other, recent semantic advances, particularly the Goldblatt-Mares–Ferenz–Tedder line of work.
(ii) To propose possible approaches to the proof theory of first-order relevant logics, employing labeled sequent calculi to construct systems with admissible Cut that enable a modular treatment of the class of relevant logics under consideration (joint work with N. Ferenz); and to suggest how a similar strategy might be extended to relevant modal logics, which, at the relational level, introduce an additional layer of complexity, being characterized not only by the usual ternary relation for implication but also by one or more binary relations for the modal operators.
(iii) To discuss the (dis)advantages of adopting “external” rather than “internal” calculi, and to explore how, in future developments of this work, one might move — via some suitable translation procedures — toward calculi devoid of “explicit” semantic components within their syntax. This concluding discussion will not be confined to the proof theory of relevant logics but will adopt a broader perspective, informed by both earlier and recent developments in the proof theory of non-classical logics.

Pozvánka na přednášku Krishna Manoorkar : Defeasible reasoning on concepts

@Seminář aplikované matematické logiky01.10.2025 16:00

Formal Concept Analysis (FCA) is a mathematical framework widely used in Knowledge Representation and Reasoning to study conceptual hierarchies. In FCA, concepts are represented as pairs of objects and features, corresponding to the extension and intension of concepts, and together they form a complete lattice. By Birkhoff's representation theorem, every complete lattice can be represented in this way. Consequently, the logic of formal concepts can be understood as the logic of lattices. This logic, along with its modal extensions and their connection to FCA, has been actively studied in recent years. However, to capture realistic forms of reasoning, it is essential to formalize defeasible reasoning on concepts.
In this talk, I present a generalization of KLM-style defeasible reasoning to the conceptual framework. Specifically, the framework introduces different notions of defeasible inclusion—forms of inclusion that typically hold by default but may be overridden by exceptions in the extension, intension, or both—by generalizing the cumulative reasoning system and the cumulative reasoning system with a loop to the conceptual setting. Furthermore, we extend cumulative models, cumulative ordered models, and preferential models to the conceptual domain and establish soundness and completeness results for these generalized models.

Pozvánka na přednášku Matteo De Berardinis : A Proof Theory for Profinite Modal Algebras

@Seminář aplikované matematické logiky11.06.2025 16:00

Profinite modal algebras are monadic over Set. This monadicity result suggests that profinite modal algebras could be presented as Lindembaum algebras for propositional theories in infinitary versions of propositional modal calculi. In fact, it is possible to identify such calculi as modal extensions of Maheara-Takeuti’s infinitary extension of the sequent calculus LK. Correspondences between syntactic properties of the calculi and regularity/exactness properties of the opposite category of profinite modal algebras can be established.

Pozvánka na přednášku Wolfgang Poiger : Coalgebraic dynamic logic (re-)visited

@Seminář aplikované matematické logiky28.05.2025 16:00

Propositional Dynamic Logic (PDL) is a well-known modal logic for reasoning about non-deterministic programs and Game Logic (GL) can be seen as a generalisation from programs to 2-player games. Such logics combine modal reasoning with an algebra of operations on their semantic structures, a perspective which was abstracted into the framework of coalgebraic dynamic logic in [1,2]. State-based structures are modelled as F-coalgebras for some Set-endofunctor F, while modalities are interpreted by natural transformations called predicate liftings. The work [1,2] heavily relies on the assumptions that F is a monad and that operations/tests/modalities are defined in accordance with this monad.
However, various (recent) examples of dynamic logics such as Instantial PDL [3] and many-valued variants of PDL [4] do not meet these requirements.
In this talk, we present a broader framework for coalgebraic dynamic logics lifting all the above-mentioned restrictions and, among others, present extensions of the main results of [1] therein. Here, the signature functor F is not required to be a monad, our coalgebraic logic may have countably many types of modalities and furthermore may be fuzzy/many-valued (taking values in an arbitrary FLew-algebra). In particular, this allows us to encompasses the dynamic logics considered in [3,4] into the coalgebraic framework.
First, we describe the general notions of coalgebra operations and tests and identify conditions ensuring them to be safe, i.e., preserving bisimulation/behavioural equivalence. We introduce reducible coalgebra operations and tests, entailing the soundness of certain reduction axioms, and show that reducibility always implies safety. For finitely-valued logics, we proceed to show that if all operations and tests are reducible then one-step completeness of the underlying coalgebraic modal logic implies strong completeness of its dynamic version. This generalises the main results of [1], and with concrete instantiations we obtain, e.g., strong completeness for a many-valued variant of iteration-free game logic and for two-valued iteration-free PDL with weighted accessibility relations.
This talk is based on joint work with Helle Hansen.

Pozvánka na přednášku Adam Přenosil : Which po-monoids arise from po-groups?

@Seminář aplikované matematické logiky21.05.2025 16:00

Mundici's representation of MV-algebras as intervals in Abelian lattice-ordered groups was a landmark result in a number of ways. Besides its key role in the theory of MV-algebras, it sparked the search for further representations of ordered algebras arising in non-classical logic by means of partially ordered groups (po-groups), with the aim of leveraging the extensively studied theory of po-groups to understand these wider (and wilder) classes of algebras. Two notable results in this direction are the representation due to Galatos & Tsinakis of GMV-algebras as so-called nuclear images of certain submonoids of lattice-ordered groups, and the representation due to Dvurečenskij & Vetterlein of so-called pseudo-effect algebras as intervals in po-groups. In this talk, we show that in the project of representing ordered monoidal structures in terms of pogroups, the class of so-called integrally closed po-monoids plays a central role. On the one hand, they are precisely the algebras representable as nuclear images of submonoids of po-groups. This vastly extends the previous representation results in this direction, showing in particular that every integral po-monoid arises from a po-group. On the other hand, they also form the basic building blocks of a different construction, which decomposes a (sufficiently well-behaved) po-monoid into a family of subalgebras associated with its positive idempotent elements.

Pozvánka na přednášku Thomas Vetterlein : Quantum logic, dagger categories, and the basic model of quantum physics

@Seminář aplikované matematické logiky30.04.2025 16:00

The idea of associating a non-classical logic with the Hilbert-space model of quantum mechanics goes back to the early days of the development of this physical theory. The success has been modest. Propositions about a quantum physical system correspond to the closed subspaces of a complex Hilbert space and hence their inner structure may be described by an orthomodular lattice. There are calculi that are reasonably called logics of orthomodular lattices. However, a convincing logic doing justice to the canonical model has not been found. Rather, undecidability results have become known. The situation is different if one replaces the framework of logic by the framework of category theory. More specifically, what we propose is to consider a dagger category whose objects are orthosets and whose morphisms are adjointable maps between them. The notion of an orthoset is entirely built on the notion of orthogonality, which in turn stands for mutual exclusion. As in logic, we deal with the interrelations between objects that are to be interpreted as Hilbert spaces. Orthoclosed subspaces, which model yes-no properties in quantum logic, correspond to dagger monomorphisms. Sasaki projections, which interpret in certain quantum logics the implication connective, correspond in the categorical approach to adjoints of inclusion maps. The conjunction of mutually exclusive propositions in quantum logics might finally be seen as corresponding to the formation of categorical biproducts. In the talk, we shall present five non-technical assumptions about a dagger category of orthosets that characterise uniquely the standard model of quantum mechanics.

Pozvánka na přednášku Temur Kutsia : Symbolic Constraints and Quantitative Extensions of Equality

@Seminář aplikované matematické logiky26.02.2025 16:00

Pozvánka na přednášku Joseph McDonald : MacNeille completion, canonical completion, and duality for monadic ortholattices

@Seminář aplikované matematické logiky12.02.2025 16:00

An ortholattice is a bounded lattice equipped with an order-inverting involutive complementation. A monadic ortholattice is an ortholattice equipped with a closure operator, known as a quantifier, whose closed elements form a sub-ortholattice. Monadic ortholattices generalize monadic Boolean algebras - the algebraic model of the classical predicate calculus in a single variable. Janowitz [3] first considered quantifiers on orthomodular lattices, and Harding [1] studied them, as well as cylindric ortholattices, for their connections to von Neumann algebras, in particular, to subfactors. We show that the variety of monadic ortholattices is closed under MacNeille and canonical completions. In each case, the completion of A is obtained by forming an associated dual space X that is a monadic orthoframe. This is a set equipped with an orthogonality relation and an additional binary relation satisfying certain conditions. For the MacNeille completion, X is formed from the non-zero elements of A, and for the canonical completion, X is formed from the proper filters of A. In either case, the corresponding completion of A is then obtained as the complete ortholattice of bi-orthogonally closed subsets of X with an additional operation defined through the binary relation on X. With the introduction of a spectral topology on a monadic orthoframe along the lines of McDonald and Yamamoto [4], we obtain a dual equivalence between the category of monadic ortholattices and homomorphisms and the category of monadic upper Vietoris orthospaces and certain continuous frame morphisms. The duality presented here is obtained in ZF independently of the Axiom of Choice. This talk is based on joint work with John Harding and Miguel Peinado [2]. [1] Harding, J.: Quantum monadic algebras. Journal of Physics A: Mathematical and Theoretical. Vol 55 (2023) [2] Harding, J., McDonald, J., Peinado, M.: Monadic ortholattices: completions and duality. Forthcoming in Algebra Universalis (2025) [3] Janowitz, M.: Quantifiers and orthomodular lattices. Pacific Journal of Mathematics. Vol 13 (1963) [4] McDonald, J., Yamamoto, K.: Choice-free duality for orthocomplemented lattices by means of spectral spaces. Algebra Universalis. Vol. 83 (2022).

Pozvánka na přednášku Martin Q. Putzer : Monadic NP Sets

@Seminář aplikované matematické logiky08.01.2025 16:00

NP languages coincide by Fagin's theorem to certain classes of structures axiomatisable in a certain fragment of second-order logic. The NP vs. coNP problem may then be expressed as a logical problem, without use of complexity theory's terminology. The problem of closure with respect to complementation may then be studied on a hierarchy of fragments of second-order logic - this has been, however, resolved only for the first two members of said hierarchy.