(ELVis v.1.0.2.0 beta)

Epistemic logic is a general name for logics each of which is a variant of modal logic and aims at formally representing one's reasoning about knowledge.

ELVis (Epistemic Logic Visualizer) includes the following three epistemic formal systems:

• Epistemic Logic (EL) / Multi-modal Logic
• Public Announcement Logic (PAL)
• Dynamic Epistemic Logic (DEL)
Each system includes GUI tools of both its sequent calculus and its semantics. Specifically, the following are implemented:
• an automated theorem prover based on a labelled sequent calculus, with
• random formula maker
• random action model maker
• a GUI Kripke/Action model editor with
• random Kripke model maker
• model checker
• frame property checker

# Browsers

ELVis is mainly tested by Chrome version 64, and this system requires a browser which supports ES6 and modern DOM API, i.e., the latest version of Chrome, Firefox, Safari and Edge are recommend.

# Local usage

If you want to use ELVis locally, clone the Github repository and use your local server as follows (npm and python commands should be usable in advance).

$git clone http://github.com/NomuraS/ELVis.git$ cd ELVis
$npm install --production$ npm start

Then browse http://localhost:8080/.

# Contact

Bug reports are welcome.

# Changelog

v.1.0.2.0 (2018-03-14)
Added: functions of "undo/redo" to the Kripke/Action model editors.
v.1.0.1.0 (2018-03-08)
Fix: some glitches.
Added: option "LaTeX output" to the sections of "Labelled Sequent Calculus".
v.1.0.0.0 (2018-03-05)
Initial release.

# References

1. S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001.
2. S. Negri and J. von Plato. Proof Analysis. Cambridge University Press, 2011.
3. S. Nomura, H. Ono, and K. Sano. A cut-free labelled sequent calculus for dynamic epistemic logic. The Proceedings of Logical Foundations in Computer Science 2016 (LFCS-2016 ), pages 283–298, 2016.
4. S. Nomura, K. Sano, and S. Tojo. Revising a sequent calculus for public announcement logic. Structural Analysis of Non-classical Logics: The Proceedings of the Second Taiwan Philosophical Logic Colloquium (TPLC-2014), pages 131– 157, 2015.
5. A. Ranta. PESCA - a proof editor for sequent calculus, 2000 (Online). http://www.cse.chalmers.se/~aarne/old/pesca/.
6. H. van Ditmarsch, W. Hoek, and B. Kooi. Dynamic Epistemic Logic. Springer Verlag Gmbh, 2008.
7. J. van Eijck. DEMO – a demo of epistemic modeling. Interactive Logic – Proceedings of the 7th Augustus de Morgan Workshop, pages 305–363, 2007.

# Introduction of EL

