S4-Tableaux'method rules

e : A.B
--------
e : A
e : A.B
--------
e : B
e : -- A
--------
e : A
e : -(A + B)
------------
e : - A
e : -(A + B)
------------
e : - B
e : -(A => B)
------------
e : A
e : -(A => B)
------------
e : -B
e : A <=> B
------------
e : A => B
e : A <=> B
------------
e : B => A
e : A + B  
-------------
e : A | e : B
e : A => B  
--------------
e : -A | e : B
e : -(A.B) 
---------------
e : -A | e : -B
e : -(A <=> B)  
--------------------------
e : -(A => B) | e:-(B => A)
e : []A
--------
e : A
e : -[]A
--------
e : <>-A
e : -<>A
--------
e : [] -A
e : []A  e -> f
---------------
f : []A
e : <>A
------------
f : A  e -> f
f new (not on the branch)

examples | rules | syntax | info | home | download Last Modified : 01-Apr-2019