Seminar on Applied Mathematical Logic

The Seminar on Applied Mathematical Logic usually takes place on Wednesdays 4pm in the lecture room 318 of the Institute of Computer Science (Pod Vodárenskou věží 2, Prague 8. See the map). The seminar hosts talks on recent work in mathematical logic and applications by members of the Prague logic community and guests. Talks are often streamed via Zoom.

To join the seminar mailing list, contact Igor Sedlár. For more information on ICS seminars, take a look at the seminar section of the ICS webpages.

The seminar is supported by the Czech Society for Cybernetics and Informatics The seminar archive can be found here.

For students: The seminar can be attended as an optional course (e.g. as course ALG500011 at the Faculty of Arts of Charles University). For more information about this, including grading details, contact Igor Sedlár.

Upcoming talks

• 05.06.2024
  David Cerna (Czech Academy of Sciences, Institute of Computer Science): One is all you need: Second-order Unification without First-order Variables

  We consider the fragment of Second-Order unification, referred to as Second-Order Ground Unification (SOGU), with the following properties: (i) only one second-order variable allowed, (ii) first-order variables do not occur. We show that Hilbert's 10th problem is reducible to a necessary condition for SOGU unifiability if the signature contains a binary function symbol and two constants, thus proving undecidability. This generalizes known undecidability results, as either first-order variable occurrences or multiple second-order variables were required for the reductions. Furthermore, we show that adding the following restriction:(i) the second-order variable has arity 1, (ii) the signature is finite, and (iii) the problem has bounded congruence, results in a decidable fragment. The latter fragment is related to bounded second-order unification in the sense that the number of bound variable occurrences is a function of the problem structure. We conclude with a discussion concerning the removal of the bounded congruence restriction. Joint work with Julian Parsert.

Recent talks

• 24.04.2024
  Tomáš Jakl (Institute of Mathematics of the Czech Academy of Sciences and Czech Technical University): A Personal Perspective on the Game Comonad Programme

  Finite model theory's main focus is in the study of logics that have close connections to descriptive complexity. One of the main tools to show e.g. inexpressibility of certain logics are model comparison games, such as the Ehrenfeucht--Fraisse, pebble, and bisimulation games. The main idea behind game comonads comes from the observation that plays in a typical model comparison game can be encoded into a semantics construction which, moreover, admit the structure of a comonad on the category of relational structures. This allows one to treat model comparison games abstractly, in the language of category theory. In this talk, I give an overview of the game comonad programme, its recent development and open problems. Concretely, I will list the most notable game comonads and explain their relationship with various logic fragments. I will also overview the recent model-theoretic results proved in this framework. I shall also explain how the various different model comparison games can be viewed as an instance of a game in arboreal categories, which are used to axiomatise common features of Eilenberg--Moore categories of coalgebras of game comonads.

• 10.04.2024
  Adam Přenosil (University of Barcelona): Pointed lattice subreducts of varieties of residuated lattices

  The literature on residuated lattices (RLs) contains a number of results describing the lattice reducts of some variety V of RLs. Such results frequently state either that every lattice is a subreduct of some RL in V (for example, if V is the variety of commutative RLs or of cancellative RLs) or that the lattice subreducts are precisely the distributive lattices (for example, if V is the variety of l-groups or of Heyting algebras). We improve on existing results of this form in two ways. Firstly, we consider pointed lattice subreducts (subreducts in the signature expanded by the constant 1 for the multiplicative unit), which gives us more fine-grained information about where exactly a sublattice can occur. Typical properties of interest whose statement requires the signature of pointed lattices are conicity and distributivity at 1. Secondly, instead of considering particular varieties of RLs, we treat semi-K and pre-K RLs uniformly, where K ranges all over positive universal classes of pointed lattices contained in a certain variety. For example, we show that every prelinear RL is distributive and that every preconic RL is distributive at 1. The description of the pointed lattice subreducts of RLs and of CRLs is left as an open problem.

• 13.03.2024
  Filip Jankovec (Czech Academy of Sciences, Institute of Computer Science): Infinitary Rules for Abelian Logic

  In Abelian logic, the reduced models are lattice-ordered Abelian groups. We will focus on three important linear models of Abelian logic: integers, rational numbers and real numbers. These three structures are indistinguishable using finitary rules, but can be separated using infinitary rules. In this talk, we will focus on finding these rules and discuss properties of the corresponding generalized quasivarieties.

