Seminar Announcement
Talk by : On Many-Valued Coalgebraic Modal Logic
@ Seminar on Applied Mathematical Logic07.12.2022 16:00
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.
Talk by : S4 Necessity and Comonads
@ Seminar on Applied Mathematical Logic30.11.2022 16:00
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).
Talk by : Beyond Parry: Applications of Intensional Subject-Matter
@ Seminar on Applied Mathematical Logic23.11.2022 16:00
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.
Talk by : The Bi-Intuitionistic Logic of Co-Trees
@ Seminar on Applied Mathematical Logic09.11.2022 16:00
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.
Talk by : Crisp bi-Gödel modal logic and its paraconsistent expansion
@ Seminar on Applied Mathematical Logic02.11.2022 16:00
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.
Talk by : A module-theoretic approach to multiset consequence relations
@ Seminar on Applied Mathematical Logic19.10.2022 16:00
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.)
Talk by : On the Complexity of *-Continuous Kleene Algebra With Domain
@ Seminar on Applied Mathematical Logic05.10.2022 16:00
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.
Talk by : Perfect pseudo MV-algebra, kite, variety, representation
@ Seminar on Applied Mathematical Logic08.06.2022 16:00
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.
Talk by : On a logico-algebraic approach to AGM belief contraction theory
@ Seminar on Applied Mathematical Logic31.05.2022 16:00
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.
Talk by : One-sorted Kleene algebra with tests
@ Seminar on Applied Mathematical Logic18.05.2022 16:00
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.
Talk by : Homomorphisms of Planning Tasks and Heuristic Search
@ Seminar on Applied Mathematical Logic27.04.2022 16:00
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.
Talk by : Layers of Propositional Types
@ Seminar on Applied Mathematical Logic13.04.2022 16:00
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.
Talk by : Layers of Propositional Types
@ Seminar on Applied Mathematical Logic13.04.2022 16:00
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.
Talk by : Integrating Machine Learning into Saturation-based ATPs
@ Seminar on Applied Mathematical Logic02.03.2022 16:00
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.
Talk by : Kapsner Complementation
@ Seminar on Applied Mathematical Logic23.02.2022 16:00
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.
Talk by : Conditional FDE-logics
@ Seminar on Applied Mathematical Logic02.02.2022 16:00
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.
Talk by : Learning Higher-Order Logic Programs From Failures
@ Seminar on Applied Mathematical Logic19.01.2022 16:00
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.)