GroLog Seminar

Logic seminar of the University of Groningen

On this page you can find a list of previous GroLog talks and events.

Mina Young Pedersen - 28 September 2023

SPEAKER: Mina Young Pedersen (University of Bergen)

DATE: Thursday 28 September 2023

TIME: 16:00-17:00

PLACE: Linnaeusborg, Room 5173.0151

TITLE: Logics of malicious and anomalous behavior in social networks

ABSTRACT:  This talk concerns agents in multi-agent systems who act out of the ordinary and/or maliciously for their own gain. Analyzing these types of agents can not only give us valuable information about agents’ potential power to disrupt, but also about the safety of systems in which they act. Specifically, I will talk about using modal logics for social networks to reason about malicious and anomalous behavior. Two examples of such studies will be given. In one, we look at a social network where agents can post and share information—and show how an agent within the system can take advantage of the network construction to post an unpopular opinion that may reach many agents. In the other example, we use temporal logic to follow a social network as it evolves through time. We show how one can use model checking to detect a particular type of agent, namely the social bot. For both systems we also cover some results for completeness, expressivity and model checking complexity. The talk is based on joint work with Rustam Galimullin, Marija Slavkovik and Sonja Smets.

 


AmirHossein Akbar Tabatabai - 1 June 2023 - A Provability Interpretation for some Propositional and Modal Logics

SPEAKER: AmirHossein Akbar Tabatabai (University of Groningen)

DATE: Thu 1 June 2023

TIME: 16:00-17:00

PLACE: Room 293 in the BernoulliBorg building (Room 5161.0293)

TITLE: A Provability Interpretation for some Propositional and Modal Logics

ABSTRACT:  In 1933, to establish a formalization for the BHK interpretation, Gödel introduced a provability interpretation for the intuitionistic propositional logic, IPC, reading the intuitionistic constructions as the usual classical proofs. Instead of using any concrete notion of a proof, he used the modal system S4 as a formalization for the intuitive concept of provability and then translated IPC into S4 in a sound and complete manner. This translation then reduced the formalization of the BHK interpretation to finding a concrete provability interpretation for the modal logic S4. 

In this talk, we will develop a framework for such provability interpretations. We will first generalize Solovay's seminal provability interpretation of the modal logic GL to capture other modal logics such as K4, KD4 and S4. The main idea is introducing a hierarchy of arithmetical theories to represent the informal hierarchy of meta-theories of the discourse and then interpreting the nested modalities in the language as the provability predicates of the different layers of this hierarchy. Later, we will combine this provability interpretation with Gödel's translation to propose a classical formalization for the BHK interpretation. The formalization suggests that the BHK interpretation is nothing but a plural name for different provability interpretations for different propositional logics based on different ontological commitments that we believe in. They include intuitionistic logic, minimal logic and some extensions of Visser-Ruitenburg's basic logic. Finally, as a negative result, we will first show that there is no provability interpretation for any extension of the logic KD45, and as expected, there is no BHK interpretation for the classical propositional logic.




Jan Rooduijn - 4 May 2023 - Focus-Style Proofs for the Two-Way Alternation-Free Modal Mu-Calculus

SPEAKER: Jan Rooduijn (University of Amsterdam)

DATE: Thu 4 May 2023

TIME: 13:30-14:30

PLACE: Room 165 in the BernoulliBorg building (Room 5161.0165)

TITLE: Focus-Style Proofs for the Two-Way Alternation-Free Modal Mu-Calculus

ABSTRACT:  We introduce a cyclic proof system for the two-way alternation-free modal μ-calculus. The system manipulates one-sided Gentzen sequents and locally deals with the backwards modalities by allowing analytic applications of the cut rule. The global effect of backwards modalities on traces is handled by making the semantics relative to a specific positional strategy of the opponent in the evaluation game. This allows us to augment sequents by so-called trace atoms, describing traces that the proponent can construct against the opponent’s strategy. The idea for trace atoms comes from Vardi’s reduction of alternating two-way automata to deterministic one-way automata. Using the multi-focus annotations introduced earlier by Marti and Venema, we turn this trace-based system into a path-based system. We prove that our system is sound for all sequents and complete for sequents not containing trace atoms. This is joint work with Yde Venema.





Rineke Verbrugge - 13 Apr 2023 -Zero-One laws for provability logic (and other modal logics)

SPEAKER: Rineke Verbrugge (University of Groningen)

DATE: Thu 13 April 2023

TIME: 16:00-17:00

PLACE: Room 222 in the BernoulliBorg building (Room 5161.0222)

TITLE: Zero-one laws for provability logic (and other modal logics)

ABSTRACT:  It has been shown in the late 1960s that each formula of first-order logic without constants and function symbols obeys a zero-one law: As the number of elements of finite models increases, every formula holds either in almost all or in almost no models of that size. Therefore, many properties of models, such as having an even number of elements, cannot be expressed in the language of first-order logic. For modal logics, limit behavior for models and frames may differ. In 1994, Halpern and Kapron proved zero-one laws for classes of models corresponding to the modal logics K, T, S4, and S5. They also proposed zero-one laws for the corresponding classes of frames, but their zero-one law for K-frames has since been disproved.

