Svejdar proof method for GL logic
[]<>p <=> []<>[]<>p
Proof 1 : <>[]<>p, <>p, []-p, []-[]<>p, []<>[]<>p, []<>p |-- []<>p, -p initial sequent 2 : -[]<>p, <>[]<>p, <>p, []-p, []-[]<>p, []<>[]<>p, []<>p |-- -p by notR applied to 1 3 : []-[]<>p, []<>[]<>p, []<>p |-- []-p by necR applied to 2 4 : []<>[]<>p, []<>p |-- <>[]<>p, []-p by posR applied to 3 5 : <>p, []<>[]<>p, []<>p |-- <>[]<>p by posL applied to 4 6 : []<>p |-- []<>[]<>p by necR applied to 5 7 : |-- ([]<>p => []<>[]<>p) by implyR applied to 6 8 : <>[]<>p, []-[]<>p, []-p, []<>p, []<>[]<>p |-- p, -[]<>p, []-p initial sequent 9 : <>p, <>[]<>p, []-[]<>p, []-p, []<>p, []<>[]<>p |-- p, -[]<>p by posL applied to 8 10 : -p, <>p, <>[]<>p, []-[]<>p, []-p, []<>p, []<>[]<>p |-- -[]<>p by notR applied to 9 11 : []-p, []<>p, []<>[]<>p |-- []-[]<>p by necR applied to 10 12 : []<>p, []<>[]<>p |-- <>p, []-[]<>p by posR applied to 11 13 : <>[]<>p, []<>p, []<>[]<>p |-- <>p by posL applied to 12 14 : []<>[]<>p |-- []<>p by necR applied to 13 15 : |-- ([]<>[]<>p => []<>p) by implyR applied to 14 16 : |-- ([]<>p <=> []<>[]<>p) by equivR applied to 7, 15
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021