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 : F
e : A => B  e : --A  e : -B
-------------------------
e : F
e : -(A.B)  e : --A  e : --B
-------------------------
e : F
e : -(A <=> B)  e : --(A => B)  e : --(B => A)
-------------------------------------
e : F
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| basis of the method (in french) Last Modified : 17-Dec-2021