In this talk, we first give a short introduction to propositional provability logic and to validity in frames (structures) and validity in models (structures with valuations). Subsequently, we prove zero-one laws for provability logic with respect to both model and frame validity. Moreover, we axiomatize validity in almost all irreflexive transitive finite models and in almost all irreflexive transitive finite frames, leading to two different axiom systems. In the proofs, we use a combinatorial result by Kleitman and Rothschild about the structure of almost all finite partial orders. The countably infinite random Kleitman-Rothschild frame will play an important role in the proof of the zero-one law for frames. On the way, we also show that a previous result by Halpern and Kapron about the axiomatization of almost sure frame validity for S4 is not correct.

Drinks & Dinner:

After the seminar there will be drinks and dinner at Osteria Da Vinci (https://osteriadavinci.nl/) . If you would like to join, please let us know as soon as possible and before Wed 12 Apr, 14:00, by filling in this form. As usual, the first round of drinks is on us!


Dominik Klein - 9 Mar 2023 - Probabilities with Gaps and gluts

SPEAKER: Dominik Klein (Utrecht University)

DATE: Thu 9 March 2023

TIME: 16:00-17:00

PLACE: Oude Boteringestraat 52, room Gamma

TITLE: Probabilities with Gaps and Gluts

ABSTRACT: Belnap-Dunn logic (BD), sometimes also known as First Degree Entailment, is a four-valued propositional logic that complements the classical truth values of True and False with two non-classical truth values Neither and Both. The latter two are to account for the possibility of the available information being incomplete or providing contradictory evidence. In this talk, I present a probabilistic extension of BD that permits agents to have probabilistic beliefs about the truth and falsity of a proposition. we provide a sound and complete axiomatization for the framework defined and also identify policies for conditionalization and aggregation. Concretely, we  introduce four-valued equivalents of Bayes’ and Jeffrey updating and also suggest mechanisms for aggregating information from different sources. Finally, we will discuss various types of Dutch-Book like rationality constraints on four valued probabilities. This talk is based on joint work with Soroush Rafiee Rad and Ondrej Majer.

Annual VVL SEMINAR and Master thesis awards 2022 - 8 DEC 2022

The Dutch Association for Logic and Philosophy of the Exact Sciences (VvL) will hold an annual in-person joint seminar organized by the University of Groningen. The event is inspired by the departmental logic seminars that are organized at universities in the Netherlands, and aims to bring together Dutch logicians in a collaborative seminar. The event will also host the award ceremony of the VvL Master Thesis Prize, where the winners will give a short presentation of their thesis.

REGISTRATION: There is no cost for attending the seminar, but to help with the organization, please register your attendance, and indicate if you would like to join the drinks and dinner by filling in this form. If you plan to join drinks and dinner, then please register before the end of Monday 5 Dec 2022. For more information on drinks and dinner, please see below.

DATE: Thursday 8 December 2022

TIME: 15:00-17:30

PLACE: Jantina Tammeszaal, 4th floor of the University Library in the centre, Broerstraat 4, 9712 CP Groningen. Access: RUG-employees/students can enter the building using their RUG-card. For other participants there will be someone at the entrance who will make sure you can enter. 

TITLE: The Annual VvL Seminar and Master Thesis Awards 2022

TALKS: 


[1] A. Baltag and S. Smets, Learning what others know, in L. Kovacs and E. Albert (eds.), LPAR23 proceedings of the International Conference on Logic for Programming, AI and Reasoning, EPiC Series in Computing, 73:90-110, 2020. https://doi.org/10.29007/plm4

PROGRAM

15:00-15:10: Opening & Welcome

15:10-16:00: VvL lecture: Sonja Smets (ILLC, University of Amsterdam)

16:00-16:15: Coffee break 

16:15:-16:25: Words from VvL Master Thesis Awards committee 

16:25-17:25: Master Thesis Prize presentations:

16:25-16:45: Anna Dmitrieva

16:45-17:05: Maximilian Siemers

17:05-17:25: Dominik Wehr 

17:25-17:30: Closing & transfer to drinks location

17:30-18:30: Drinks at Brasserie Groen (see below)

18:30-20:15 (ca.): Dinner at Brasserie Groen (see below)


The drinks and dinner will take place at Brasserie Groen (Carolieweg 16-1, 9711 LS Groningen, 8 min walk from the venue, 12 min walk from the train station). The dinner will consist of a 2-course menu (main+dessert) for 32.50 euro per person, excluding drinks. For the main course, there will be a choice of meat (beef), fish or vegetarian (mushroom risotto). The dessert is a grand dessert (composed of samples from their dessert menu). The restaurant has confirmed that the 2-course dinner can be completed in the given time, and that participants can pay separately.


ORGANISATION:

Zoé Christoff, z.l.christoff@rug.nl

Helle Hvid Hansen, h.h.hansen@rug.nl

Barteld Kooi, b.p.kooi@rug.nl



 

Sabine Frittella - 15 Nov 2022- Non-standard probabilities and belief functions over Belnap Dunn logic


SPEAKER: Sabine Frittella (INSA Centre Val de Loire)

DATE: Tuesday, 15 November 2022

TIME: 16:00-17:00

PLACE: Room 289 in the BernoulliBorg building (Room 5161.0289)

TITLE: Non-standard probabilities and belief functions over Belnap Dunn logic

ABSTRACT: Belnap Dunn logic is a four-valued logic introduced in order to reason with incomplete and/or inconsistent information. It relies on the idea that pieces of evidence supporting a statement and its negation can be independent. Non-standard probabilities were proposed in [1] to generalize the notion of probabilities over formulas of Belnap Dunn logic. In [2], we continue this line of research and study the implications of using mass functions, belief functions and plausibility functions to formalize reasoning with incomplete/contradictory evidence within the framework of Belnap Dunn logic.

[1] D. Klein, O. Majer, and S. Rafiee Rad. Probabilities with gaps and gluts. Journal of Philosophical Logic, 50(5):1107–1141, October 2021

[2] M. Bílková, S. Frittella, D. Kozhemiachenko, O. Majer, and S. Nazari. Reasoning with belief functions over Belnap--Dunn logic. preprint. 2022. ArXiv:2203.01060

Dan Frumin - 13 Oct 2022 - semantic cut-elimination for the logic of bunched implications

SPEAKER: Dan Frumin (University of Groningen)

DATE: Thursday, 13 October 2022

TIME: 16:00-17:00

PLACE: Room 50 in the LinneausBorg building (Room 5173.0050)

TITLE: Semantic Cut-Elimination for the Logic of Bunched Implications 

ABSTRACT: The logic of bunched implications (BI) is a substructural logic that forms the backbone of separation logic, the much studied logic for reasoning about heap-manipulating programs. Although the proof theory and metatheory of BI are mathematically involved, the formalization of important metatheoretical results is still incipient. In this talk, we present a self-contained formalized, in the Coq proof assistant, proof of a central metatheoretical property of BI: cut-elimination for its sequent calculus. 

The presented proof is *semantic*, in the sense that it is obtained by interpreting sequents in a particular "universal" model. This results in a more modular and elegant proof than a standard Gentzen-style cut-elimination argument, which can be subtle and error-prone in manual proofs for BI. In particular, our semantic approach avoids unnecessary inversions on proof derivations, or the uses of cut-reductions and the multi-cut rule.     

Chiara lisciandra - 30 jun 2022 (online) 

SPEAKER: Chiara Lisciandra (University of Munich)

DATE: Thursday, 30 June 2022

TIME: 16:00-17:00

PLACE: ONLINE (Zoom link sent via mailing list)

TITLE: Norms2: Norms About Norms

ABSTRACT: In this paper, I outline and defend the view that variations in compliance levels with one and the same norm represent different norms about following norms. In support of this claim, I first argue that classic game-theoretic accounts, which define norms as Nash equilibria of noncooperative games, typically consider variations in compliance levels as separate norms. After that, I suggest a more fine-grained, game-theoretic distinction that accounts for degrees of compliance with the same norm and I show how to incorporate such an account into a psychological framework. Finally, the paper examines what given degrees of compliance can reveal about the dynamics underlying the process of norm change. I will argue that they are indicators of different reactions to the introduction of new norms.

Cancelled Rineke Verbrugge - 8 Jun 2022 (hybrid) - Hosted by the Probability and Statistics seminar

SPEAKER: Rineke Verbrugge (University of Groningen)

DATE: Wednesday, 8 June 2022

TIME: 16:00-17:00

PLACE: Hybrid: BernoulliBorg room 293 and Zoom (link sent via mailing list)

TITLE: Zero-one laws for provability logic (and other modal logics)

ABSTRACT: It has been shown in the late 1960s that each formula of first-order logic without constants and function symbols obeys a zero-one law: As the number of elements of finite models increases, every formula holds either in almost all or in almost no models of that size. Therefore, many properties of models, such as having an even number of elements, cannot be expressed in the language of first-order logic.  For modal logics, limit behavior for models and frames may differ. In 1994, Halpern and Kapron proved zero-one laws for classes of models corresponding to the modal logics K, T, S4, and S5. They also proposed zero-one laws for the corresponding classes of frames, but their zero-one law for K-frames has since been disproved.

In this talk, we first give a short introduction to propositional provability logic and to validity in frames (structures) and validity in models (structures with valuations). Subsequently, we prove zero-one laws for provability logic with respect to both model and frame validity. Moreover, we axiomatize validity in almost all irreflexive transitive finite models and in almost all irreflexive transitive finite frames, leading to two different axiom systems. In the proofs, we use a combinatorial result by Kleitman and Rothschild about the structure of almost all finite partial orders. The countably infinite random Kleitman-Rothschild frame will play an important role in the proof of the zero-one law for frames. On the way, we also show that a previous result by Halpern and Kapron about the axiomatization of almost sure frame validity for S4 is not correct.

Joost J. Joosten - 18 May 2022 (Joint session with AI Colloquium) - Model checking and formally verified software for temporal quantitative regulations

SPEAKER: Joost J. Joosten (University of Barcelona)

DATE: Wednesday, 18 May 2022

TIME: 16:00-17:00

PLACE: Room Omega at the Faculty of Philosophy (Building 1131, Oude Boteringestraat 52, 9712 GL Groningen) 

TITLE: Model checking and formally verified software for temporal quantitative regulations

ABSTRACT: In this talk, I will first expose the general activities of our research group within the covenant of the University of Barcelona, Formal Vindications S.L. and Guretruck S.L. We will speak on the European Regulation 561 for transport and then generalise the setting to temporal quantitative regulations in general. The challenge here is to find the right balance between expressibility on the one hand and feasible model checking problems on the other hand. In joint work with Moritz Müller we present a particular class of stopwatch automata that in a well-defined sense proposes such a balance. In particular, we expose an automaton for the above mentioned Regulation 561. We will see how work with proof assistants can be combined with model checking to strive for ultimate security in programming certain computable laws. Throughout the talk we shall recurrently dwell on impact of legal software on society.

Some preliminary results can be found on: http://formalvindications.com/work/


BALDER TEN CATE - 24 Mar 2022 (IN PERSON) - Exact learnability for formulas in fragments of first-order logic

SPEAKER: Balder ten Cate (University of Amsterdam)

DATE: Thursday, 24 March 2022

TIME: 17:00-18:00

PLACE: Zernike Campus, Bernoulliborg, Room 5161.0293

TITLE: Exact learnability for formulas in fragments of first-order logic

ABSTRACT: Computational learning theory studies the algorithmic aspects of learning concepts from examples. In particular, Dana Angluin's "exact learnability" model (which dates back to the 1980s) formalizes learnability in an interactive setting, where the learner may ask questions, and is required to identify the target concept with certainty after finitely many (preferably, polynomially many) questions, very much like in the children's game "mastermind" that many of us grew up with, or the "wordle" game that is currently wildly popular online.

In order for a concept class to be exactly learnable in the above sense, it must of course be the case that every concept in the class is uniquely characterizable by some finite set of examples. Because, otherwise, there would be no way to guarantee that the learner will be able to identify the target concept with certainty (in finite time). Thus, exact learnability is closely linked to unique characterizability. More precisely, unique characterizability is a necessary condition for exact learnability.

In this talk, I will review some recent results about unique characterizability and exact learnability of formulas in some fragments of FO logic.

Revantha ramanayake - 9 Dec 2021 (online) - Cuts, calculi, Complexity

SPEAKER: Revantha Ramanayake (University of Groningen)

DATE: Thursday, 9 December 2021

TIME: 16:00-17:00

PLACE: Bernoulliborg, Room 5161.0165 ONLINE (the zoom link will be sent via the mailing list)

TITLE: Cuts, Calculi, Complexity

ABSTRACT: I will introduce some of the research themes underlying my work: cut-elimination, developing analytic proof calculi for non-classical logics, and using such calculi to obtain decidability and complexity for substructural logics. I will provide a high-level overview and present specific topics of particular interest to me including cut-elimination for provability logics, what to do when cut-elimination fails for your favourite logic in the sequent calculus (the conventional approach), a programme rethinking this approach (and a new paradigm called cut-reduction that extends cut-elimination), and decidability and complexity for many extensions of the commutative Full Lambek calculus with weakening/contraction.

CANCELLED: Thomas Ågotnes - 18 Nov 2021 - Somebody knows

SPEAKER: Thomas Ågotnes (University of Bergen)

DATE: Thursday, 18 November 2021

TIME: 15:15-16:45

PLACE: Linnaeusborg Building, Room 5173.0149

TITLE: Somebody Knows

ABSTRACT: Several different notions of group knowledge have been extensively studied in the epistemic and doxastic logic literature, including common knowledge, general knowledge (everybody-knows) and distributed knowledge. In this talk I will study a natural notion of group knowledge between general and distributed knowledge: somebody-knows. While something is general knowledge if and only if it is known by *everyone*, this notion holds if and only if it is known by *someone*.  This is stronger than distributed knowledge, which is the knowledge that follows from the total knowledge in the group.  I introduce a modality for somebody-knows in the style of standard group knowledge modalities, and study its properties. Unlike the other mentioned group knowledge modalities, somebody-knows is not a normal modality; in particular it lacks the conjunctive closure property. I provide an equivalent neighbourhood semantics for the language with a single somebody-knows modality, together with a completeness result: the somebody-knows modalities are completely characterised by the modal logic EMN extended with a particular weak conjunctive closure axiom.  I also show that the satisfiability problem for this logic is PSPACE-complete. The neighbourhood semantics and the completeness and complexity results also carry over to logics for so-called local reasoning  (Fagin et al., 1995) with bounded ``frames of mind'', correcting an existing completeness result in the literature (Allen 2005). If there is time I will also reflect on the general idea of group belief, and the (perhaps surprising) observation that most of the time it doesn't actually exist. The talk is based on joint work with Yi N. Wang.


Jorge A. pérez - 30 Sep 2021 - The Logical Foundations of Message-Passing Concurrency


SPEAKER: Jorge A. Pérez (University of Groningen)

DATE: Thursday, 30 September 2021

TIME: 14:15-16:00

PLACE: Room 0149 in the Linneausborg building (Room 5173.0149)

TITLE: The Logical Foundations of Message-Passing Concurrency

ABSTRACT: The Curry-Howard(-de Bruijn) isomorphism is a landmark result for sequential programming languages: on the one hand, it tightly relates logical propositions and types; on the other hand, it connects logic proofs and functional programs.

A concurrent analogue of the Curry-Howard isomorphism remained elusive for many years. In 2010, Caires and Pfenning filled this gap: they defined a correspondence that relates, on the one hand, propositions in linear logic and session types for correct communications; on the other hand, it connects linear logic proofs with message-passing processes in the pi-calculus.

The significance and consequences of this Curry-Howard correspondence for concurrency are many and far-reaching. In my talk, I will first give an overview of this profound and beautiful result. Then, I will discuss a generalization of Caires and Pfenning's correspondence based on an extension of linear logic with operators of hybrid logic, which gives a logical justification to domain-aware message-passing concurrency.

Zoi Terzopoulou - 17 June 2021 - Majority Dynamics for Groups with Incomplete Preferences

SPEAKER: Zoi Terzopoulou (Amsterdam)

DATE: Thursday, 17 June 2021

TIME: 14:15-16:00

PLACE: online / zoom

ABSTRACT: Consider a group of agents that hold incomplete preferences over a set of alternatives (i.e., cannot compare some of them) and need to consensually select a winner amongst their options. A dynamic process in which the agents gradually complete their preferences by adopting the opinion of the majority may assist them in reaching the desired consensus. We explore such settings analytically and experimentally. We find that, unfortunately, majority dynamics are not always beneficial with respect to consensus, although they can often be so. We also study whether the chair of a group can manipulate the obtained consensus, by deciding the order in which the alternatives will be considered in the process—our relevant observations vary, depending on the consensus notions that are of interest.

Marta Gawek - 6 May 2021 - An Epistemic Separation Logic with Action Models

SPEAKER: Marta Gawek (LORIA Nancy)

DATE: Thursday, 6 May 2021

TIME: 14:15-16:00

PLACE: online / zoom (link will be sent via the mailing list)

TITLE: An Epistemic Separation Logic with Action Models

ABSTRACT

The aim of the talk is to investigate extensions of separation logic with epistemic and dynamic epistemic modalities. Separation logics are based on the intuitionistic logic of bunched implications (BI) or its classical counterpart Boolean BI. These logics combine additive and multiplicative connectives in the language, expressing the notions of resource composition and resource decomposition. Epistemic Separation Logic with Action Models (ESLAM) is a generalization of the Public Announcement Separation Logic (PASL) of Courtault et al. The syntax and semantics of ESLAM are presented, as well as reduction axioms for the elimination of dynamic modalities.

References: 

[1] Jean-René Courtault, Hans van Ditmarsch, and Didier Galmiche. A Public Announcement Separation Logic. Mathematical Structures in Computer Science 29(6):828–871, 2019. https://doi.org/10.1017/S0960129518000348

[2] David Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, Springer, 2002. https://doi.org/10.1007/978-94-017-0091-7

[3] Hans van Ditmarsch, Didier Galmiche, and Marta Gawek. An Epistemic Separation Logic with Action Models. Proceedings of 9th ICLA, 2021.Joint work with Hans van Ditmarsch and Didier Galmiche. https://www.isichennai.res.in/~sujata/icla2021/proceedings.pdf#page=50

Helle Hvid Hansen - 15 April 2021 -  Bisimulations for Non-Expressive Logics, Coalgebraically

SPEAKER: Helle Hvid Hansen (Groningen)

DATE: Thursday, 15 April 2021

TIME: 14:15-16:00

PLACE: online / zoom

TITLE: Bisimulations for Non-Expressive Logics, Coalgebraically

SLIDES: download PDF here 

ABSTRACT:
  A characteristic property of modal logics is that they are bisimulation invariant: If two states are bisimilar then they satisfy the same formulas. If the converse holds, then the logic is said to be expressive, and we have a generalisation of the classic Hennessy-Milner theorem. However, for some applications, modal logics that are not expressive are of independent interest. Such an example is given by contingency logic (see e.g. [2,4]). We can now turn the question of expressiveness around and ask, given a possibly non-expressive modal language, what is a suitable notion of semantic equivalence?
  This question was investigated at the abstract level of coalgebraic modal logic in [1,3]. Coalgebraic modal logic is a category-theoretical framework in which modal logics for many types of structures, including Kripke and neighbourhood frames, can be developed and studied in a unified setting. In particular, the fundamental relationship between modal logics and bisimulations can be proved at this level.
  In this talk, I will first give a brief introduction to coalgebraic modal logic, and then present the main contributions of [1] which introduces a notion of \Lambda-bisimulation, which is defined parametric in a modal logic. The main result here is a Hennessy-Milner style theorem for finite coalgebras and \Lambda-bisimulations.
  Finally, time permitting, I will briefly sketch the work from [3] which generalises the work of [1] to modal logics over a non-classical base, and coalgebras over other base categories than Set.

[1] Z. Bakhtiari and H.H. Hansen. Bisimulation for Weakly Expressive Coalgebraic Modal Logics. Proceedings of CALCO 2017.
[2] J. Fan, Y. Wang, and H. van Ditmarsch. Almost necessary. Proceedings of AiML 2014.
[3] J. de Groot, H.H. Hansen, A. Kurz. Logic-induced-bisimulations. Proceedings of AiML 2020.
[4] H. Montgomery and R. Routley. Contingency and non-contingency bases for normal modal logics. Logique et Analyse, 9:318–328, 1966.

Malvin Gattinger - 21 Jan 2021 - Protocols for Unreliable Dynamic Gossip

SPEAKERS: Malvin Gattinger (University of Groningen) 

DATE: 21 January 2021

TIME: 14:15 -16:00

PLACE: Zoom (link distributed via mailinglist)

ABSTRACT:

Gossip describes the spread of information throughout a network of agents. In Dynamic Gossip the network can grow at run-time. Most gossip protocols assume that all agents are reliable. We drop this assumption and study Dynamic Gossip with unreliable agents that "lie" about their own secret. We show that protocols from the literature no longer work with unreliable agents, in the sense that they no longer characterise the same networks. In addition, we show that unreliable agents that do not initiate communication are harder to identify than agents that do. This has paradoxical consequences for measures against unreliability, for example to combat the spread of false information in social networks. Time permitting, we will also discuss preliminary ideas for new protocols to deal with unreliable agents.

Joint work with Line van den Berg (Grenoble).

Related publication: https://doi.org/10.1007/978-3-030-65840-3_4

If you want to familiarise yourself with Dynamic Gossip before the talk, you can play with this website made by Ramon Meffert: https://ramonmeffert.github.io/tools-for-gossip/

LIRa/GroLog logic afternoon - 3 Dec 2020 - Zoé christoff & Aybüke özgün

SPEAKERS: Zoé Christoff (University of Groningen) and Aybüke Özgün (University of Amsterdam)

DATE: 3 December 2020

TIME: 15:30-18:00

PLACE: Zoom (link distributed via mailinglist)

PLAN: 

TITLES & ABSTRACTS

Zoé Christoff: Group Knowledge in Epistemic Logic with Names 

(joint work with Marta Bílková and Olivier Roy)

In many situations, we refer to a group of agents using a label, say "Trump supporters" or "trolls", without knowing exactly who the members of the group are. Sometimes, we even fail to know whether we, ourselves, are members of a given group. Yet, epistemic logic typically comes with the simplifying assumption that group membership is common knowledge among the entire population. In 1993 already, Grove and Halpern introduced a generalized epistemic logic relaxing this assumption and replacing the usual indexes to denote agents with abstract names that can have different referents, both individuals or groups, in different possible worlds. In that generalized framework, they replace the standard K_i modalities with modalities of the form S_n and E_n, for "someone with name n knows" and "everyone with name n knows", respectively. In our current work, we discuss extensions of this generalized logic with group modalities for common knowledge and distributed knowledge.  

Reference: A. J. Grove and J. Y. Halpern. Naming and Identity in Epistemic Logics Part I: The Propositional Case. Journal of Logic and Computation, 3(4):345–378, 08, 1993.

Aybüke Özgün: Uncertainty about Evidence

We develop a logical framework for reasoning about knowledge and evidence in which the agent may be uncertain about how to interpret their evidence. Rather than representing an evidential state as a fixed subset of the state space, our models allow the set of possible worlds that a piece of evidence corresponds to to vary from one possible world to another, and therefore itself be the subject of uncertainty. Such structures can be viewed as (epistemically motivated) generalizations of topological spaces. In this context, there arises a natural distinction between what is actually entailed by the evidence and what the agent knows is entailed by the evidence---with the latter, in general, being much weaker. We provide a sound and complete axiomatization of the corresponding bi-modal logic of knowledge and evidence entailment, and investigate some natural extensions of this core system, including the addition of a belief modality and its interaction with evidence interpretation and entailment, and the addition of a “knowability" modality interpreted via a (generalized) interior operator. 

This is joint work with Adam Bjorndahl.


Allard Tamminga - 22 Oct 2020 - Expressivity Results for Deontic Logics of Collective Agency

SPEAKER: Allard Tamminga (Universität Greifswald)

DATE: 22 October 2020

TIME: 15:15-17:00

PLACE: Online via Zoom (link distributed via mailinglist)

ABSTRACT:

We use a deontic logic of collective agency to study reducibility questions about collective agency and collective obligations. The logic that is at the basis of our study is a multi-modal logic in the tradition of stit ('sees to it that') logics of agency. Our full formal language has constants for collective and individual deontic admissibility, modalities for collective and individual agency, and modalities for collective and individual obligations. We classify its twenty-seven sublanguages in terms of their expressive power. This classification enables us to investigate reducibility relations between collective deontic admissibility, collective agency, and collective obligations, on the one hand, and individual deontic admissibility, individual agency, and individual obligations, on the other. (Joint work with Hein Duijf and Frederik Van De Putte)

Pietro Baroni: Modeling argumentation processes with multi-labelling systems (event Canceled)

SPEAKER: Pietro Baroni (University of Brescia, Italy)

DATE: 26 March 2020

TIME: 15:15-17:00

PLACE: Bernoulliborg, room 0293

ABSTRACT

Argumentation is a complex phenomenon which, for the purpose of formal modelling, can be understood as a process involving various phases.

Analysing the formal argumentation literature it turns out that some of these phases have somehow been the subject of more intensive investigation than others.

In particular the assessment of the final justification of statements has been often treated as a sort of simple byproduct of argument evaluation.

Towards rebalancing this situation, a generic formalism called multi-labelling systems has been proposed for modelling argumentation processes (and more generally multi-stage evaluation processes).

The talk will present the basic concepts of multi-labelling systems and show how this formalism allows to capture different kinds of argumentation processes and to achieve desirable goals like tunability and principled comparison of statement justification and harmonization between different formalisms.

Bahareh afshari - 18 Feb 2020 - CIRCULAR PROOFS IN MODAL LOGIC

SPEAKER: Bahareh Afshari (University of Gothenburg and ILLC, University of Amsterdam)

DATE: 18 February 2020

TIME: 15:15-17:00

PLACE: Bernoulliborg, room 0267

ABSTRACT

In this talk we look at (sound) circular reasoning and how it can been formalised as proof systems in their own right. The focus will be on modal logics, ranging from GL to more expressive languages such as the modal mu-calculus. We will further discuss how circular proofs contribute to the development of the theory of fixed point modal logic and mention future avenues of research.

For a related paper, see Afshari, B., & Leigh, G. E. (2017, June). Cut-free completeness for modal mu-calculus. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (pp. 1-12). IEEE.

Downloadable from: http://www.cse.chalmers.se/~bahafs/publications/AL17.pdf

LOGIC afternoon ON PROVABILITY & DEL - 10 Dec 2019

SPEAKERS: Gerard Renardel de Lavalette (University of Groningen) and Hans van Ditmarsch (LORIA)

DATE: 10 December 2019

TIME: 15:15-17:00

PLACE: Bernoulliborg, room 0222

TITLES & ABSTRACTS

Gerard Renardel de Lavalette: The mathematics of provability

Traditionally, the notion of provability is defined in terms of derivations: sequences or tree-like structures consisting of formulae or sequents, satisfying certain conditions involving proof rules. The 'driving force' of derivations usually consists of conditional statements: implications in the object language A -> B, entailments in the metalanguage, e.g. A,B |- A&B, or proof rules involving sequents: e.g. if G |- A and G,B |- C then G, A -> B |- C.

I propose an alternative, more mathematical definition of derivability, capitalizing on the dynamic character of conditional statements. It is based on set-valued functions F : P(EXP) -> P(EXP), where EXP denotes a collection of expressions and P denotes the power set operator. The intended meaning of F is:  for every collection E of expressions, E entails every expression A in F(E). So when EXP is a collection of atomic formulae, F represents the Horn sentence

/\ {/\ E -> A |  E a subset of EXP, A in F(E) }

Working out this idea in the context of propositional Horn logic leads to a characterization of derivability: F |- G iff is contained in F*, where F* is the Kleene closure of F. It appears that the set-valued functions  with the operator .* form a weak kind of Kleene algebra.This leads to an easy proof of completeness and to several results on uniform and polynomial interpolation.

This first experiment with set-valued functions is extended to full Horn logic and its sublogics EQL (equational logic) and CEQL (conditional equational logic). This brings in substitutions: functions that map expressions to expressions by replacing variables by terms. For Horn logic we have F |- G iff G contained in (SC(F))*, where SC(F) is the substitution closure of F. For EQL and CEQL, we get F |- G iff G contained in (SC(F U EAX))* where U denotes union and EAX is the collection of equality axioms. We obtain straightforward completeness results, and a new technique leads to interpolation results for EQL en CEQL.


Hans van Ditmarsch: Dynamic epistemic logic for distributed computing - asynchrony and concurrency

We will present some recent work on asynchrony and concurrency in dynamic epistemic logics (DEL), building on foundations in distributed computing and temporal epistemic logics. Asynchrony can be modelled by reasoning over histories of actions of different length. How to do this in DEL was proposed by [Dégremont, Löwe, Witzel: TARK 2011]. By equivalence relations on protocol-generated forests along different depths of trees, they can identify action histories of different length. More or less strongly related to DEL this was also considered for: gossip protocols [Apt, Grossi, vd Hoek, TARK 2015], logic puzzles [vD, van Eijck, Wu: KR 2010], and for the immediate snapshot algorithm in distributed computing [Goubault, Ledent, Rajsbaum: GandALF 2018]. We will present the last in some detail: Kripke models and action models can be represented as simplicial complexes. Dynamic epistemic logic can then be interpreted on such complexes.

From the perspective of dynamic epistemic logic, a further departure towards distributed computing and asynchrony is to distinguish the sending and receiving of messages, such as the making versus hearing of announcements. Recent proposals are [Knight, Maubert, Schwarzentruber; MSCS 2019] and [Balbiani, vD, Fernandez Gonzalez; ArXiV 2019] (SR 2017). From the latter we will present asynchronous announcement logic. Its axiomatization resembles that of public announcement logic, and the dynamic modalities can also be eliminated. Further research is on (what is known as) concurrent common knowledge.

Finally, how do we model concurrency in DEL? Both true concurrency and intersection concurrency are conceivable. We recall some older work in the area: [vD, vd Hoek, Kooi: AAMAS 2003] and [van Eijck, Sietsma, Wang: JANCL 2011]. The Muddy Children Problem is a joy forever: the action of three muddy children not stepping forward because none of them know whether they are muddy, is always modelled as the public announcement of a conjunction with three conjuncts. Should this not be a concurrent action with three components?


Fernando Velázquez Quesada - 12 Sep 2019 - BELIEFS BASED ON EVIDENCE AND ARGUMENTATION.

SPEAKER: Fernando Velázquez Quesada (ILLC, University of Amsterdam)

DATE: 12 September 2019

TIME: 15:15-17:00

PLACE: Energy Academy building, room 0062

ABSTRACT: 

The talk, based on a series of works together with Chenwei Shi and Sonja Smets ("Argument-based Belief in Topological Structures", "Beliefs Based on Evidence and Argumentation"), presents a logical system that combines a topological extension of evidence models ("Justified Belief and the Topology of Evidence") with tools from abstract argumentation theory ("On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games"). The system uses evidence models for representing the information an agent has collected/inferred about which is the real world, and uses abstract argumentation theory for selecting the sets of evidence that defines the agent's beliefs. The talk will focus on the basic ideas of the two involved frameworks, discussing how they are combined to define two types of beliefs, and the properties of the resulting notions.

Grolog/LIRa Logic afternoon - 1 July 2019

SPEAKERS: Roberto Ciuni (Philosophy, University of Padova), Karolina Krzyzanowska (ILLC, University of Amsterdam), Louwe Kuijer (Computer Science, University of Liverpool)

DATE: Monday 1 July 2019

TIME: 14:00-17:00 (& later drinks) 

PLACE: Room Beta, Faculty of Philosophy, Oude Boteringestraat 52

TITLES & ABSTRACTS: 

Roberto Ciuni: Information-based oughts and their interaction with knowledge and belief

In this talk, I present a conditional logic that enables us to reason about information-based oughts and the role they play in decision-theoretical scenarios that crucially involve knowledge and beliefs. Unconditional oughts and beliefs turn to be special cases of their conditional counterparts. The paper proceeds as follows. After providing a bit of background and setup, I introduce the notions of an objective ought and an information-based ought, and we present a maximality-based semantics for them and the doxastic notions we deal with, in the style of Hansson, Board, van Benthem, Baltag and Smets. Finally, I present a complete axiom system for the resulting logic.

Louwe Kuije: Minimal rationality constraints for conditional obligation

A conditional obligation is of the form O(p|q), with the meaning that p is obligatory under the condition that q is true. We can give semantics to this O operator using a preference relation on states, by saying that O(p|q) holds if p is true on all the "best" q states.

But of course that does not fully determine the semantics unless we specify what we mean by a state being one of the "best". There are several options: we could say that a states is "best" if it is maximal (i.e., there is no other state that is strictly preferred) or if it is optimal (i.e., weakly preferred over all other states). Here, we take a different option and say that a state is among the "best" states if it is part of at least one so-called minimal retentive set. Defining "best" in this way leads to a weak logic for O, but we can find contexts where this weak logic is the appropriate choice.

In this talk I will (i) introduce the semantics for O based on minimal retentive sets and give an example, (ii) introduce a sound an complete axiomatization, and discuss how it differs from other axiomatizations of conditional obligations and (iii) briefly discuss the challenges encountered while defining a canonical model for this logic.

Karolina Krzyzanowska: True clauses, false connections, and the limits of pragmatic explanations

It is a common intuition that the antecedent of an indicative conditional should have something to do with its consequent, that they should be somehow connected. However, only very few theories of conditionals do justice to this intuition. In fact, many prominent accounts of indicative conditionals validate the Principle of Conjunctive Sufficiency that allows to infer a conditional from the truth of its antecedent and the consequent. Consequently, many odd conditionals whose antecedents and consequents are not connected at all are rendered true, or highly acceptable, on these accounts. Their proponents tend to dismiss the oddness of such conditionals as a pragmatic phenomenon, outside the scope of interest of a semanticist or a logician. This is not to say that no pragmatic explanations of the oddity of missing-link conditionals have been proposed. In my talk, I will discuss the most salient of these proposals and I will present empirical data that show how they all fail. 

Nina Gierasimczuk - 6 June 2019 - From grammar inference to learning action models. A case for Explainable AI.

SPEAKER: Nina Gierasimczuk (DTU, Copenhagen)

DATE: 6 June 2019

TIME: 15:15-17:00

PLACE: Room Beta, Faculty of Philosophy, Oude Boteringestraat 52

ABSTRACT: 

The endeavour of finding patterns in data spans over many different fields, from computational linguistics to self-driving cars. Machine learning is undeniably a great source of progress across the board.  In my talk I will resurrect the old way of thinking about learning, along the lines of symbolic artificial intelligence. I will report on a recent work about inferring action models from descriptions of action executions. Such a framework constitutes an informed, reliable and verifiable way of learning, in which the learner can not only classify objects correctly, but can also report on the symbolic representation she bases her conjectures on. It is nice that the ability for AI to “explain itself” in such a way is nowadays a growing demand in the community. My action models are those of Dynamic Epistemic Logic, and the methodology is automata-theoretic in spirit. 

The results on DEL action learning model are based on:

Thomas Bolander and Nina Gierasimczuk, Learning to Act: Qualitative Learning of Deterministic Action Models, Journal of Logic and Computation, Volume 28, Issue 2, 6 March 2018, Pages 337-365. 

Stefan Wintein - 2 May 2019 - Interpolating between Riddles, Tableaux and Self-Referential Truth

SPEAKER: Stefan Wintein (Rotterdam)

DATE: 2 May 2019

TIME: 15:15-17:00

PLACE: Aquarium, Faculty of Philosophy, Oude Boteringestraat 52

ABSTRACT: In "On all Strong Kleene Generalizations of Classical Logic" (Wintein 2016) I developed a uniform tableau calculus, the SK calculus, for what I call 'Strong Kleene Generalizations of Classical Logic', a class of logics including familiar ones such as LP, K3, FDE and Exactly True Logic, but also a host of unfamiliar ones. In my talk, I will explain that and how the SK calculus can be motivated from, and is related to, earlier work I did on Raymond Smullyan’s knight-knave riddles and on theories of self-referential truth. I will also explain how the calculus is used in "Interpolation for Dunn-logics and their extensions" (Wintein and Muskens 2017) to define a novel interpolation method for the logics that it characterizes. In a nutshell, I will use the SK calculus to interpolate between different lines of my research in philosophical logic.

Jacek Wawer - 4 Apr 2019 - Ockhamism without Molinism

SPEAKER: Jacek Wawer (Kraków)

DATE: 4 April 2019

TIME: 15:15-17:00

PLACE: Room Beta, Faculty of Philosophy, Oude Boteringestraat 52

ABSTRACT: According to Ockhamism some future contingents are true: a true future contingent faithfully represents what will happen in the actual future. It turns out that a simple-minded representation of Ockhamism within the branching-time framework proves to be highly problematic from the semantic perspective. As a response, many branching-time theorists turned to Molinism -- a theory that assigns truth values not only to actual future contingents, but also to counterfactual future contingents. According to Ockhamism the sentence, "The coin will land heads", uttered before the coin toss is true. According to Molinism, even if one does not toss the coin, the sentence "Had I tossed the coin, it would've landed heads" is true. I will first explain that one can address the formal problems of Ockhamism without resorting to Molinism. Then, I present a formal theory that allows for Ockhamism without Molinism. According to this theory, every future contingent is either true or false, while all the counterfactual future contingents are neither true nor false.