• 14.02.2024
  Wesley Fussner (Czech Academy of Sciences, Institute of Computer Science): New directions in quantum reasoning

  The logical underpinnings of quantum mechanics have been the subject of sustained interest since Birkhoff and von Neumann’s pioneering work in the 1930s, but progress has been impeded by the difficulty of several fundamental questions in the area, most notably issues connected to decidability. However, recent years have seen the emergence of a new approach that situates quantum logic within the substructural paradigm, opening the possibility of applying totally new techniques. In this talk, we will discuss these recent trends, report on some important progress arising from this perspective, and identify some open remaining questions.

• 07.02.2024
  Amir Tabatabai (Czech Academy of Sciences, Institute of Mathematics): On Geometric Implications

  It is a well-known fact that although the poset of open sets of a topological space is a Heyting algebra, its Heyting implication is not necessarily stable under the inverse image of continuous functions and hence is not a geometric concept. This leaves us wondering if there is any stable family of implications that can be safely called geometric. In this talk, we will first introduce an abstract notion of implication as a binary modality and investigate its basic properties and possible representations. Then, we will use a weaker version of categorical fibrations to define the geometricity of a category of pairs of spaces and implications over a given category of spaces. We will characterize all geometric categories over a given category S, provided that S has some basic closure properties. Specifically, we will show that there is no non-trivial geometric category over the full category of spaces.

• 31.01.2024
  Nicholas Ferenz (Czech Academy of Sciences, Institute of Computer Science): Relevance Properties in First-Order Relevant Logics

  In this work-in-progress talk I begin the discussion of relevance properties available in first-order logics. I explore the philosophical motivation for many first-order variants of the Variable Sharing Property, and show of some logics whether or not they satisfy these properties. Future mathematical and philosophical directions are outlined.

• 25.01.2024, special session
  Soroush Rafiee Rad (University of Amsterdam): On Decidability of Inductive Logic

  We show that while standard first-order inductive logic is not decidable, a large class of inferences in objective Bayesian inductive logic is decidable. Decidability is achieved by reducing the general inference problem to a quantifier-free problem. We show that for any inference if the quantifier-free reduction of the premisses is satisfiable, then the original inference is decidable. We also consider inferences with infinitely many premisses and explore some properties of the logic.

• 24.01.2024
  Simon Santschi (University of Bern): Equational theories of idempotent semifields

  An idempotent semifield is an idempotent semiring such that its multiplicative reduct is a group. In this talk I will present several results about equational theories of idempotent semifields. The results include that no non-trivial class of idempotent semifields has a finitely based equational theory; that there are continuum-many equational theories of idempotent semifields; and that the equational theory of the class of all idempotent semifields is co-NP-complete. This is joint work with George Metcalfe.

• 17.01.2024
  Roman Kuznets (TU Wien): What Proof Theory Can Do for You

  Although the prime object of study for structural proof theory is proof calculi (especially analytic ones), it has many applications to important logical properties, such as conservativity, consistency, decidability, complexity, interpolation, etc. In my talk, I will present some recent successes in solving long-time open problems by proof-theoretic means, including the Lyndon interpolation property for Gödel logic (intermediate logic of linear frames) and the decidability of (bimodal) intuitionistic S4.

• 13.12.2023
  Anantha Padmanabha (Indian Institute of Technology, Dharwad): Decidable Fragments of First Order Modal Logic

  First Order Modal Logic (FOML) extends First Order Logic (FO) with modal operators. FOML is suitable for many applications including planning, predicate epistemic logics among others. However, FOML is computationally unfriendly. Most of the decidable fragments of FO that are decidable (like the two variable fragment, guarded fragment, restriction to unary predicates) become undecidable when extended with modal operators. Until recently, the only known decidable fragment of FOML was the monodic fragment. In this talk we will discuss some new and interesting decidable fragments of FOML and its variants that we have identified. This talk includes some of the results from the speaker's PhD thesis (supervised by R. Ramanujam) and some results in collaboration with Mo Liu, R. Ramanujam and Yanijing Wang.

• 08.11.2023
  Wesley Fussner (Czech Academy of Sciences, Institute of Computer Science): A Tour of Substructural Interpolation

  "Interpolation" refers to a cluster of fundamental metalogical properties with applications spanning hardware and software verification, databases, and many other areas. In this talk, we survey the state of the art on interpolation in substructural logics, focusing in particular on big-picture features that shed some light on the nature of interpolation generally. We will also discuss some of the most important remaining open questions and on-going efforts to solve them.

