Svejdar proof method for GL logic
[][]p => []p
The formula is false in state 1 of the model below : the accessiblity relation is the transitive closure of the following relation : 1 -> 2 No variables is true in the state 1 No variables is true in the state 2
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021