Schlagwort-Archiv: Logik


A proof assistant is what happens if you spend all your time developing a type checker for your language and forget that programs also need to be run.

Vladislav Zavialov: Why Dependent Haskell is the Future of Software Development


Philosophischer Literatur-Schock des Tages: Ludwig hat nicht nur die Wahrheitstabelle erfunden, sonder auch gleich die "Verwirre deine LeserInnen indem du die Zeilen möglichst kreativ sortierst." Tradition begonnen.

Gossiping Cats.

Many common decision problems about gossip graphs can be reduced to checks of NetKAT equivalences.

Malvin Gattinger & Jana Wagemaker: Towards an Analysis of Dynamic Gossip in Netkat. RAMiCS 2018.

Schlüsselprobleme in Theorie und Praxis.


Consider the following example scenario. Bob would like to borrow the apartment of his friend Anne while she is away on vacation. Anne would be very happy to do him this favor. So they now have the joint goal of making sure that Bob can enter the apartment when he arrives. Anne will think about how to achieve the goal, and might come up with the following plan: Anne puts the key under the door mat; when Bob arrives, Bob takes the key from under the door mat; Bob opens the door with the key. Note that the plan does not only contain the actions required by Anne herself, but also the actions of Bob. These are the kind of multi-agent plans that this paper is about.
However, the plan just presented does not count as an implicitly coordinated plan. When Bob arrives at the apartment, he will clearly not know that the key is under the door mat, unless Anne has told him, and this announcement was not part of the plan just presented.

Thorsten Engesser, Thomas Bolander, Robert Mattmüller & Bernhard Nebel: Cooperative Epistemic Multi-Agent Planning for Implicit Coordination. arXiv:1703.02196 In Proceedings of the Ninth Workshop on Methods for Modalities, 2017.


Real Life

M and E would like to borrow the apartment of their friend P while they are on vacation. P has given a key to another friend S. Unfortunately, S does not remember where the key is and what it looks like. Slight confusion becomes common knowledge and coming up with a plan involves many emails and phone calls. Surprisingly, it all works out, even though only two of the involved agents know Kripke models and product updates.

Es sei denn, einer stellt dumme Fragen.

Das Rätsel will ich lösen!
Logik, Logik, zur Wahrheit führt nur Logik!

Abronsius, in Tanz der Vampire: Wahrheit

Institute for Laughter, Luxury and Community.

It's a privilege and pleasure to be here.

Nutural Transformation.

What does a category theorist call a coconut?

Philip Wadler

Ältere Beiträge «