Seminar on Applied Mathematical Logic

Upcoming Talks

Recent Talks

• 30.04.2025
  
  Thomas Vetterlein (Johannes Kepler University Linz): Quantum logic, dagger categories, and the basic model of quantum physics

  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.

• 23.04.2025
  
  Václav Cenker (Palacky University in Olomouc): Free Algebras in Finitely Generated Varieties of Commutative BCK-Algebras

  In this talk, I will present a description of finitely generated free algebras in certain finitely generated varieties of commutative BCK-algebras. The construction relies on homomorphisms from free commutative BCK-algebras to free ŁBCK-algebras that extend the insertion of generators, allowing us to draw on existing results. A key step involves analyzing valuations and their equivalence classes, which leads to a precise count of the elements of the free algebras and a full structural characterization. In the final part of the talk, I will outline some ongoing work and open questions concerning the axiomatization of subvarieties of commutative BCK-algebras.

• 16.04.2025
  
  Sam Braunfeld (Institute of Computer Science, Czech Academy of Sciences and Faculty of Mathematics and Physics, Charles University): Orbit-counting for groups acting on countable sets

  Beginning in the 1970s, Peter Cameron generalized the classical problem of counting the orbits of a finite group action by considering actions on countable sets. These actions naturally give rise to infinite sequences of integers, including many classical sequences. The asymptotic behavior of these sequences was conjectured to be tightly constrained, falling into narrow bands with large gaps. We will indicate the proofs of these conjectures and their fundamental connection to model theory.

• 26.03.2025
  
  Daniele Nantes (Imperial College London): Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

  The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction. We evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool grounded on a common formal compositional symbolic execution engine to support both correctness and incorrectness reasoning. Joint work with Andreas Lööw, Philippa Gardner, et al. (Imperial College London).

• 19.03.2025
  
  Adam Přenosil (University of Barcelona): Hölder's theorem for totally ordered monoids

  A fruitful research programme in the study of residuated lattices has been to take inspiration from results about lattice-ordered groups and extend them to wider classes of residuated lattices. Two important classes for this purpose are the variety of GBL-algebras and its subvariety of GMV-algebras, which significantly extend the variety of lattice-ordered groups while still preserving some group-like behavior. One classical result about ordered groups which has been extended in this way is Hölder's theorem. This theorem is an abstract characterization of the totally ordered groups which embed into the additive ordered group of reals R as precisely the Archimedean ones (i.e. those which lack infinitesimal elements). In their study of the Archimedean property in residuated lattices, Ledda, Paoli and Tsinakis recently extended Hölder's theorem to an abstract characterization of algebras which embed either into the reals R, or into the negative cone of the reals R-, or into the standard MV-chain [0, 1] as precisely the so-called strongly simple GBL-algebras. In the present joint work with Luca Spada, we further extend Hölder's theorem beyond the residuated setting, obtaining an abstract characterization of the dense submonoids of the totally ordered monoids R, R-, and [0, 1].

• 05.03.2025
  
  Nicholas Ferenz (University of Lisbon): Topics, Focus, and Relevance Properties in First-Order Relevant Logic

  We investigate the problem of providing relevance properties for first order logics by expanding on recent work concerning relevance as topical in propositional relevant logics. We propose a theory of topic for first order languages, relying on the use of focus markers in an extension of the usual first order language, and suggest how such an enrichment of the language and conceptual apparatus of the logic can provide avenues into the first order relevance problem.

• 26.02.2025
  
  Temur Kutsia (Johannes Kepler University Linz): Symbolic Constraints and Quantitative Extensions of Equality

  Quantitative extensions of equality characterize the degree of approximation between objects. Fuzzy proximity and similarity relations are notable examples of such extensions. These and similar relations are used to model concepts such as vagueness, uncertainty, imprecision, and imperfection. Various approaches to formalizing quantitative information have led to the development of well-known logical, algebraic, and topological formalisms and structures, such as fuzzy logic, rough logic, metric algebras, quantitative algebras, metric and proximity spaces, etc.

  Symbolic constraint solving is ubiquitous in many areas of mathematics and computer science. Unification, matching, anti-unification, disunification, and ordering constraints are prominent examples that play a crucial role in automated reasoning, term rewriting, declarative programming, and their applications. In this talk, we present recent advances in solving unification and anti-unification constraints in theories where equality is replaced by its quantitative approximation. Our algorithms solve unification and anti-unification problems modulo fuzzy tolerance relations (i.e., reflexive and symmetric but not necessarily transitive), allowing mismatches between symbol names and arities. We will discuss the general principles behind these techniques, provide examples, present some of the algorithms, and characterize their properties.