• 01.11.2023
  Zuzana Haniková (Czech Academy of Sciences, Institute of Computer Science): Maximum satisfiability problem in the real-valued MV-algebra

  In propositional Boolean logic, maximum satisfiability (MaxSAT) problem can be viewed as a generalization of the SAT problem. An input to the SAT problem is a CNF formula (a list of clauses) and the question is whether there is an assignment that satisfies all of them. MaxSAT is an optimization problem, namely to determine the maximum number of satisfied clauses in the list, over all assignments. Our work addresses the MaxSAT problem problem for a list of arbitrary formulas in the language of propositional Łukasiewicz logic, over the semantics provided by the MV-algebra on the real interval [0,1]. First we reduce the MaxSAT problem to the SAT problem in the same semantics. This provides a classification against which other approaches to the problem can be compared. Then we define a tableau-like method that eventually yields one or more systems of linear constraints, similar to the earlier approaches of Hähnle or Olivetti. This is joint work with Felip Manya and Amanda Vidal, presented at Tableaux 2023.

• 04.10.2023
  Andrew Tedder (University of Vienna): Negated Implications in Connexive Relevant Logics

  Adding connexive theses to relevant logics has the unsavoury result of allowing one to prove every negated implication. In this talk, I'll diagnose this problem, and consider some avenues by which this result can be avoided.

• 26.06.2023
  Filip Jankovec (Czech Academy of Sciences, Institute of Computer Science): From Abelian logic to Łukasiewicz unbound

  In this talk, we investigate connections between the family of comparative logics including Abelian logic, and some generalizations of Łukasiewicz logic. We provide axiomatizations for some extensions of pointed Abelian logic including unbound Łukasiewicz logic. We show the importance of the semilinearity property and we present the discrete versions of unboud Łukasiewicz logic. This talk is based on joint work with Marta Bílková, Petr Cintula and Carles Noguera.



• 07.06.2023
  Vít Punčochář (Czech Academy of Sciences, Institute of Philosophy): Fuzzy Information States and Fuzzy Support

  The semantic framework for representing questions known as inquisitive semantics is based on a relation of support relating formulas and information states (modeled as sets of possible worlds). In my talk I will discuss two ways of fuzzifying inquisitive semantics. The first one replaces crisp information states with fuzzy information states (modeled as fuzzy sets of possible worlds). The second one replaces the crisp notion of support with a notion of fuzzy support. I will show some properties of the resulting framework. For example, I will show that if we fuzzify inquisitive semantics in these two different directions, we obtain an abstract and very general version of a principle known from the basic inquisitive semantics as Truth-Support Bridge. I will also sketch some open questions related to this approach.



• 17.05.2023
  Hans van Ditmarsch (University of Toulouse, CNRS, IRIT): Everyone Knows that Everyone Knows

  A gossip protocol is a procedure for sharing secrets in a network. The basic action in a gossip protocol is a telephone call wherein the calling agents exchange all the secrets they know. An agent who knows all secrets is an expert. The usual termination condition, given a finite number of agents, is that all agents are experts. We report on research investigating the termination condition that all agents know that all agents are experts. If agents only exchange secrets, there is no knowledge of the time, and no knowledge of the protocol, even stronger termination conditions are unreachable. Furthermore, n-2 + (n choose 2) calls are optimal to reach this epistemic goal. Although it is easy to come up with schedules achieving this, it is remarkably non-trivial to show that they are optimal.

  Some references:

  1. Martin Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, Pierre Régnier: The epistemic gossip problem. Discrete Mathematics 342(3), pp 654-663, 2019.
  2. Hans van Ditmarsch, Malvin Gattinger, Rahim Ramezanian: Everyone Knows that Everyone Knows: Gossip Protocols for Super Experts. Studia Logica, to appear, 2023. https://doi.org/10.1007/s11225-022-10032-3
  3. Hans van Ditmarsch, Malvin Gattinger: The Limits to Gossip: Second-Order Shared Knowledge of All Secrets is Unsatisfiable. Proceedings of WoLLIC, pp 237-249, 2022.

• 10.05.2023
  Emil Jeřábek (Czech Academy of Sciences, Institute of Mathematics): A Simplified Lower Bound on Intuitionistic Implicational Proofs

  One of the major open problems in classical proof complexity is to prove super-polynomial lower bounds on the length of proofs in Frege (aka Hilbert-style) systems, or equivalently, sequent calculus or natural deduction. Interestingly, exponential lower bounds are known for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubeš (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that the presence of disjunction is essential for these lower bounds, but Jeřábek (2017) adapted them to the purely implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon–Boppana). In this talk, I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene’s slash. Apart from Frege, it applies directly to sequent calculus and (dag-like) natural deduction, obviating also the need for translation of these proof systems to Frege. One motivation for this work comes from presistent claims by Gordeev and Haeusler, who purport to show that all intuitionistic implicational tautologies have polynomial-size dag-like natural deduction proofs, implying NP = PSPACE. Their claims are false as they contradict the above-mentioned exponential lower bounds (and, in fact, also older exponential lower bounds on constant-depth proofs), but for a non-specialist, understanding this requires tracking down multiple papers and some reading between the lines. Our argument consolidates all proof-theoretic components of the lower bound into one simple proof, depending only on the Alon–Boppana circuit lower bound.



