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