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: <>p from 9 (11) 2: []-[]<>p from 8 (12) 2: -[]<>p from 11 (13) 2: F from 9 and 12 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: <>-<>p from 4 (7) 1 -> 2 from 6 (8) 2: -<>p from 6 (9) 2: []<>[]<>p from 7 and 3 (10) 2: <>[]<>p from 9 (11) 2: []-p from 8 (12) 2: -p from 11 (13) 2 -> 3 from 10 (14) 3: []<>p from 10 (15) 3: []<>[]<>p from 13 and 9 (16) 3: []-p from 13 and 11 (17) 3: -p from 16 (18) 3: <>[]<>p from 15 (19) 3: <>p from 14 (20) 3 -> 4 from 19 (21) 4: p from 19 (22) 4: []-p from 20 and 16 (23) 4: []<>[]<>p from 20 and 15 (24) 4: []<>p from 20 and 14 (25) 4: <>p from 24 (26) 4: <>[]<>p from 23 (27) 4: -p from 22 (28) 4: F from 21 and 27 end case 2
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021