• 03.05.2023
  Kentaro Yamamoto (Czech Academy of Sciences, Institute of Computer Science): How to compute uniform interpolant semantically

  This talk will be a tutorial of a known technique on computing uniform interpolants by examining finite (or finitely generated) algebras and their extensions. We will focus on intermediate logics, but the method is reasonably general.



• 19.04.2023
  Libor Barto (Charles University, Faculty of Mathematics and Physics): Promise Model Checking Problems over a Fixed Model

  The fixed-template constraint satisfaction problem (CSP) can be seen as the problem of deciding whether a given primitive positive first-order sentence is true in a fixed structure (also called model). We study a class of problems that generalizes the CSP simultaneously in two directions: we fix a set L of quantifiers and Boolean connectives, and we specify two versions of each constraint, one strong and one weak. Given a sentence which only uses symbols from L, the task is to distinguish whether the sentence is true in the strong sense, or it is false even in the weak sense. We classify the computational complexity of these problems for the existential positive equality-free fragment of first-order logic and we prove some upper and lower bounds for the positive equality-free fragment. The partial results are sufficient, e.g., for all extensions of the latter fragment. This is a joint work with Kristina Asimi and Silvia Butti.



• 22.03.2023
  Ivo Pezlar (Institute of Philosophy, Czech Academy of Sciences): Computational Content of a Generalized Kreisel-Putnam Rule

  In this talk, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid? Our answer is positive for the Split rule as well as for its newly proposed generalized versions.



• 08.03.2023
  Alexander Leitsch (Technical University Vienna): First-Order Proof Schemata and Inductive Proof Analysis

  Proofs are more than just validations of theorems; they can contain interesting mathematical information like bounds or algorithms. However this information is frequently hidden and proof transformations are required to make it explicit. One such transformation on proofs in sequent calculus is cut-elimination (i.e. the removal of lemmas in formal proofs to obtain proofs made essentially of the syntactic material of the theorem). In his famous paper ``Untersuchungen ueber das logische Schliessen'' Gentzen showed that for cut-free proofs of prenex end-sequents Herbrand's theorem can be realized via the midsequent theorem. In fact Gentzen defined a transformation which, given a cut-free proof p of a prenex sequent S, constructs a cut-free proof p' of a sequent S' (a so-called Herbrand sequent) which is propositionally valid and is obtained by instantiating the quantifiers in S. These instantiations may contain interesting and compact information on the validity of S. Generally, the construction of Herbrand sequents requires cut-elimination in a given proof p (or at least the elimination of quantified cuts). The method CERES (cut-elimination by resolution) provides an algorithmic tool to compute a Herbrand sequent S' from a proof p (with cuts) of S even without constructing a cut-free version of p. A prominent and crucial principle in mathematical proofs is mathematical induction. However, in proofs with mathematical induction Herbrand's theorem typically fails. To overcome this problem we replace induction by recursive definitions and proofs by proof schemata. An extension of CERES to proof schemata (CERESs) allows to compute inductive definitions of Herbrand expansions (so-called Herbrand systems) representing infinite sequences of Herbrand sequents, resulting in a form of Herbrand's theorem for inductive proofs.



• 01.03.2023
  Nicholas Ferenz (Institute of Computer Science, Czech Academy of Sciences): One-variable RQ & RS5: A Frame Based Equivalence

  Often, for a propositional logic L, some one-variable fragment of L's first order extension corresponds to some modal logic on L. For the relevant logic R, it seems that the one-variable fragment of RQ (the stronger of R's two standard first-order extensions) corresponds to the modal relevant logic RS5 (the S5ish axiomatic extension of R which contains classical S5 in translation). This talk is a work in progress showing this equivalence. One direction of the equivalence is obtained by transforming first-order models into modal models. The other direction is (almost) obtained by evaluating all of RQ in a particular modal model. I also discuss some philosophical upshots/consequences of this result.



