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| basis of the method (in french) | Last Modified : 30-Apr-2011 |