We contrast Bonanno’s ‘Belief Revision in a Temporal Framework’ (Bonanno, 2008) with preference change and belief revision from the perspective of dynamic epistemic logic (DEL). For that, we extend the logic of communication and change of van Benthem et al. (2006b) with relational substitutions (van Benthem, 2004) for preference change, and show that this does not alter its properties. Next we move to a more constrained context where belief and knowledge can be defined from preferences (Grove, 1988; Board, 2002; Baltag and Smets, 2006, 2008b), prove completeness of a very expressive logic of belief revision, and define a mechanism for updating belief revision models using a combination of action priority update (Baltag and Smets, 2008b) and preference substitution (van Benthem, 2004). 1 Reconstructing AGM style belief revision

Philosopher: What I would like to understand better is how game theory can help us to understand rational choice, and how this is related to logic. Philosophy has a long-standing interest in rational behavior. The hallmark of rationality is always taken to be the “good reasons for acting” that rational people can give. But game theory seems more concerned with what people actually do than in the reasons they might care to give for their actions.

Philosopher: It has taken me a while but I think I now see what social software is trying to get at. Its ultimate driving force seems to be a desire to help solve social problems. For this, one should of course understand these problems and get a good grasp of their structure. So, and that’s the second element, we focus on the analysis of such social problems. Finally, the way of going about in both the analysis and the formulation of the possible solutions is to make use of formal techniques that originate from a variety of disciplines— economics, logic, computer science. And this is what gives the enterprise its cross-disciplinary flavor.

Logician: It is such a pity I had to miss Rohit’s lecture. And Rohit himself has dashed off now, to a conference in Paris. On the day before the talk, one of the NIAS fellows asked me with a worried look on his face what the word “algorithm” meant that he had seen in the lecture announcement, and could we please make sure that our guest lecturer knew that part of the audience was unfamiliar—even uncomfortable—with the jargon of computer science and logic? So we forewarned Rohit, of course. Now you all understand why I am curious how it went. Can anyone tell me?

The fundamental relations in private law are claims and duties. These legal relations can be changed by agents with the appropriate legal powers. We use propositional dynamic logic and ideas about propositional control from the agency literature to formalize these changes in legal relations. Our models are sets of states with functions specifying atomic facts, agents' abilities to change atomic facts, legal relations between agents concerning changing atomic facts and agents' powers. We present a formal language that allows us to describe models and changes of models caused by two kinds of actions: actions that change atomic facts and actions that change legal relations. Next, we present a sound and complete calculus for this language. The paper demonstrates that the perspective on actions borrowed from computer science can be used to shed interesting light on the dynamics of legal relations.

The paper gives a formal analysis of public lies, explains how public lying is related to public announcement, and describes the process of recoveries from false beliefs engendered by public lying. The framework treats two kinds of public lies: simple lying update and two-step lying, which consists of suggesting that the lie may be true followed by announcing the lie. It turns out that agents’ convictions of what is true are immune to the first kind, but can be shattered by the second kind. Next, recovery from public lying is analyzed. Public lies that are accepted by an audience cannot be undone simply by announcing their negation. The paper proposes a recovery process that works well for restoring beliefs about facts but cannot be extended to beliefs about beliefs. The formal machinery of the paper consists of KD45 models and conditional neighbourhood models, with various update procedures on them. Completeness proofs for a number of reasoning systems (converse belief logic, public lies logic, lying and recovery logic, conditional neighbourhood logic, plus its dynamic version) are included.

This paper presents a formalization of refraining from actions and a deontic logic based on a process logic. The notion of refraining is needed to handle obligated actions. To refrain to do an action is to do something else. The process logic used is a mix of dynamic logic and temporal logic: actions in it are interpreted as sets of paths and temporal formulas describe the process of performing actions. The deontic logic has a temporal propositional constant saying that a bad thing will be done in the next moment. Normative properties of actions can be defined according to what happens in the process of performing actions.