• 12.02.2025
  
  Joseph McDonald (University of Alberta): MacNeille completion, canonical completion, and duality for monadic ortholattices

  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)

• 08.01.2025
  
  Martin Q. Putzer (Charles University, Faculty of Arts): Monadic NP Sets

  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.

• 11.12.2024
  
  Chun-Yu Lin (Czech Academy of Sciences, Institute of Computer Science): Nonclassical Polyadic Algebra : Soft and Hard

  In this talk, I will characterize the polyadic algebras arising from algebraic implicative predicate logic, and prove a functional representation theorem. Then I will address the categorical formulation for non-classical polyadic algebras.

• 04.12.2024
  
  Daniil Kozhemiachenko (Aix-Marseille Université): Filter-induced entailment relations in paraconsistent Gödel logics

  We consider two expansions of Gödel logic with two versions of paraconsistent negation. The first one is G_inv — the expansion with an involuitive negation ~_i defined via v(~_iA)=1-v(A). The second one is G^2 --- an expansion with a so-called ‘strong negation’ ¬. This logic utilises two independent valuations on [0,1] — v_1 (positive support) and v_2 (negative support) that are connected via ¬. Two valuations in G^2 can be combined into one valuation v on [0,1]^⟕ — the twisted product of [0,1] with itself — with two components v_1 and v_2. The two logics are closely connected but do not coincide since the set of values of G^2 is not ordered linearly. Our main goal is to study different entailment relations in G_inv and G^2 that are induced by filters on [0,1] and [0,1]^⟕, respectively. In particular, we determine the exact number of such relations in both cases, establish whether any of them coincide with the entailment defined via the order on [0,1] and [0,1]^⟕, and obtain their hierarchy. We also construct reductions of filter-induced entailment relations to the ones defined via the order.

• 20.11.2024
  
  Manfred Droste (Institute of Computer Science of the University of Leipzig): Weighted Automata and Quantitative Logics

  Quantitative models and quantitative analysis in Computer Science are receiving increased attention. The goal of this talk is to investigate quantitative automata and quantitative logics. Weighted automata on finite words have already been investigated in seminal work of Schützenberger (1961). They consist of classical finite automata in which the transitions carry weights. These weights may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. This concept soon developed a flourishing theory. We investigate weighted automata and their relationship to weighted logics. For this, we present syntax and semantics of a quantitative logic; the semantics counts ‘how often’ a formula is true in a given word. Our main result, extending the classical result of Büchi, shows that if the weights are taken from an arbitrary semiring, then weighted automata and a syntactically defined fragment of our weighted logic are expressively equivalent. A corresponding result holds for infinite words. Moreover, this extends to quantitative automata investigated by Henzinger et al. with (non-semiring) average-type behaviors, or with discounting or limit average objectives for infinite words.

• 13.11.2024
  
  Raheleh Jalali (Czech Academy of Sciences, Institute of Computer Science): Admissibility of Visser's Rules in Intuitionistic Modal Logics

  We study the connection between the form of the primitive rules of a proof system and the rules the system admits. We introduce a general and syntactically defined family of sequent-style calculi over the modal language and its fragments as an approximate formalization for "constructively acceptable" systems. We call these calculi constructive and show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser’s rules. This means that there exists a polynomial-time algorithm that, given a proof of the premise of a Visser’s rule, provides a proof for its conclusion. As a positive application, we establish the feasible admissibility of Visser’s rules in several sequent calculi for intuitionistic modal logics, including CK, IK, and their extensions by the modal axioms T, B, 4, 5, and the axioms for bounded width and depth, and propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser’s rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus.

• 06.11.2024
  
  Štěpán Holub (Charles University, Faculty of Mathematics and Physics): Isabelle/HOL and Its Logic: User's Point of View

  Isabelle is a generic proof assistant that allows axiomatization of arbitrary object logic, the most widely used of which is HOL. The talk will be an introduction in Isabelle/HOL. I will briefly sketch its history and mention my motivation for using it in an ongoing project of formalization of combinatorics on words. The main part of the talk will be a live session illustrating how some design features of Isabelle/HOL are reflected in user's work. Time permitting, these will include the distinction between meta-logic and the object logic, polymorphic simple types, higher order unification, (non-existence of) proof terms, design of proof tactics, and construction of verified algorithms.