• 25.01.2023
  Igor Sedlár (Institute of Computer Science, Czech Academy of Sciences): Kleene Algebra With Tests for Weighted Programs

  Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular expressions with applications in proving program equivalence. We extend the language of Kleene algebra with tests so that it is sufficient to formalize reasoning about a simplified version weighted programs. We introduce relational semantics for the extended language, and we generalize the relational semantics to an appropriate extension of Kleene algebra with tests, called Kleene algebra with weights and tests. We demonstrate by means of an example that Kleene algebra with weights and tests offers a simple algebraic framework for reasoning about equivalence and optimal runs of weighted programs.



• 11.01.2023
  Guillermo Badia (University of Queensland): A Parametrised Axiomatization for a Large Number of Restricted Second-Order Logics

  By limiting the range of the predicate variables in a second-order language one may obtain restricted versions of second-order logic such as weak second-order logic or definable subset logic. In this note we provide an infinitary strongly complete axiomatization for several systems of this kind having the range of the predicate variables as a parameter. The completeness argument uses simple techniques from the theory of Boolean algebras. This is joint work with John L. Bell (see https://arxiv.org/abs/2207.02709).



• 14.12.2022
  Zuzana Haniková (Czech Academy of Sciences, Institute of Computer Science): Vopěnka's Alternative Set Theory and its mathematical context

  This talk will be an exposition of Vopěnka's Altenative Set Theory (AST), as first presented in his monograph "Mathematics in the Alternative Set Theory" published by Teubner Verlag in 1979, in relation to some pertinent mathematical developments of the 20th century; namely, Skolem's work in nonstandard models of arithmetic, Vopěnka's nonstandard models of set theory, Robinson's nonstandard analysis, Vopěnka and Hájek's work in the theory of semisets, or Parikh's almost consistent theories. My aim will be to lay out the design choices Vopěnka made for the AST, and to discuss possible inspiration for them. In addition to the Teubner book, I will rely on ``Introduction to Mathematics in the Alternative Set Theory'', published in 1989 in Slovak. This talk is based on my paper "Vopěnkova Alternativní teorie množin v matematickém kánonu 20. století", recently published in Filosofický časopis; English translation available as arXiv:2211.11020.



• 07.12.2022
  Chun-Yu Lin (Czech Academy of Sciences, Institute of Computer Science): On Many-Valued Coalgebraic Modal Logic

  A well-known result in coalgebraic modal logic is that its completeness can be determined at the one-step level. We generalize the result to the finitely many-valued case by using the canonical model construction method. We prove the result for coalgebraic modal logics based on three different many-valued algebraic structures, including the finitely-valued {\L}ukasiewicz algebra, the commutative integral Full-Lambek algebra (FL$_{ew}$-algebra) expanded with canonical constants and Baaz Delta, and the FL$_{ew}$-algebra expanded with valuation operations. On the other hands, we also generalize Pattinson's stratification method for colagebraic modal logic to the many-valued setting. In contrast to standard techniques of canonical model construction, this method employs an induction principle to prove the soundness and completeness the logics. This talk is based on joint works with Dr.Churn-Jung Liau in Academia Sinica, Taiwan.



• 30.11.2022
  Colin Zwanziger (Czech Academy of Sciences, Institute of Philosophy): S4 Necessity and Comonads

  I will delineate the categorical semantics of S4 necessity operators, in settings ranging from propositional logic up to dependent type theory. In each setting, the semantics of the S4 necessity operator is given by a suitable *comonad*. We will see that S4 modal dependent type theory (Nanevski et al. 2008) has the advantage of subsuming both S4 modal predicate logic and intensional logic, while adding the expressive power of dependent types. The comonadic semantics for this dependent type theory is adapted from Zwanziger (2022).



• 23.11.2022
  Thomas M. Ferguson (Czech Academy of Sciences): Beyond Parry: Applications of Intensional Subject-Matter

  A number of philosophers working in logical frameworks that are sensitive to models of topic---like Fine and Berto---have taken note that intensional operators can have a transformative effect on a sentence's overall subject-matter. With its implicit model of topic playing a central role, Parry's logic of analytic implication (PAI) has proven a very fertile setting to explore the topic-theoretic contributions made by intensional operators. Parry's framework thus serves as a satisfactory incubator in which the theory of intensional topics can mature. In this talk, I would like to show how the lessons learned about intensionality and topic within this context can be ported to other settings. In particular, I will review some issues in Berto's theory of topic-sensitive intentional modals (TSIMs) and show how techniques incubated in Parry's context can supply solutions to limitations with several interpretations of TSIMs.



• 09.11.2022
  Miguel Martins (University of Barcelona): The Bi-Intuitionistic Logic of Co-Trees

  A bi-Heyting algebra validates the Gödel-Dummett axiom (p \to q) \lor (q \to p) iff the poset of its prime filters is a disjoint union of co-trees (i.e., order duals of trees). Bi-Heyting algebras of this kind are called bi-Gödel algebras and form a variety that algebraizes the extension bi-LC of bi-intuitionistic logic axiomatized by the Gödel-Dummett axiom. In this talk, we will present some of our contributions to the study of the lattice Ext(bi-LC) of extensions of bi-LC. We developed the methods of Jankov-style formulas for bi-Gödel algebras and used them to prove that there are exactly continuum many extensions of bi-LC. We also showed that all these extensions can be uniformly axiomatized by canonical formulas. Our main result is a characterization of the locally tabular extensions of bi-LC. We introduced a sequence of co-trees, called the finite combs, and showed that a logic in Ext(bi-LC) is locally tabular iff it contains at least one of the Jankov formulas associated with the finite combs. It follows that there exists the greatest non-locally tabular extension of bi-LC and consequently, a unique pre-locally tabular extension of bi-LC. These results contrast with the case of the intermediate logic axiomatized by the Gödel-Dummett axiom, which is known to have only countably many extensions, all of which are locally tabular. This is joint work with Nick Bezhanishvili and Tommaso Moraschini.



• 02.11.2022
  Daniil Kozhemiachenko (INSA Centre Val de Loire): Crisp bi-Gödel modal logic and its paraconsistent expansion

  We provide a Hilbert-style axiomatisation for the crisp bi-G\"{o}del modal logic $\KbiG$. We prove its completeness w.r.t. crisp Kripke models where formulas at each state are evaluated over bi-G\"{o}del algebra $[0,1]$. We also consider a paraconsistent expansion of $\KbiG$ with a De Morgan negation $\neg$ which we dub $\KGsquare$. We devise a Hilbert-style calculus for it and prove its completeness w.r.t. crisp Kripke models with two valuations over $[0,1]$ as a consequence of a~conservative translation from $\KbiG$ to $\KGsquare$. We also study semantical properties of $\KbiG$ and $\KGsquare$. In particular, we show that Glivenko theorem holds only in finitely branching frames. We also explore the classes of formulas that define the same classes of frames both in $\mathbf{K}$ (the classical modal logic) and $\KG^c$. We show that, among others, all Sahlqvist formulas and all formulas $\phi\rightarrow\chi$ where $\phi$ and $\chi$ are monotone, define the same classes of frames in $\mathbf{K}$ and $\KG^c$. The presentation is based on joint work with Marta Bílková and Sabine Frittella.



• 19.10.2022
  Adam Přenosil (Institute of Computer Science, CAS): A module-theoretic approach to multiset consequence relations

  The syntax of abstract algebraic logic (AAL) lives in the powerset of the algebra of formulas, in the sense that logics are defined as structural closure operators on this powerset. While this assumption has served well as the bedrock of AAL, much of the architecture of AAL does not depend on the particular properties of the formula powerset. Blok and Jónsson took the first step in this direction when they replaced the formula powerset in the basic theory of algebraization by the powerset of an M-set (a set with a monoid action). Galatos and Tsinakis then took this abstraction even further, replacing the powerset by a complete lattice. A resource-conscious logician might then wish to take a further step and allow for a different, "multiplicative" way of combining syntactic objects, thus obtaining an abstraction of multiset-based consequence relations. An attempt to stretch the framework of Galatos and Tsinakis in this direction was already made in a 2019 paper by Cintula, Gil-Feréz, Moraschini and Paoli. We provide a different answer to the same problem and explain why we find it preferable to the existing one. (This talk is based on joint work with Constantine Tsinakis.)



• 05.10.2022
  Igor Sedlár (Institute of Computer Science, CAS): On the Complexity of *-Continuous Kleene Algebra With Domain

  We prove that the problem of deciding membership in the equational theory of *-continuous Kleene algebra with domain is EXPTIME-complete. Our proof makes essential use of Hollenberg's equational axiomatization of program equations valid in relational test algebra. We also identify a weak version of Kleene algebra with domain, called Kleene algebra with literals, KAL, and we show that the equational theory of this class of algebras is PSPACE-complete.



• 08.06.2022
  Michal Botur (Palacký University Olomouc): Perfect pseudo MV-algebra, kite, variety, representation

  We study the structure of perfect residuated lattices, focussing especially on perfect pseudo MV-algebras. We show that perfect pseudo MV-algebras can be represented as a generalised version of Kowalski and Dvurečenskij's kites. We characterise varieties generated by kites and describe the lattice of these varieties as a complete sublattice of the lattice of perfectly generated varieties of perfect pseudo MV-algebras.



• 31.05.2022
  Davide Fazio (University of Cagliari): On a logico-algebraic approach to AGM belief contraction theory

  In this talk we investigate an algebraic approach to AGM (Alchourrón, Gärdenfors, Makinson) logic of theory change by using the tools of abstract algebraic logic. Specifically, we generalize the notions involved in the definition of epistemic operators, in particular contraction, to arbitrary finitary propositional logics, and we show how to switch from a syntactic-based approach to a semantic one. This allows to build a solid bridge between the validity of AGM postulates in a propositional logic and specific algebraic properties of its intended algebraic counterpart. Such a connection deserves particular attention when we deal with maxichoice contractions. We close the talk by discussing open problems and further developments of the above framework. Joint work with M. Pra Baldi.



• 18.05.2022
  Igor Sedlár (ICS CAS): One-sorted Kleene algebra with tests

  Kleene algebra with tests, KAT, is a simple two-sorted algebraic framework for verifying properties of propositional while programs. One-sorted alternatives to KAT have been explored, mainly in connection with applications in automated program verification. A well known example of this approach is Kleene algebra with domain, KAD. A generalization of KAD called one-sorted Kleene algebra with tests, OneKAT, was recently proposed by the author in collaboration with J. Wannenburg. In this paper we show that KAT can be transformed into a flexible one-sorted framework that retains all natural properties of KAT. This framework, called Kleene algebra with test operators, is based on the idea of extending Kleene algebra with a set of test operators such that the set of images of the multiplicative unit under test operators generates a Boolean algebra of tests.



• 27.04.2022
  Rostislav Horčík (Czech Technical University): Homomorphisms of Planning Tasks and Heuristic Search

  Classical planning tasks are modeled in the Planning Domain Description Language (PDDL), a schematic language based on first-order logic. Using a grounding process, most state-of-the-art planners turn this first-order representation into a propositional one. However, grounding may cause an exponential blowup. Therefore, investigating methods for computing plans directly on the first-order level is essential. To build such a first-order planner, one must invent an admissible heuristic navigating the search algorithm like A* without grounding the original planning task. We introduce homomorphisms between PDDL tasks that allow us to transform a PDDL task into a smaller one by reducing the number of its objects. Consequently, one can compute an admissible heuristic for the original task in the smaller one.



• 13.04.2022
  Vít Punčochář (FLU CAS): Layers of Propositional Types

  In my talk I will describe a framework that is based on the idea that various logical expressions, e.g. modal adverbs or the conditional ‘if’, generate statements that provide information of different types. This idea is partly inspired by the team semantics for propositional dependence logic but deviates from it in several respects. Most importantly, instead of the two semantic layers used in dependence logic -- possible worlds and teams -- a whole hierarchy of contexts is introduced and different types of formulas are evaluated at different levels of this hierarchy. This leads to a rich stratification of informational types. I will explore the formal aspects of this approach and apply it to a number of puzzling phenomena related to modalities and conditionals.



• 02.03.2022
  Martin Suda (CIIRC, Czech Technical University): Integrating Machine Learning into Saturation-based ATPs

  Applying the techniques of machine learning (ML) promises to dramatically improve the performance of modern automatic theorem provers (ATPs) and thus to positively impact their applications. The most successful avenue in this direction explored so far is machine-learned clause selection guidance, where we learn to recognize and prefer for selection clauses that look like those that contributed to a proof in past successful runs. In this talk I present Deepire, an extension of the ATP Vampire where clause selection is guided by a recursive neural network (RvNN) for classifying clauses based solely on their derivation history.



• 23.02.2022
  Andrew Tedder (Ruhr University Bochum): Kapsner Complementation

  In this paper I discuss a class of algebras appropriate to model, and, philosophically speaking, also to capture the central commitments of, Kapsner Strongly Connective logics. I introduce this class of logics, and its relation to standard connexive systems, introduce the class of algebras, comparing with some work on algebraic semantics of connexive logics by Storrs McCall, and give some examples. I close with some avenues of future work and open problems.



• 02.02.2022
  Nicholas Ferenz (ICS CAS): Conditional FDE-logics

  The logic FDE, especially in its four-valued presentation, and sometimes referred to as the Belnap-Dunn logic due to its origins in the work of both Nuel Belnapand J. Michael Dunn, is typically presented without a conditional connective. Moreover, adding a conditional to FDE is not always straightforward, and sometimes presents interesting problems. An infamous problem shared by many paraconsistent logics is that the standard definitions of the material conditional (via disjunction and negation) result in a conditional for which modus ponens is not valid. While there are several extensions and expansions of FDE with a conditional connective, the present work adds to this list by combining Dunn's two-valued relational approach to FDE with conditionals, where the conditionals are defined (semantically) as in the conditional logics presented by Chellas in his 1975 paper "Basic conditional logic" and in chapter 10 of his 1980 book "Modal Logic". In addition, we present a general frame semantics that, strictly speaking, is only necessary for some of the extensions (quantified or propositional) of the base logics constructed here.



• 19.01.2022
  David Cerna (ICS CAS): Learning Higher-Order Logic Programs From Failures

  Learning complex programs through inductive logic programming (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile Learning From Failures paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Furthermore, we provide a theoretical framework capturing the class of higher-order definitions handled by our extension. (Joint work with Stanisław J. Purgał and Cezary Kaliszyk.)



• 10.11.2021
  Jamie Wannenburg (ICS CAS): A Generalization of Ultraproducts

  A construction, called ‘prime products’ will be presented that generalizes the ultraproduct construction (which is often used to create non-standard models in universal algebra and model theory). This construction will be tied to ‘positive’ formulas, in a manner that is analogous to how ultraproducts are tied to ‘full’ first order formulas—with negation. In particular, there is an analogue of Łoś’ Theorem, implying that prime products preserve existential positive formula (EPF). Furthermore, one can show that a class K of algebras is axiomatized by ‘coherent sentences’ (universally quantified implications between EPF) iff K is closed under ultraroots and prime products. There is also a limited analogue of the Łoś-Suszko Theorem, which holds for any quasivariety K of finite type with a finite nontrivial member: The nontrivial members of K satisfy the same existential positive sentences iff the nontrivial members of K have isomorphic ‘prime powers’. This condition is known as ‘passive structural completeness’.



• 03.11.2021
  Kentaro Yamamoto (ICS CAS): The automorphism groups of ultrahomogeneous lattices

  This is a continuation of the talk the presenter gave last year on the automorphism group Aut(L) of the countable ultrahomogeneous Heyting algebra L universal with respect to all finite Heyting algebras, the smallest model of the model completion of their first-order theory. After reminding ourselves of the relevant definitions, we look at an elementary construction showing that the automorphism group of L is not topologically isomorphic to any of those of better-known ultrahomogeneous lattices. We then go over the notion of independence among finite subsets of L that can be used to establish the simplicity of Aut(L). The notion of independence derives from the superamalgamation property of the age of L. Finally, we will discuss future work regarding the automorphism group of a structure and the superamalgamation property of its age.



• 27.10.2021
  Sara Ayhan (Ruhr University Bochum): Reduction procedures and the meaning of proofs

  What are ‘good’ reduction procedures and why is it important to distinguish these from ‘bad’ ones? It has been argued that from a philosophical point of view, or more specifically a standpoint of proof-theoretic semantics, reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the same conclusion would have to be identified (see Schroeder-Heister, P. & Tranchini, L. (2017). Ekman’s Paradox. Notre Dame Journal of Formal Logic, 58(4), 567-581). Therefore, we need to be careful: We cannot just accept any reduction procedure, i.e. any procedure eliminating some kind of detour in a derivation. I agree with this conclusion, however, I will argue that the question, which reductions we accept in our system, is not only important if we see them as generating a theory of proof identity but is also decisive for the more general question whether a proof has meaningful content. By annotating derivations and reductions with lambda terms in accordance with the Curry-Howard-correspondence, it becomes much clearer what may be wrong with certain reductions. I will give examples of such reductions and show that allowing these would not only trivialize identity of proofs of the same conclusion but that it would allow to reduce a term of one type to the term of an arbitrary other. The lambda calculus and some well-known properties thereof can provide us with directions as to why this happens in these cases but not in the cases of ‘well-behaved’ reductions. If we take reductions as inducing an identity relation then that would force us to dentify proofs of different arbitrary formulas. But even if we reject this assumption about proof identity, I will argue that allowing such reductions would render derivations in such a system meaningless.



• 20.10.2021
  David Fernández Duque (ICS CAS and Ghent University): Decidability of some intuitionistic and Gödel modal logics with transitivity

  There are various modal logics in the literature based on intuitionistic or Gödel logic, with the general pattern that very weak logics such as K, or very strong logics such as S5, are known to be decidable, but the decidability of "intermediate" logics such as S4 is or was unknown. We discuss relatively recent techniques that can be used to prove the decidability of many of these logics via finite 'bi-relational' models, and state several results obtained in this way. (Joint work with Philippe Balbiani and Martín Diéguez)