A gossip protocol is a procedure for spreading secrets among a group of agents, using a connection graph. The goal is for all agents to get to know all secrets, in which case we call the execution of the protocol successful. We consider distributed and dynamic gossip protocols. In distributed gossip, the agents themselves instead of a global scheduler determine whom to call. In dynamic gossip, not only secrets are exchanged but also telephone numbers (agent identities). This results in increased graph connectivity. We define six such distributed dynamic gossip protocols, and we characterize them in terms of the topology of the graphs on which they are successful, wherein we distinguish strong success (the protocol always terminates, possibly assuming fair scheduling) from weak success (the protocol sometimes terminates). For five of these protocols, strong success (fair) and weak success are characterized by weakly connected graphs. This result is surprising, because the protocols are fairly different. In the sixth protocol, an agent may only call another agent if it does not know the other agent’s secret. Strong success for this protocol is characterized by graphs for which the set of non-terminal nodes is strongly connected. Weak success for this protocol is characterized by weakly connected graphs satisfying further topological constraints that we define in the paper. One direction of this characterization is surprisingly harder to prove than the other results in this contribution.

A gossip protocol is a procedure for spreading secrets among a group of agents, using a connection graph. In each call between a pair of connected agents, the two agents share all the secrets they have learnt. In dynamic gossip problems, dynamic connection graphs are enabled by permitting agents to spread as well the telephone numbers of other agents they know. This paper characterizes different distributed epistemic protocols in terms of the (largest) class of graphs where each protocol is successful, i.e. where the protocol necessarily ends up with all agents knowing all secrets.

