+ + Epistemic Logic Suite +
++
+
| + p: + | +
+
+
+
+
+ |
+
| + q: + | +
+
+
+
+
+ |
+
| + r: + | +
+
+
+
+
+ |
+
| + s: + | +
+
+
+
+
+ |
+
| + t: + | +
+
+
+
+
+ |
+
- Dynamic Epistemic Logic Playground
--
-
| p: |
-
-
- |
| q: |
-
-
- |
| r: |
-
-
- |
| s: |
-
-
- |
| t: |
-
-
- |
-
-
-
- When entering a formula:
-
-
-
- use
~Afor $\lnot{}A$
- - use
(A & B)for $(A\land{}B)$
- - use
(A | B)for $(A\lor{}B)$
- - use
(A -> B)for $(A\rightarrow{}B)$
- - use
K{a,b,c}Afor $K_{a,b,c}A$
- - use
[A]Bfor $[A]B$
-
- - use
- -
- -
- - -
Editing Instructions
--
-
- Click in the open space to add a world -
- Drag between worlds to add a transition for the current agent -
- Ctrl-drag a world to move graph layout -
- Click a world or a transition to select it -
-
- When a world is selected:
-
-
-
- R toggles reflexivity for the current agent -
- Delete removes the world -
- -
- When a transition is selected:
-
-
-
- L(eft), R(ight), B(oth) change direction -
- Delete removes the transition -
- - Copy the URL from your browser's URL bar to share your model! -
Examples
--
-
- A simple classical logic example. Does $p = q$? -
- A tautology is a formula which is true no matter what the propositional variables are set to. -
- Agent $a$ doesn't know that $p$ is true or that $p$ is false. -
- $a$ knows that $b$ knows that $p$ is true. -
- Announcing the formula $p \land \lnot K_b p$ makes it false! (strange) -
What is (Epistemic) Logic?
- Epistemic Logic is way of formally reasoning about knowledge. - In order to understand how Epistemic logic works, let's start with classical logic and build - up from there. -Classical Logic and Formulas
-- In classical logic we start with propositional variables, our propositional - variables are $p$, $q$, $r$, $s$, and $t$. Each propositional variable can either be - true or false. For example we can say $p$ is false, written as $\lnot p$, and let's say - $q$ is true, written just as $q$. -
- -- Alongside propositional variables, we have the classical logical connectives: -
-
-
- $\lnot A$ (not) which is true when $A$ is false, -
- $A \land B$ (and) which is true when both $A$ and $B$ are true, -
- $A \lor B$ (or) which is true when $A$ is true, or $B$ is true, or both are true, -
- and $A \rightarrow B$ (conditional) which is true if $B$ is true whenever $A$ is true. -
(p <-> q) in the playground.
- Worlds, Agents, and Epistemic Logic
-- Epistemic Logic is designed for reasoning about the knowledge of someone (we call that someone an agent). - We might imagine that an agent does not know whether they are in a situation where - $p$ is true, or a situation where $p$ is not true, i.e. $\lnot p$. - We express situations as worlds. - We express an agent's knowledge by drawing relations (arrows) between worlds. These worlds - and agent relations together are called a model. -
-- Here's an example model for when an agent $a$ doesn't know if they are in - a situation where $p$, or a situation where $\lnot p$: - -
-- When you enter a classical formula into the playground, the formula is evaluated at each world as if that - world was just a classical logic by itself. Epistemic logic introduces a new logical connective which takes advantage of agents' relations - between worlds: -
-
-
- $K_b A$ (knowledge of an agent $b$) which is true at a world when $A$ is true at all worlds connected to that - world by $b$ arrows. -
- along with $K_{a,b,c} A$ which is shorthand for $K_a A\land K_b A\land K_c A$. -
- If you add more than one agent you can reason about one agent's knowledge of - another agent's knowledge e.g. $K_a K_b p$, $a$ knows that $b$ knows that $p$ is true. -
-- Finally, for the sake of representing knowledge, in Epistemic logic it is expected that all agent's relations between worlds are - equivalence relations, i.e. each agent's relation is: -
-
-
- reflexive, so each world is related to itself; -
- symmetric, if a world $0$ is related to a world $1$, then world $1$ is also related to world $0$; -
- and transitive, if a world $0$ is related to a world $1$, and world $1$ is related to world $2$ then - world $0$ has to be related to world $2$ as well. - -
Dynamic Epistemic Logic - Public Announcement
-- Dynamic Epistemic Logic introduces announcement, a mechanism for publicly announcing facts that - become the knowledge of all agents. Given a formula $A$, a public announcement removes all - worlds where $A$ is not true. -
-- Dynamic Epistemic Logic also introduces a logical connective: -
-
-
- $[A]B$ (public announcement of $A$) which is true at a world if $B$ is true after $A$ is announced, or if the world - is removed by the announcement. -
Project Information
-- This project is based on the open-source Modal Logic Playground by Ross Kirsling. - The Epistemic Logic Playground was made by Elliot Evans. - Special thanks to my non-classical logic instructors Richard Zach and Audrey Yap, as well - as my classmates Jaxson, Parker, Koray, Alejandro, and Tina who provided feedback on this project. -
-- More resources on Epistemic Logic and this project: -
- -+ + +
+ + +
+ + +
Syntax
+-
+
-
+ When entering a formula:
+
-
+
-
+ use
+
+ ~A ++ for $\lnot{}A$ +
+ -
+ use
+
+ (A & B) ++ for $(A\land{}B)$ +
+ -
+ use
+
+ (A | B) ++ for $(A\lor{}B)$ +
+ -
+ use
+
+ (A -> B) ++ for $(A\rightarrow{}B)$ +
+ -
+ use
+
+ K{a,b,c}A ++ for $K_{a,b,c}A$ +
+ -
+ use
+
+ D{a,b,c}A ++ for $D_{a,b,c}A$ +
+ -
+ use
+
+ C{a,b,c}A ++ for $C_{a,b,c}A$ +
+ -
+ use
+
+ [A]B ++ for $[A]B$ +
+
+ -
+ use
+
+ Editing Instructions +
+-
+
- + Click in the open space to + + add a world + + +
- + Drag between worlds to + + add a transition for the current agent + + +
- + Ctrl-drag a world to + + move + + graph layout + +
- + Click a world or a transition to + + select + + it + +
-
+ When a world is selected:
+
-
+
- + + R + + toggles reflexivity for the current agent + +
- + + Delete + + removes the world + +
+ -
+ When a transition is selected:
+
-
+
- + + L + + (eft), + + R + + (ight), + + B + + (oth) change direction + +
- + + Delete + + removes the transition + +
+ - + Copy the URL from your browser's URL bar to share your model! + +
About this project
++ Epistemic Model Suite is being developed by Carlos Aguilera Ventura. + The model-checking part, as well as the main interface, is a fork of the open source project + Dynamic Epistemic Logic + by Elliot Evans (which is instead based on + Modal Logic Playground, + by Ross Kirsling). +
+