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 archive can be found here.
Upcoming talks
 The seminar will resume in September 2022.
Recent talks

08.06.2022
Michal Botur (Palacký University Olomouc): Perfect pseudo MValgebra, kite, variety, representationWe study the structure of perfect residuated lattices, focussing especially on perfect pseudo MValgebras. We show that perfect pseudo MValgebras 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 MValgebras.

31.05.2022
Davide Fazio (University of Cagliari): On a logicoalgebraic approach to AGM belief contraction theoryIn 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 syntacticbased 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): Onesorted Kleene algebra with testsKleene algebra with tests, KAT, is a simple twosorted algebraic framework for verifying properties of propositional while programs. Onesorted 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 onesorted 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 onesorted 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 SearchClassical planning tasks are modeled in the Planning Domain Description Language (PDDL), a schematic language based on firstorder logic. Using a grounding process, most stateoftheart planners turn this firstorder representation into a propositional one. However, grounding may cause an exponential blowup. Therefore, investigating methods for computing plans directly on the firstorder level is essential. To build such a firstorder 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 TypesIn 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 Saturationbased ATPsApplying 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 machinelearned 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 ComplementationIn 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 FDElogicsThe logic FDE, especially in its fourvalued presentation, and sometimes referred to as the BelnapDunn 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 twovalued 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 HigherOrder Logic Programs From FailuresLearning complex programs through inductive logic programming (ILP) remains a formidable challenge. Existing higherorder 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 higherorder definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Furthermore, we provide a theoretical framework capturing the class of higherorder 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 UltraproductsA construction, called ‘prime products’ will be presented that generalizes the ultraproduct construction (which is often used to create nonstandard 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 latticesThis 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 firstorder 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 betterknown 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 proofsWhat 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 prooftheoretic 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 SchroederHeister, P. & Tranchini, L. (2017). Ekman’s Paradox. Notre Dame Journal of Formal Logic, 58(4), 567581). 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 CurryHowardcorrespondence, 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 wellknown properties thereof can provide us with directions as to why this happens in these cases but not in the cases of ‘wellbehaved’ 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 transitivityThere 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 'birelational' models, and state several results obtained in this way. (Joint work with Philippe Balbiani and Martín Diéguez)