Epistemic Logic (EL) was developed in the late 50s and 60s, and has become the basic and origin of all other epistemic logics. This is basically the same as the (normal) modal logic S5 (KT5,KT45,KTB4) if the logic deals with the concept of knowledge (in the case of belief, it is usually based on modal logic KD45). If the logic aims at the formal representation of knowledge of not only a single agent but multi-agents, its syntax has a plural number of modalities (#a, #b, etc) corresponding to each agent's knowledge, i.e, in such a case, the logic is based on muti-modal logic S5.

# Syntax of EL

 Let Agent = { a, b, c, a0, a1, a2, ... } be a countable set of agents and Atom = { p, q, r, p0, p1, p2, ... } be a countable set of atomic formulas.

The EL-formula A is defined by BNF as follows:
A ::= p | ~ A | (A -> A) | #aA
where a ∈ Agent and p ∈ Atom.

#aA reads "agent a knows that A".

Then other logical connectives are defined in the usual way as follows:
• A & B := ~(A -> ~B)
• A v B := ~A -> B
• bot := p & ~p
• top := bot -> bot
• A <-> B := (A->B) & (B->A)
• $aA := ~#a~A. Note that ~, ->, &, v, <-> , top, bot, #a, and$a and are usually denoted by $$\neg$$, $$\to$$, $$\wedge$$, $$\vee$$, $$\leftrightarrow$$, $$\top$$, $$\bot$$, $$\Box_a$$ (or $$K_a$$), and $$\Diamond_a$$ (or $$\hat{K}_a$$) respectively.

For readability of a formula, the following notations are also usable:

• #A := #aA
• $A :=$aA
• knows(a,A) := #aA
• knows_if(a,A) := #aA v ~#aA

# Hilbert-style proof system of EL

• ##### Modal axioms

(Taut) all tautologies of propositional tautologies
(K) #(A -> B) -> (#A -> #B)
(T) #A -> A
(B) A -> #$A (D) #A ->$A
(4) #A -> ##A
(5) $A -> #$A

• ##### inference rule

(MP) From A -> B and A, infer B
(Nec) From A, infer #aA

version 1.0.0
The

version 1.0.0
The

# Introduction of PAL

Public Announcement Logic (PAL) is an epistemic logic for formally expressing changes of human knowledge. When we obtain some information through communication with others, our state of knowledge may change. For example, if ‘John does not know whether it will rain tomorrow or not’ is true and he gets information from the weather forecast which says that ‘it will not rain tomorrow,’ then the state of John’s knowledge changes, so ‘John knows that it will not rain tomorrow’ becomes true.

While a Kripke model of the standard epistemic logic stands for the state of knowledge, the standard epistemic logic does not have any syntax for properly expressing changes of the state of knowledge. PAL was introduced for the purpose of dealing with the flexibility of human knowledge, and the change of knowledge formally realized by the announcement operator [A] which can restrict possible worlds of Kripke semantics.

# Syntax of PAL

 Let Agent = { a, b, c, a0, a1, a2, ... } be a countable set of agents and Atom = { p, q, r, p0, p1, p2, ... } be a countable set of atomic formulas.

The PAL-formula A is defined by BNF as follows:
A ::= p | ~ A | (A -> A) | #aA | [A]A
where a ∈ Agent and p ∈ Atom.

#aA reads "agent a knows that A",
[A]B reads "after an announcement of A, B holds".

Then other logical connectives are defined in the usual way as follows:
• A & B := ~(A -> ~B)
• A v B := ~A -> B
• bot := p & ~p
• top := bot -> bot
• A <-> B := (A->B) & (B->A)
• $aA := ~#a~A • <A>B := ~[A]~B Note that ~, ->, &, v, <-> , top, bot, #a, and$a and are usually denoted by $$\neg$$, $$\to$$, $$\wedge$$, $$\vee$$, $$\leftrightarrow$$, $$\top$$, $$\bot$$, $$\Box_a$$ (or $$K_a$$), and $$\Diamond_a$$ (or $$\hat{K}_a$$) respectively.

For readability of a formula, the following notations are also usable:

• #A := #aA
• $A :=$aA
• knows(a,A) := #aA
• knows_if(a,A) := #aA v ~#aA

# Hilbert-style proof system of PAL

• ##### Modal axioms

(Taut) all tautologies of propositional tautologies
(K) #a(A -> B) -> (#aA -> #aB)

• ##### Reduction axioms of PAL

(RA1) [A]q <-> (A->q)
(RA2) [A](B->C) <-> ([A]B->[A]C)
(RA3) [A]~B <-> (A->~[A]B)
(RA4) [A]#aB <-> (A->#a[A]B)
(RA5) [A][B]C <-> [A&[A]B]C

• ##### inference rule

(MP) From A -> B and A, infer B
(Nec) From A, infer #aA

not used

version 1.0.0
The

# Introduction of DEL

Dynamic Epistemic Logic (DEL) is an advanced variation of PAL; as the name PAL shows, it deals mainly with ‘public announcements,’ by which every agent shares the same information; however, the state of knowledge may be changed not only by public announcements but also announcements to a specific group in a community.

A typical example is ‘private announcements,’ in which someone communicates something to only a single person (e.g., a personal letter). An extension of PAL, DEL is a logic which can express not only public announcements, but more delicate and complicated flows of information such as private announcement, and such a factor that causes a change of knowledge state is called an action (or event) as a whole.

Technically, the notion of action a is defined with the action model which is almost the same as the Kripke model with a finite domain. Interestingly or oddly, an action model differs from a Kripke model and belongs to the syntax field of DEL.

# Syntax of DEL

 Let Agent := { a, b, c, a0, a1, a2, ... } be a countable set of agents, Atom := { p, q, r, p0, p1, p2, ... } be a countable set of atomic formulas, Evt := { e0, e1, e2, ... } be a countable set of actions (or sometimes called events),

An (S5) action frame is a pair (S, ~) where S is a non-empty finite set of actions and ~ : Agent → S×S is a function which assigns an equivalence relation on S to an agent.

The DEL-formula A and action model E = (S, ~, pre) are simultaneously defined as follows (p ∈ Atom, e ∈ Evt, a ∈ Agent):
A ::= p | ~A | (A -> A) | #aA | [(E,e)]A
where (S, ~) is an action frame, pre is a function which assigns a DEL-formula pre(b) to each action b ∈ S, and an expression (E,e) is called a pointed action model.

#aA reads "agent a knows that A",
[(E,e)]A reads "after an action of (E,e), formula A holds".

Let E = (S, ~, pre). Then Dom(E) := S, and Rel(E) := ~, and Pre(E) := pre.

Other logical connectives are defined in the usual way as follows:
• A & B := ~(A -> ~B)
• A v B := ~A -> B
• bot := p & ~p
• top := bot -> bot
• A <-> B := (A->B) & (B->A)
• $aA := ~#a~A • <(E,e)>A := ~[(E,e)]~A • &&(Rel(E)(a)(e,x))A) := A[x/e1] & A[x/e2] & ... & A[x/en] where {e1, e2,..., en} = { x ∈ Dom(E) | (e,x) ∈ Rel(E)(a)} and A[x/y] means "x in A is substituted by y". Note that ~, ->, &, v, <-> , top, bot, #a,$a and &&(Rel(E)(a)(e,x)) are usually denoted by $$\neg$$, $$\to$$, $$\wedge$$, $$\vee$$, $$\leftrightarrow$$, $$\top$$, $$\bot$$, $$\Box_a$$ (or $$K_a$$), $$\Diamond_a$$ (or $$\hat{K}_a$$), and $$\bigwedge\limits_{e\sim^E_ax}$$ respectively.

For readability of a formula, the following notations are also usable:

• #A := #aA
• $A :=$aA
• knows(a,A) := #aA
• knows_if(a,A) := #aA v ~#aA

# Hilbert-style proof system of DEL

• ##### Modal axioms

(Taut) all tautologies of propositional tautologies
(K) #a(A -> B) -> (#aA -> #aB)

• ##### Reduction axioms of DEL

(RA1) [(E,e)]q <-> (Pre(E)(e)->q)
(RA2) [(E,e)](B->C) <-> ([(E,e)]B-> [(E,e)]C)
(RA3) [(E,e)]~A <-> (Pre(E)(e) -> ~[(E,e)]A)
(RA4) [(E,e)]#aA <-> (Pre(E)(e) -> &&(Rel(E)(a)(e,x))#a[(E,x)]A)
(RA5) [(E1,e1)][(E2,e2)]A <-> [(E1,e1);(E2,e2)]A

• ##### inference rule

(MP) From A -> B and A, infer B
(Nec) From A, infer #aA

undo
redo
 Reflexive Symmetric Transitive Eucleadian Serial
State
 label
State
 label
undo
redo
 Reflexive Symmetric Transitive Eucleadian Serial
State
 label
State
 label