ВУЗ: Не указан
Категория: Не указан
Дисциплина: Не указана
Добавлен: 18.10.2024
Просмотров: 13
Скачиваний: 0
ВНИМАНИЕ! Если данный файл нарушает Ваши авторские права, то обязательно сообщите нам.
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Бисимуляция
Определение (Z : M
- M
0
)
Пусть M = (W , R
4
, V )
4∈τ
и M
0
= (W
0
, R
0 4
, V
0
)
4∈τ
—
τ -модели. Непустое отношение Z ⊆ W × W
0
является бисимуляцией между M и M
0
, если выполняются условия:
1
Если Zww
0
, то в w и в w
0
истинны одни и те же переменные.
2
Если Zww
0
и R
4
wv
1
. . . v
n
, то существуют v
0 1
, . . . , v
0
n
,
такие что R
0 4
w
0
v
0 1
. . . v
0
n
и v
i
Zv
0
i
(для 1 ≤ i ≤ n).
3
Если Zww
0
и R
0 4
w
0
v
0 1
. . . v
0
n
, то существуют v
1
, . . . , v
n
, для которых R
4
wv
1
. . . v
n
и Zv
i
v
0
i
(для 1 ≤ i ≤ n).
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Бисимуляция
Бисимуляция — обобщение ограниченного морфизма.
Истинность модальных формул инвариантна относительно бисимуляции:
w
- w
0
⇒
w
! w
0
w
- w
0
— существует бисимуляция Z : M
- M
0
,
такая что Zww
0
(w ∈ M, w
0
∈ M
0
)
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Бисимуляция и логика первого порядка
Формулы логики первого порядка не инвариантны относительно бисимуляции:
0 1
2 3
4 5
e
o
p
p
p
p
∃x∃y(R(x, y) & ¬R(y, x))
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Модальная эквивалентность без бисимуляции
w
w'
M
N
w 6
- w
0
,
но
w
! w
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Теорема Хеннесси – Милнера
Определение
Модель M имеет конечный образ
, если множество
{(v
1
, . . . , v
n
) | Ruv
1
. . . v
n
}
конечно для всякого мира u и всякого отношения R из M.
Теорема
Если M и M
0
— τ -модели с конечным образом, то для любых
w ∈ M и w
0
∈ M
0
w
- w
0
⇐⇒
w
! w
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Теорема Хеннесси – Милнера
Доказательство.
⇐
Докажем, что
! — бисимуляция. Пусть w ! w
0
и Rwv,
но не существует v
0
, такого что R
0
w
0
v
0
и v
! v
0
S
0
= {u
0
| R
0
w
0
u
0
}
S
0 6= ∅ (т.к. M, w |= ♦> и w ! w
0
)
S
0
= {w
0 1
, . . . , w
0
n
} (т.к. M
0
— модель с конечным образом)
По предположению для каждого w
0
i
∈ S
0
найдется ψ
i
,
такая что M, v |= ψ
i
и M
0
, w
0
i
6|= ψ
i
M
, w |= ♦(ψ
1
& · · · & ψ
n
) и M
0
, w
0 6|= ♦(ψ
1
& · · · & ψ
n
)
w 6
! w
0
— противоречие
Обратное условие бисимуляции доказывается так же.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Теорема Хеннесси – Милнера
Доказательство.
⇐
Докажем, что
! — бисимуляция. Пусть w ! w
0
и Rwv,
но не существует v
0
, такого что R
0
w
0
v
0
и v
! v
0
S
0
= {u
0
| R
0
w
0
u
0
}
S
0 6= ∅ (т.к. M, w |= ♦> и w ! w
0
)
S
0
= {w
0 1
, . . . , w
0
n
} (т.к. M
0
— модель с конечным образом)
По предположению для каждого w
0
i
∈ S
0
найдется ψ
i
,
такая что M, v |= ψ
i
и M
0
, w
0
i
6|= ψ
i
M
, w |= ♦(ψ
1
& · · · & ψ
n
) и M
0
, w
0 6|= ♦(ψ
1
& · · · & ψ
n
)
w 6
! w
0
— противоречие
Обратное условие бисимуляции доказывается так же.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Теорема Хеннесси – Милнера
Доказательство.
⇐
Докажем, что
! — бисимуляция. Пусть w ! w
0
и Rwv,
но не существует v
0
, такого что R
0
w
0
v
0
и v
! v
0
S
0
= {u
0
| R
0
w
0
u
0
}
S
0 6= ∅ (т.к. M, w |= ♦> и w ! w
0
)
S
0
= {w
0 1
, . . . , w
0
n
} (т.к. M
0
— модель с конечным образом)
По предположению для каждого w
0
i
∈ S
0
найдется ψ
i
,
такая что M, v |= ψ
i
и M
0
, w
0
i
6|= ψ
i
M
, w |= ♦(ψ
1
& · · · & ψ
n
) и M
0
, w
0 6|= ♦(ψ
1
& · · · & ψ
n
)
w 6
! w
0
— противоречие
Обратное условие бисимуляции доказывается так же.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Теорема Хеннесси – Милнера
Доказательство.
⇐
Докажем, что
! — бисимуляция. Пусть w ! w
0
и Rwv,
но не существует v
0
, такого что R
0
w
0
v
0
и v
! v
0
S
0
= {u
0
| R
0
w
0
u
0
}
S
0 6= ∅ (т.к. M, w |= ♦> и w ! w
0
)
S
0
= {w
0 1
, . . . , w
0
n
} (т.к. M
0
— модель с конечным образом)
По предположению для каждого w
0
i
∈ S
0
найдется ψ
i
,
такая что M, v |= ψ
i
и M
0
, w
0
i
6|= ψ
i
M
, w |= ♦(ψ
1
& · · · & ψ
n
) и M
0
, w
0 6|= ♦(ψ
1
& · · · & ψ
n
)
w 6
! w
0
— противоречие
Обратное условие бисимуляции доказывается так же.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Теорема Хеннесси – Милнера
Доказательство.
⇐
Докажем, что
! — бисимуляция. Пусть w ! w
0
и Rwv,
но не существует v
0
, такого что R
0
w
0
v
0
и v
! v
0
S
0
= {u
0
| R
0
w
0
u
0
}
S
0 6= ∅ (т.к. M, w |= ♦> и w ! w
0
)
S
0
= {w
0 1
, . . . , w
0
n
} (т.к. M
0
— модель с конечным образом)
По предположению для каждого w
0
i
∈ S
0
найдется ψ
i
,
такая что M, v |= ψ
i
и M
0
, w
0
i
6|= ψ
i
M
, w |= ♦(ψ
1
& · · · & ψ
n
) и M
0
, w
0 6|= ♦(ψ
1
& · · · & ψ
n
)
w 6
! w
0
— противоречие
Обратное условие бисимуляции доказывается так же.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Теорема Хеннесси – Милнера
Доказательство.
⇐
Докажем, что
! — бисимуляция. Пусть w ! w
0
и Rwv,
но не существует v
0
, такого что R
0
w
0
v
0
и v
! v
0
S
0
= {u
0
| R
0
w
0
u
0
}
S
0 6= ∅ (т.к. M, w |= ♦> и w ! w
0
)
S
0
= {w
0 1
, . . . , w
0
n
} (т.к. M
0
— модель с конечным образом)
По предположению для каждого w
0
i
∈ S
0
найдется ψ
i
,
такая что M, v |= ψ
i
и M
0
, w
0
i
6|= ψ
i
M
, w |= ♦(ψ
1
& · · · & ψ
n
) и M
0
, w
0 6|= ♦(ψ
1
& · · · & ψ
n
)
w 6
! w
0
— противоречие
Обратное условие бисимуляции доказывается так же.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Свойство конечной модели
Определение
Модальный тип τ обладает свойством конечной модели относительно класса τ -моделей M, если всякая τ -формула φ,
выполнимая в некоторой модели из M, выполнима и в некоторой конечной модели из M.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Подформулы
Определение
Множество формул Σ
замкнуто относительно взятия подформул
, если:
φ ∨ ψ ∈ Σ
⇒ φ ∈ Σ и ψ ∈ Σ
¬φ ∈ Σ
⇒ φ ∈ Σ
4(φ
1
, . . . , φ
n
) ∈ Σ
⇒ φ
1
∈ Σ, . . . , φ
n
∈ Σ
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Фильтрация M
f
Σ
по Σ = {♦p, p}
0 4
3 1
2
p, q
p
p
p
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Фильтрация M
f
Σ
по Σ = {♦p, p}
|0|
0 4
3 1
2
p, q
p
p
p
|1|
W
f
— один мир для каждого набора значений формул из Σ
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Фильтрация M
f
Σ
по Σ = {♦p, p}
|0|
0 4
3 1
2
p, q
p
p
p
|1|
p
V
f
(p) = {|w| | M, w |= p} для всех переменных из Σ
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Фильтрация M
f
Σ
по Σ = {♦p, p}
|0|
0 4
3 1
2
p, q
p
p
p
|1|
p
Rwv ⇒ R
f
|w||v|
R
f
|w||v|, ♦φ ∈ Σ и M, v |= φ ⇒ M, w |= ♦φ
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Фильтрация M
f
Σ
по Σ = {♦p, p}
|0|
0 4
3 1
2
p, q
p
p
p
|1|
p
Фильтрация является гомоморфизмом, но не всегда является ограниченным морфизмом.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Размер фильтрации
Утверждение
Фильтрация по множеству формул Σ, замкнутому относительно взятия подформул, содержит не более 2
|Σ|
элементов.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Теорема о фильтрации для базового модального языка
Теорема
Пусть M
f
Σ
— фильтрация M по множеству формул Σ,
замкнутому относительно взятия подформул. Тогда для любых φ ∈ Σ и w ∈ M
M
, w |= φ
⇐⇒
M
f
Σ
, |w| |= φ.
Доказательство.
Индукция по φ.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Фильтрация
Свойство конечной модели
Теорема
Если формула базового модального языка φ выполнима, то она выполнима и в конечной модели, содержащей не более
2
m
возможных миров, где m — количество подформул формулы φ.
Доказательство.
Если φ выполнима в модели M, то φ выполнима в любой фильтрации M по множеству всех подформул φ.
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Упражнение
Докажите, что истинность темпоральных формул инвариантна относительно темпоральной бисимуляции.
Пусть M и M
0
— конечные корневые темпоральные модели с корнями w и w
0
. Докажите, что если в w и w
0
истинны одни и те же формулы, то существует темпоральная бисимуляция, связывающая w и w
0
Неклассические логики и представление знаний
ВШЭ
Инвариантность модальных формул
Бисимуляция
Конечные модели
Упражнения
Упражнение
Докажите, что истинность темпоральных формул инвариантна относительно темпоральной бисимуляции.
Пусть M и M
0
— конечные корневые темпоральные модели с корнями w и w
0
. Докажите, что если в w и w
0
истинны одни и те же формулы, то существует темпоральная бисимуляция, связывающая w и w
0
Неклассические логики и представление знаний
ВШЭ