A natural way to represent beliefs and the process of updating beliefs is presented by Bayesian probability theory, where belief of an agent a in P can be interpreted as a considering that P is more probable than not P. This paper attempts to get at the core logical notion underlying this. The paper presents a sound and complete neighbourhood logic for conditional belief and knowledge, and traces the connections with probabilistic logics of belief and knowledge. The key notion in this paper is that of an agent a believing P conditionally on having information Q, where it is assumed that Q is compatible with what a knows. Conditional neighbourhood logic can be viewed as a core system for reasoning about subjective plausibility that is not yet committed to an interpretation in terms of numerical probability. Indeed, every weighted Kripke model gives rise to a conditional neighbourhood model, but not vice versa. We show that our calculus for conditional neighbourhood logic is sound but not complete for weighted Kripke models. Next, we show how to extend the calculus to get completeness for the class of weighted Kripke models. Neighbourhood models for conditional belief are closed under model restriction (public announcement update), while earlier neighbourhood models for belief as `willingness to bet' were not. Therefore the logic we present improves on earlier neighbourhood logics for belief and knowledge. We present complete calculi for public announcement and for publicly revealing the truth value of propositions using reduction axioms. The reductions show that adding these announcement operators to the language does not increase expressive power.

Rohit Parikh advocates a collaboration between logicians, philosophers, computer scientists and game theorists, in an effort to use the techniques from their fields to shed light on social phenomena, in his well known plea for social software. So far, this enterprise has largely neglected a topic of key importance: money. What is money, how is it created, how does it disappear, and how does it shape our society? The paper takes on these questions in the form of a discourse where participants from a variety of backgrounds shine their lights on them.

The paper compares two kinds of models for logics of knowledge and belief, neighbourhood models and epistemic weight models. We give sound and complete calculi for both, and we show that our calculus for neighbourhood models is sound but not complete for epistemic weight models. Epistemic weight models combine knowledge and probability by using epistemic accessibility relations and weights to define subjective probabilities. Our Probability Comparison Calculus for this class of models is a further simplification of the calculus that was presented in AIML 2014.

This lecture introduces and discusses a tiny program for epistemic model checking with S5 models in Haskell. The model update operations are public announcement and publicly observable factual change. The implementation is much more efficient than the earlier implementation of DEMO (Van Eijck 2007), but less efficient than a symbolic model checker for DEL (Lecture 3). Still, because the approach is so simple, it gives a useful idea of what goes on in model checking DEL. As examples, we implement the sum and product riddle, which is solved in a few seconds, and the parametrized muddy children problems, where the cases with up to ten children run in a matter of seconds. Next, we look at PRODEMO, a program for probabilistic epistemic model checking, and use it for solving some probabilistic epistemic model checking problems. Abstract This lecture introduces and discusses a tiny program for epistemic model checking with S5 models in Haskell. The model update operations are public announcement and publicly observable factual change. The implementation is much more efficient than the earlier implementation of DEMO (Van Eijck 2007), but less efficient than a symbolic model checker for DEL (Lecture 3). Still, because the approach is so simple, it gives a useful idea of what goes on in model checking DEL. As examples, we implement the sum and product riddle, which is solved in a few seconds, and the parametrized muddy children problems, where the cases with up to ten children run in a matter of seconds. Next, we look at PRODEMO, a program for probabilistic epistemic model checking, and use it for solving some probabilistic epistemic model checking problems. Update of the abstract: the slides give a full implementation of public announcement updates for S5 models and for S5 weight models.This lecture introduces and discusses a tiny program for epistemic model checking with S5 models in Haskell. The model update operations are public announcement and publicly observable factual change. The implementation is much more efficient than the earlier implementation of DEMO (Van Eijck 2007), but less efficient than a symbolic model checker for DEL (Lecture 3). Still, because the approach is so simple, it gives a useful idea of what goes on in model checking DEL. As examples, we implement the sum and product riddle, which is solved in a few seconds, and the parametrized muddy children problems, where the cases with up to ten children run in a matter of seconds. Next, we look at PRODEMO, a program for probabilistic epistemic model checking, and use it for solving some probabilistic epistemic model checking problems. Update of the abstract: the slides give a full implementation of public announcement updates for S5 models and for S5 weight models. Who in Modal and Epistemic Logic? Who in Modal and Epistemic Logic? Saul Kripke (born 1940) Jaakko Hintikka (1929–2015)

In this chapter, a semantic theory is taken to be a collection of rules for specifying the interpretation of a class of natural language expressions. The chapter uses Haskell as the implementation language. It demonstrates that implementing a Montague style fragment in a functional programming language with flexible types is a breeze: Montague's underlying representation language is typed lambda calculus, be it without type flexibility, so Montague's specifications of natural language fragments in PTQ Montague and UG Montague are in fact already specifications of functional programs. The chapter also explains how to implement an evaluation function. As an example of the process of implementing inference for natural language, the chapter considers the language of the Aristotelian syllogism as a tiny fragment of natural language. One of the trademarks of Montague grammar is the use of possible worlds to treat intensionality. The simplest kind of communicative action probably is question answering.

Representation of ignorance about large numbers --- agent a does not know agent b's key --- is not feasible in standard Kripke semantics. The paper introduces register models that allow for compact representation of such ignorance. This is used to design a sound an complete language for number guessing games. The probabilities generated by our semantics allow for and motivate Monte Carlo model checking for register models. We show that the approach can be extended to a real life setting, namely the analysis of cryptographic security protocols. We look at a well known security protocol for secret key distribution over an insecure network, and point out how this can be analyzed with our modified version of Kripke semantics.

Viewing the way society has defined its rules and mechanisms as “social software”, we want to understand how people behave given their understanding of the societal rules and given their wish to further their interest as they conceive it, and how social mechanisms should be designed to suit people furthering their interest as they conceive it. This chapter is written from the perspective of strategic game theory, and uses strategic game scenarios and game transformations to analyze societal mechanisms.

htmlabstractWe present a variant of Kripke models to model knowledge of large numbers, applicable to cryptographic protocols. Our Epistemic Crypto Logic is a variant of Dynamic Epistemic Logic to describe com- munication and computation in a multi-agent setting. It is interpreted on register models which eciently encode larger Kripke models. As an example we formalize the well-known Die-Hellman key exchange. The presented register models also motivate a Monte Carlo method for model checking which we compare against a standard algorithm, using the key exchange as a benchmark.