RNDr. Tomáš Jakl, Ph.D.

Článek

10.1007/s11225-026-10230-3

Katedra teoretické informatiky

We review four areas of theoretical computer science which share technical or philosophical ideas with the work of Belnap on his useful four-valued logic. Perhaps surprisingly, the inspiration by Belnap-Dunn logic is acknowledged only in the study of d-frames. The connections of Belnap's work and linear logic, Blame Calculus or the study of LVars are not openly admitted. The key to three of these connections with Belnap's work go via the twist-product representation of bilattices. On the one hand, it allows us to view the class of models of linear logic built using the Chu construction as based on Belnap-Dunn logic. On the other hand, twist-product representation theorems are essential in the theory of d-frames and, also, the key theorem of Blame Calculus is essentially a twist-product representation theorem too, albeit with a strong proof-theoretic flavour.

Článek

10.46298/lmcs-21(4:10)2025

Katedra teoretické informatiky

We present a categorical theory of the composition methods in finite model theory -- a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman--Vaught--Mostowski (FVM) type theorems, which characterize how logical equivalence behaves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the existential and positive existential fragments, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments. This is an extended version of the LiCS 2023 conference paper of the same name.

Článek

10.1007/s10485-025-09802-6

Katedra teoretické informatiky

We study restrictions of the correspondence between the lattice SE(L) of strongly exact filters, of a frame L, and the coframe So(L) of fitted sublocales. In particular, we consider the classes of exact filters E(L), regular filters R(L), and the intersections J(CP(L)) and J(SO(L)) of completely prime and Scott-open filters, respectively. We show that all these classes of filters are sublocales of SE(L) and as such correspond to subcolocales of So(L) with a concise description. The theory of polarities of Birkhoff is central to our investigations. We automatically derive universal properties for the said classes of filters by giving their descriptions in terms of polarities. The obtained universal properties strongly resemble that of the canonical extensions of lattices. We also give new equivalent definitions of subfitness in terms of the lattice of filters.

Stať ve sborníku

10.1109/LICS56636.2023.10175751

Katedra teoretické informatiky

We present a categorical theory of the composition methods in finite model theory – a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman–Vaught–Mostowski (FVM) type theorems, which characterize how logical equivalence be- haves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the positive existential fragment, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments.