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