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