Tableaux'method for S4
<>[]<>p => []p
The formula (<>[]<>p => []p) is not valid Formula's counter-model Number of states = 4 Initial state = 1 The accessibility relation is the reflexive and transitive closure of the following relation : 1 -> 2 , 3 3 -> 4 No variable is true in state 1 No variable is true in state 2 No variable is true in state 3 The true variables in state 4 are : p
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021