Schlagwort-Archiv: Logik

Stampproof.

Mensen namen maar gewoon aan dat de aardappel gekookt zou worden, omdat de vorige aardappel dat ook deed. Terwijl er maar één aardappel hoeft te zijn die niet wordt gekookt, en dan is de hele onderbouwing onder je stamppot weg.

De Speld: Koken op deductie: maak logisch onontkoombare gerechten!

Rest in Proof.

In 1998, a chapter on realizability by his hand came out in the Handbook of Proof Theory. Characteristically, Anne’s text had been finished a few years before, faithfully meeting his deadline, but delays by other authors kept him updating, somewhat grumblingly, with all new results in the area. What he published had to be the complete state of the art.

Johan van Benthem and Dick de Jongh: Anne Troelstra (1939-2019)

Runless.

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

Chaostabelle.

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. https://doi.org/cwhw

Schlüsselprobleme in Theorie und Praxis.

Theory

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

Ältere Beiträge «