• 30.10.2024
  
  Filip Jankovec (Czech Academy of Sciences, Institute of Computer Science): About semilinear prevarieties of Abelian l-groups

  It is a well-known fact that Abelian logic has no finitary extensions (which is equivalent to the fact that the quasivariety of Abelian l-groups has no notrivial subquasivariety). In this talk we will try to axiomatize all semilinear (infinitary) extensions of Abelian logic. Alternatively, we will try to provide an axiomatization for all semilinear prevarieties of abelian l-groups. The strategy we will try to use is as follows: For a subdirectly irreducible chain C, we find a generalized quasiequation E such that for any Abelian l-group A we have: E does not hold in A if C is embeddable in A.

• 23.10.2024
  
  Daniil Kozhemiachenko (Aix-Marseille Université): Abduction in the extensions of the Belnap—Dunn logic.

  We explore the problem of explaining observations from a classically inconsistent theory by adopting a paraconsistent framework. In particular, we consider theories formulated in the languages of the Belnap—Dunn logic and its implicative expansion. The solutions are then given in one of the two further expansions of BD: BD○ that introduces formulas of the form ○ϕ (‘the information on ϕ is reliable’) and BDΔ that augments the language with Δϕ's (‘there is information that ϕ is true’). We show that explanations in BD○ and BDϕ are not reducible to one another. We analyse the complexity of standard abductive reasoning tasks (solution recognition, solution existence, and relevance / necessity of hypotheses) depending on the language of the solution and on the language of the theory. In addition, we consider the complexity of abductive reasoning in the Horn fragment of the implicative extension of BD. The talk is based on the joint work with Meghyn Bienvenu and Katsumi Inoue.

• 16.10.2024
  
  Giovanni Sambin (University of Padova): Mathematics as a natural and dynamic process. Mathematical facts.

  In a dynamic vision, in which mathematics is seen as a human product, one moves from a given truth to a careful handling of acquired information. So the foundation is intuitionistic (Law of Excluded Middle is not assumed) to distinguish positive existence, predicative (Power Set Axiom is not assumed) to distinguish sets constructed from below from collections, effective (Axiom of unique Choice is not assumed) to distinguish operations with explicit instructions from functions. Adopting this minimalist foundation in practice brings out some deep underlying structures of topology, such as logical duality between closed and open, symmetry between points and observables, continuity as a commutative square, etc., that were previously hidden by too strong assumptions. Topology in the proper sense is obtained by adding a module of convergence to these basic structures. In this way, richer notions are obtained so that, for example, it can be proved that there is an embedding of the category of concrete spaces, with points, into that of positive topologies, which are pointfree. This brings to solution an issue that has been open for more than half a century, It turns out that topology plays a central role for all mathematics, since it allows one to distinguish real, or computational, aspects from ideal, or infinitary ones. Since points are usually determined by an infinite amount of information, in order to maximize the computational, or real, aspects of mathematics, pointfree topology must be developed as much as possible. Ideal aspects are introduced locally and explicitly as ideal points and spaces over a positive topology. The most important structures in mathematics, such as real numbers, Zariski topology, etc., are obtained as ideal spaces over a positive topology. A lot of future work remains: primarily, to expand the mathematics expressible in this way as much as possible and to develop a proof assistant based on the minimalist foundation.

• 09.10.2024
  
  Igor Sedlár (ICS CAS): Epistemic Probability Logics

  Epistemic logics formalise reasoning about agents' epistemic attitudes, such as knowledge and belief, towards the occurrence or non-occurrence of events. Similarly, epistemic probability logics formalise reasoning about epistemic attitudes towards the probability of events. One of the most important epistemic probability logics studied in the literature is Fagin and Halpern's PS5 (Fagin and Halpern, 1994), which extends the standard multi-agent epistemic logic S5 with probability operators expressing linear combinations of probabilities of events. In this work-in-progress talk, we outline an alternative approach to combining epistemic logics with probability, based on modal fuzzy logic. Our work aims at extending the results of a recent paper by Baldi, Cintula and Noguera (2020), who showed that there are mutual translations between the propositional fragment of PS5 and the fuzzy logic of probability introduced by Hájek et al. (2000), based on propositional Łukasiewicz logic. Our aim is to determine whether there are similar translations linking richer fragments of PS5, including modal operators, and fuzzy probability logics based on modal Łukasiewicz logic.

• 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.

• 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).