Tableaux'method for S4
[]p <=> [][]p
The formula ([]p <=> [][]p) is valid Proof that its negation is unsatisfiable (1) 1: -([]p <=> [][]p) case 1 (2) 1: -([]p => [][]p) from 1 (3) 1: []p from 2 (4) 1: -[][]p from 2 (5) 1: p from 3 (6) 1: <>-[]p from 4 (7) 1 -> 2 from 6 (8) 2: -[]p from 6 (9) 2: []p from 7 and 3 (10) 2: F from 8 and 9 end case 1 case 2 (2) 1: -([][]p => []p) from 1 (3) 1: [][]p from 2 (4) 1: -[]p from 2 (5) 1: []p from 3 (6) 1: F from 4 and 5 end case 2
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021