Svejdar proof method for GL logic
[]p => [][]p
Proof 1 : p, [][]p, []p |-- []p initial sequent 2 : []p |-- [][]p by necR applied to 1 3 : |-- ([]p => [][]p) by implyR applied to 2
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021