Семантичні моделі та секвенційні числення транзиційних модальних логік
Досліджено чисті першопорядкові транзиційні модальні логіки часткових предикатів. Описано семантичні моделі та мови таких логік Для пропонованих логік побудовано числення секвенційного типу. Для цих числень доведено теореми коректності й повноти. Исследованы чистые первопорядковые транзиционные мода...
Saved in:
| Published in: | Компьютерная математика |
|---|---|
| Date: | 2013 |
| Main Author: | |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2013
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/84739 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Семантичні моделі та секвенційні числення транзиційних модальних логік / О.С. Шкільняк // Компьютерная математика. — 2013. — № 1. — С. 141-150. — Бібліогр.: 6 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860159726661140480 |
|---|---|
| author | Шкільняк, О.С. |
| author_facet | Шкільняк, О.С. |
| citation_txt | Семантичні моделі та секвенційні числення транзиційних модальних логік / О.С. Шкільняк // Компьютерная математика. — 2013. — № 1. — С. 141-150. — Бібліогр.: 6 назв. — укр. |
| collection | DSpace DC |
| container_title | Компьютерная математика |
| description | Досліджено чисті першопорядкові транзиційні модальні логіки часткових предикатів. Описано семантичні моделі та мови таких логік Для пропонованих логік побудовано числення секвенційного типу. Для цих числень доведено теореми коректності й повноти.
Исследованы чистые первопорядковые транзиционные модальные логики частичных предикатов. Описаны семантические модели и языки таких логик. Для предложенных логик построены исчисления секвенциального типа. Для этих исчислений доказаны теоремы корректности и полноты.
Pure first-order transitional modal logics of partial predicates are studied. For the introduced logics, we describe semantic models and languages and we construct sequent calculi. The correctness and completeness theorems are proved for such calculi.
|
| first_indexed | 2025-12-07T17:54:13Z |
| format | Article |
| fulltext |
Компьютерная математика. 2013, № 1 141
Досліджено чисті першопорядко-
ві транзиційні модальні логіки
часткових предикатів. Описано
семантичні моделі та мови таких
логік Для пропонованих логік по-
будовано числення секвенційного
типу. Для цих числень доведено
теореми коректності й повноти.
© О.C. Шкільняк, 2013
УДК 004.42:510.69
О.С. ШКІЛЬНЯК
СЕМАНТИЧНІ МОДЕЛІ
ТА СЕКВЕНЦІЙНІ ЧИСЛЕННЯ
ТРАНЗИЦІЙНИХ МОДАЛЬНИХ
ЛОГІК
Вступ. Для розв'язання широкого кола задач
інформатики й програмування з великим
успіхом використовуються [1, 2] модальні ло-
гіки. Апарат епістемічних логік успішно за-
стосовується для опису інформаційних та ек-
спертних систем, баз даних і баз знань.
Темпоральні логіки є ефективним механіз-
мом моделювання динамічних систем,
специфікації та верифікації програм. На базі
цих логік збудовано низку систем та мов
специфікації.
Традиційні модальні логіки базуються на
класичній логіці предикатів. Водночас обме-
ження класичної логіки мотивують необхід-
ність побудови нових, програмно-орієнтова-
них логічних формалізмів модального типу.
Можливості традиційних модальних логік
та композиційно-номінативних логік част-
кових квазіарних предикатів [3] синтезують
композиційно-номінативні модальні логіки
(КНМЛ). Важливим класом КНМЛ є транзи-
ційні модальні логіки (ТМЛ), вони відбива-
ють аспект зміни й розвитку предметних об-
ластей, описуючи переходи від одного стану
світу до іншого. В межах ТМЛ природним
чином можна розглядати традиційні модаль-
ні логіки – алетичні, темпоральні, епістеміч-
ні, деонтичні тощо. Підкласами ТМЛ є
мультимодальні (ММЛ) та темпоральні
(ТмМЛ) композиційно-номінативні логіки.
Окремими випадками ММЛ є епістемічні
КНМЛ та загальні ТМЛ (ЗТМЛ). Різні класи
КНМЛ досліджувались, зокрема, в роботах
[4–6].
Т.М. Провотар, К.Д. Протасова
Компьютерная математика. 2010, №
142
Дана робота присвячена
дослідженню чистих першо-
порядкових ТМЛ. Наведено основні
семантичні властивості таких логік,
О.С. ШКІЛЬНЯК
142 Компьютерная математика. 2013, № 1
зокрема, властивості відношення логічного наслідку для множин специ-
фікованих станами формул. На цій основі для ММЛ і ТмМЛ еквітонних
предикатів запропоновано числення секвенційного типу. Характерна їх
особливість – використання спрощених форм елімінації модальностей та форм
елімінації кванторів під реномінаціями. Для таких числень доведено теореми
коректності та повноти.
Поняття, які в цій статті не визначаються, тлумачимо в сенсі робіт [3, 4, 6].
Семантичні моделі транзиційних модальних логік. Центральне поняття
КНМЛ – поняття композиційно-номінативної модальної системи (КНМС).
КНМС – це об'єкт вигляду M = (Cms, Fт, Jт), де Cms – композиційна мо-
дальна система (КМС), Fm – множина формул відповідної мови КНМЛ, Jт –
відображення інтерпретації формул на станах світу.
КМС задають семантичні аспекти світу, вони є семантичними моделями
реляційного типу. КМС мають вигляд Cms = (S, R, Pr, C), де S – множина станів
світу, R – множина відношень на S вигляду ρ ⊆ S × S
n, Pr – множина предикатів
на станах світу, C – множина композицій на Pr. Така C визначається базовими
модальними композиціями та базовими загальнологічними композиціями
відповідного рівня (для чистих першопорядкових логік це ¬, ∨, R ,v
x ∃x).
Для першопорядкових КНМЛ конкретизуємо S як множину неокласичних [3]
алгебраїчних систем вигляду α = (Aα, Prα), де Prα – множина еквітонних часткових
предикатів вигляду VAα →{T, F}. Тоді
S
A Aα
α∈
= U – множина усіх базових даних
світу,
S
Pr Prα
α∈
= U – множина предикатів усіх станів світу.
Транзиційна модальна система (ТМС) – це КНМС, у якої R складається з
відношень вигляду ρ ⊆ S × S. Трактуємо ρ як відношення переходу на станах.
ТМС із базовими модальними композиціями {Кi | i∈I} та R = {>i | i∈I},
де кожному >i зіставлено Кi , назвемо мультимодальними (ММС). ТМС із
єдиною базовою модальною композицією � (необхідно), у яких R= {>}, назвемо
загальними (ЗТМС). ТМС, у яких R= {>}, а базовими модальними композиціями
є �↑ (завжди буде) та �↓ (завжди було), назвемо темпоральними (ТмМС).
Для ЗТМС та ТмМС традиційно задають [3, 4] дуальні композиції �, �↑, �↓.
Залежно від властивостей відношень переходу можна визначати різні класи
ТМС. Традиційно розглядають випадки, коли ці відношення можуть бути реф-
лексивними, симетричними чи транзитивними. Якщо в ММС всі >i рефлексив-
ні, то в назві ММС пишемо символ R; якщо всі >i транзитивні, то пишемо T;
якщо всі >i симетричні, то пишемо S. Отримуємо такі чисті типи ММС:
R-ММС, T-ММС, S-ММС, RT-ММС, RS-ММС, TS-ММС, RTS-ММС.
Аналогічно отримуємо відповідні класи ТмМС та ЗТМС:
СЕМАНТИЧНІ МОДЕЛІ ТА СЕКВЕНЦІЙНІ ЧИСЛЕННЯ ТРАНЗИЦІЙНИХ МОДАЛЬНИХ ЛОГІК
Компьютерная математика. 2013, № 1 143
R-ЗТМС, T-ЗТМС, S-ЗТМС, RT-ЗТМС, RS-ЗТМС, TS-ЗТМС, RTS-ЗТМС;
R-ТмМС, T-ТмМС, S-ТмМС, RT-ТмМС, RS-ТмМС, TS-ТмМС, RTS-ТмМС.
Водночас для ММС можливі складніші, змішані типи (наприклад, >1 симет-
ричне, >2 транзитивне й рефлексивне, >2 рефлексивне і т. д.).
ММС із скінченними множинами однотипних відношень переходу назвемо
епістемічними. Вони є семантичними моделями епістемічних КНМЛ.
Мова чистих першопорядкових ТМС. Алфавіт мови: множини V предмет-
них імен та Ps предикатних символiв (ПС); символи базових композицій ¬, ∨,
,v
xR ∃x; множина Ms символів базових модальних композицій (модальна сигна-
тура). Множина Fт формул мови визначається індуктивно:
FA) кожний p∈Ps – (атомарна) формула;
FL) нехай Φ, Ψ∈Fт; тодi ¬Φ∈Fт, ∨ΦΨ∈Fт, ( ) ,v
xR FmΦ ∈ ∃xΦ∈Fт;
FM) нехай Φ∈Fт, �∈Ms; тодi �Φ∈Fт.
У випадку ММС маємо Ms = {Кi | i∈I}, тоді п. FM набуває вигляду:
FК) нехай Φ∈Fт, Кi ∈Ms; тодi Кi Φ∈Fт.
Зокрема, у випадку ЗТМС маємо Ms = {�}, тоді п. FM набуває вигляду:
F�) нехай Φ∈Fт; тодi �Φ∈Fт.
У випадку ТмМС маємо Ms = {�↑, �↓}, п. FM набуває вигляду:
FT) нехай Φ∈Fт; тодi �↑Φ, �↓Φ ∈Fт.
Задамо відображення інтерпретації атомарних формул на станах Iт : Рs × S →Pr,
при цьому Iт(p, α) ∈ Prα . Таке Iт продовжимо до відображення інтерпретації формул
на станах Jт : Fт × S →Pr. При цьому Jт(Φ, α) ∈ Prα.
IA) Jт(p, α) = Iт(p, α) для всіх p∈Ps;
IL) Jт(¬, α) = ¬(Jт(Φ, α)); Jт(∨ΦΨ, α) = ∨(Jт(Φ, α), Jт(Ψ, α));
( , ) R ( ( , ));v v
x xJm R JmΦ α = Φ α
Jт(∃xΦ, α)(d)
, якщо ( , )( ) для деякого ,
, якщо ( , )( ) для всіх ,
невизначене в усіх інших випадках.
T Jm d x a T a A
F Jm d x a F a A
α
α
Φ α ∇ = ∈= Φ α ∇ = ∈
a
a
У випадку ММС додаємо такий пункт:
IК) Jт(Кi Φ, α)(d)
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
i
i
T Jm d T S
F S Jm d F
Φ δ = δ∈ α δ= δ∈ α δ Φ δ =
>
>
Якщо для α не існує такого β, що α >i β, то Jт(Кi Φ, α)(d)↑ для кожного
d∈VAα.
О.С. ШКІЛЬНЯК
144 Компьютерная математика. 2013, № 1
У випадку ТмМС додаємо пункт:
IT) Jт(�↑Φ, α)(d)
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках;
T Jm d T S
F S Jm d F
Φ δ = δ∈ α δ= δ∈ α δ Φ δ =
>
>
Jт(�↓Φ, α)(d)
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
T Jm d T S
F S Jm d F
Φ δ = δ∈ δ α= δ∈ δ α Φ δ =
>
>
Якщо для α не існує такого β, що α > β, то Jт(�↑Φ, α)(d)↑ для всіх d∈VAα;
якщо для α не існує такого β, що β > α, то Jт(�↓Φ, α)(d)↑ для всіх d∈VAα.
Тип ТМС визначається її модальною сигнатурою Мs, однотипністю відно-
шень із R для кожного �∈Мs та сигнатурою синтетичної неістотності [3].
Предикат Jт(Φ, α), який є значенням формули Φ у стані α, позначаємо Φα.
Φ істинна в ТМС M (позначаємо M |= Φ), якщо Φα є істинним для кожного
α∈S.
Φ усюди істинна (позначаємо |= Φ), якщо M |= Φ для всіх ТМС M одного типу.
ТМС скорочено позначаємо як (S, R, А, Jт).
Можна виділити [4] ТМС із сильною умовою визначеності на станах, назва-
ні St-ТМС, та ТМС із загальною умовою визначеності на станах, названі Gn-
ТМС. Модальні композиції St-ТМС не зберігають [4] еквітонність предикатів, що
може привести до порушення інформаційної монотонності. Водночас [4]
модальні композиції Gn-ТМС умову еквітонності зберігають.
Символи модальних композицій можна проносити через реномінації.
Теорема 1. Для довільних �∈Ms маємо | v v
x xR R= Φ ↔ Φ� � .
Взаємодія модальних композицій та кванторів складніша.
Теорема 2. |= ∃x�Φ → �∃xΦ та |= �∀xΦ →∀x�Φ для довільних �∈Ms.
Водночас [4] маємо |≠ ∀x�Φ → �∀xΦ та |≠ �∃xΦ → ∃x�Φ.
Відношення логічного наслідку для множин формул. Секвенційні чис-
лення ТМЛ будуємо на основі властивостей відношення логічного наслідку
для множин специфікованих станами формул. Такі формули мають вигляд Φα,
де Φ – формула, α – її специфікація (відмітка), яку трактуємо як ім’я стану світу.
Нехай M – ТМС із множиною станів S, Γ – множина специфікованих стана-
ми формул, в якій специфікації (імена станів) утворюють множину S.
Множина Γ узгоджена із ТМС M, якщо задана ін’єкція S у S.
Нехай ∆ та Γ – множини специфікованих станами формул.
СЕМАНТИЧНІ МОДЕЛІ ТА СЕКВЕНЦІЙНІ ЧИСЛЕННЯ ТРАНЗИЦІЙНИХ МОДАЛЬНИХ ЛОГІК
Компьютерная математика. 2013, № 1 145
∆ є логічним наслідком Γ в узгодженій із ними ТМС M (позначаємо Γ |=M ∆),
якщо для всіх d∈VA із умови Φα(dα) = T для всіх Φα∈Γ випливає: неможливо
Ψβ(dβ) = F для всіх Ψβ∈∆. Надалі запис Γ |=M ∆ матиме на увазі узгодженість M із
Γ та ∆.
∆ є логічним наслідком Γ (щодо ТМС певного типу), що позначаємо Γ |= ∆,
якщо Γ |=M ∆ для всіх ТМС M відповідного типу.
Розглянемо основні властивості відношення |=M. Немодальні властивості по-
вторюють відповідні [3] властивості логічного наслідку для множин формул
логіки еквітонних предикатів. Це наведені в [4] властивості ¬|−, ¬−|, ∨|−, ∨−|, RT|−,
RT–|, ΦN|−, RR|−, RR–|, R¬|−, R¬–|, R∨|–, R∨–|, до яких додаємо такі властивості:
С) якщо Γ∩∆ ≠ ∅, то Γ |=M ∆;
U) нехай Γ ⊆ Υ та ∆ ⊆ Σ. Тоді Γ |=M ∆ ⇒ Υ |=M Σ;
R∃R|−)
,
, ( ) ,u x
v yR x α∃ Φ Γ |=M ∆ ⇔ ( ) ,u
vR x α∃ Φ Γ |=M ∆;
R∃R−|) Γ |=M ∆, ,
, ( )u x
v yR x α∃ Φ ⇔ Γ |=M ∆, ( )u
vR x α∃ Φ ;
R�|−) Γ, ( )v
xR αΦ� |=M ∆ ⇔ Γ, ( )v
xR αΦ� |=M ∆, де �∈Ms;
R�−|) Γ |=M ∆, ( )v
xR αΦ� ⇔ Γ |=M ∆, ( )v
xR αΦ� , де �∈Ms.
Властивості, пов'язані з елімінацією кванторів:
∃R|–) ( ) ,u
vR x α∃ Φ Γ |=M ∆ ⇔ ,
, ( ) ,u x
v yR αΦ Γ |=M ∆ (тут y∈VT, y∉nm(Γ, ∆, ( ))u
vR x∃ Φ );
∃|–) ∃хΦα, Γ |=M ∆ ⇔ ( ) ,x
yR αΦ Γ |=M ∆ (тут у∈VT та у∉пт(Γ, ∆,Φ));
∃R–|) Γ |=M ∆, ,
, ( ) ,u x
v yR αΦ ( )u
vR x α∃ Φ ⇔ Γ |=M ∆, ( )u
vR x α∃ Φ ;
∃–|) Γ |=M ∆, ( ) ,x
yR αΦ ∃хΦα ⇔ Γ |=M ∆, ∃хΦα.
Розглянемо елімінацію модальностей. У випадку ММС маємо (тут Кi ∈Ms):
Кi |–) Кi Φα, Γ |=M ∆ ⇔ {Φβ | α >i β}∪Γ |=M ∆;
Кi –|) Γ |=M ∆, Кi Φα ⇔ Γ |=M ∆, Φβ для всіх станів β∈S таких, що α >i β.
У випадку ТмМС маємо:
�↑|–) �↑Φα, Γ |=M ∆ ⇔ {Φβ | α>β}∪Γ |=M ∆;
�↑–|) Γ |=M ∆, �↑Φα ⇔ Γ |=M ∆, Φβ для всіх станів β∈S таких, що α>β;
�↓|–) �↓Φα, Γ |=M ∆ ⇔ {Φβ | β>α}∪Γ |=M ∆;
�↓–|) Γ |=M ∆, �↓Φα ⇔ Γ |=M ∆, Φβ для всіх станів β∈S таких, що β>α.
Наведені властивості відношення |= індукують (окрім С і U) відповідні
секвенційні форми, а властивість С задає умову замкненості секвенції.
Базові секвенційні форми. Специфікацією стану назвемо слово вигляду α|–
чи α–|, де α – ім'я стану. Стани іменуємо натуральними числами. Початковий
стан позначаємо як 0.
О.С. ШКІЛЬНЯК
146 Компьютерная математика. 2013, № 1
Секвенції збагачуємо збудованими на даний момент виведення множинами
станів та відношень на станах. Нехай Σ – множина специфікованих формул,
α{Aα}, β{Aβ}, … – побудовані на поточний момент стани із множинами їх базо-
вих даних; M – схема моделі світу, тобто збудоване на цей момент відношення
досяжності, записане для імен станів; St – множина імен станів на даний момент.
Збагачені секвенції записуємо як Σ // α{Aα}, β{Aβ}, … // M, скорочено Σ // St // M.
Наведемо базові секвенційні форми числень чистих першопорядкових ТМЛ
еквітонних предикатів. Форми, аналогічні відповідним формам числень логіки
еквітонних квазіарних предикатів [3], не змінюють схему моделі світу:
|– ¬ |
|
, // //
, // //
A St M
A St M
α−
α −
Σ
¬ Σ
; −| ¬ |
|
, // //
, // //
A St M
A St M
α −
α−
Σ
¬ Σ
;
|−∨ | |
|
, // // , // //
, // //
A St M B St M
A B St M
α − α −
α −
Σ Σ
∨ Σ
; −|∨ | |
|
, , // //
, // //
A B St M
A B St M
α− α−
α−
Σ
∨ Σ
;
|−RT |
,
| ,
( ), // //
( ), // //
v
x
z v
z x
R A St M
R A St M
α −
α −
Σ
Σ
; −|RT |
,
| ,
( ), // //
( ), // //
v
x
z v
z x
R A St M
R A St M
α−
α−
Σ
Σ
;
|−RR |
|
( ), // //
( ( )), // //
v w
x y
v w
x y
R A St M
R R A St M
α −
α −
Σ
Σ
o
; −|RR |
|
( ), // //
( ( )), // //
v w
x y
v w
x y
R A St M
R R A St M
α−
α−
Σ
Σ
o
;
|−R¬ |-
|-
( ), // //
( ), // //
v
x
v
x
R A St M
R A St M
α
α
¬ Σ
¬ Σ
; −|R¬ |
|
( ), // //
( ), // //
v
x
v
x
R A St M
R A St M
α−
α−
¬ Σ
¬ Σ
;
−|R∨ |
|
( ) ( ), // //
( ), // //
v v
x x
v
x
R A R B St M
R A B St M
α−
α−
∨ Σ
∨ Σ
; |−R∨ |
|
( ) ( ), // //
( ), // //
v v
x x
v
x
R A R B St M
R A B St M
α −
α −
∨ Σ
∨ Σ
;
|−ΦN |
,
| ,
( ), // //
( ), // //
v
u
y v
z u
R A St M
R A St M
α −
α −
Σ
Σ
, де у∈µ(A); −|ΦN |
,
| ,
( ), // //
( ), // //
v
u
y v
z u
R A St M
R A St M
α−
α−
Σ
Σ
,
де у∈µ(A);
|−R∃R |
,
| ,
( ), // //
( ), // //
u
v
u x
v y
R xA St M
R xA St M
α −
α −
∃ Σ
∃ Σ
; −|R∃R |
,
| ,
( ), // //
( ), // //
u
v
u x
v y
R xA St M
R xA St M
α−
α−
∃ Σ
∃ Σ
;
|−R∃p |
|
, // //
( ), // //x
y
xA St M
R xA St M
α −
α −
∃ Σ
∃ Σ
; −|R∃p |
|
, // //
( ), // //x
y
xA St M
R xA St M
α−
α−
∃ Σ
∃ Σ
.
Форми типів RT, ΦN, R∃R, R∃p допоміжні, усі інші форми – основні.
|–∃R
,
| ,
|
( ), // '//
( ), // //
u x
v y
u
v
R A St M
R xA St M
α −
α −
Σ
∃ Σ
; –|∃R
,
| | ,
|
( ), ( ), // //
( ), // //
u u x
v v y
u
v
R xA R A St M
R xA St M
α− α−
α−
∃ Σ
∃ Σ
;
СЕМАНТИЧНІ МОДЕЛІ ТА СЕКВЕНЦІЙНІ ЧИСЛЕННЯ ТРАНЗИЦІЙНИХ МОДАЛЬНИХ ЛОГІК
Компьютерная математика. 2013, № 1 147
|–∃ |
|
( ), // '//
, // //
x
yR A St M
xA St M
α −
α −
Σ
∃ Σ
; –|∃ | |
|
, ( ), // //
, // //
x
yxA R A St M
xA St M
α− α−
α−
∃ Σ
∃ Σ
.
Для |–∃R умови: y∈VT, y∉nm(Γ, ∆, ( ))u
vR x∃ Φ ; при цьому до носія Aα стану α до-
дається новий елемент у. Для |–∃ умови: y∈VT, у∉nт(Σ, А); до Aα додається новий у.
Форми для пронесення реномінації через модальні оператори (тут �∈Ms):
|−R� |
|
( ), // //
( ), // //
v
x
v
x
R A St M
R A St M
α −
α −
Σ
Σ
�
�
; −|R� |
|
( ), // //
( ), // //
v
x
v
x
R A St M
R A St M
α−
α−
Σ
Σ
�
�
.
Форми елімінації модальних операторів записуються по-різному залежно
від властивостей відношень переходу. Традиційними є випадки, коли ці
відношення можуть бути транзитивними, рефлексивними чи симетричними. За-
уважимо, що для ТмМЛ, �↑ та �↓ при симетричності > діють ідентично, тому за
умови такої симетричності темпоральні числення ідентичні відповідним числен-
ням ЗТМЛ.
Наведемо як приклад форми |− Кi та −| Кi для наступних двох випадків.
1. Загальний випадок. Якщо на >i не накладені додаткові умови, то маємо:
|− Кi
| |
|
K , , // //
K , // //
i
i
A A St M
A St M
α − β −
α −
Σ
Σ
; −| Кi
|
|
, // ' // { }
K , // //
i
i
A St M
A St M
β−
α−
Σ ∪ α β
Σ
>
.
Форма |− Кi застосовується до α|− Кi A для всіх наявних у даний момент (згідно
схеми моделі світу М) станів β таких, що α>iβ. Якщо таких станів немає, то вво-
димо новий стан β (при цьому Aβ = Aα) та додаємо α>iβ до М.
Для форми −| Кi вводимо новий стан β, до схеми моделі світу М додаємо α>iβ
та задаємо Aβ = Aα .
2. >i транзитивне, рефлексивне та симетричне. У цьому випадку маємо:
|− Кi
| | |
|
K , , K , // //
K , // //
i i
i
A A A St M
A St M
α − β − β −
α −
Σ
Σ
; −| Кi
|
|
, // ' // { , }
K , // //
i i
i
A St M
A St M
β−
α−
Σ ∪ α β β α
Σ
> >
.
Форма |− Кi застосовується до α|− Кi A для всіх наявних у даний момент (згідно
схеми М) станів β таких, що α>i β чи β >i α. Специфікована β|− Кi A тут необхідна че-
рез транзитивність >i. Згідно з рефлексивністю >i при першому застосуванні фор-
ми |− Кi засновок має вигляд α|− Кi A, α|−A, Σ // St // M.
Для −| Кi вводимо новий стан β, до М додаємо α>iβ та β>iα, задаємо Aβ = Aα .
Теорема 3. Нехай | |
| |
//
//
M
M
− −
− −
Λ Κ
Γ ∆
та | | | |
| |
// //
//
M M
M
− − − −
− −
Λ Κ Χ Ζ
Γ ∆
– базові секвен-
ційні форми. Тоді: 1) якщо Λ |= Κ, то Γ |= ∆; 2) якщо Λ |= Κ та Χ |= Ζ, то Γ |= ∆.
Наслідок. Для наведених секвенційних форм маємо:
О.С. ШКІЛЬНЯК
148 Компьютерная математика. 2013, № 1
1) із Γ |≠ ∆ випливає Λ |≠ Κ; 2) із Γ |≠ ∆ випливає Λ |≠ Κ або Χ |≠ Ζ.
Побудова секвенційного дерева. Процедура побудови секвенційного дере-
ва для числень ТМЛ у цілому аналогічна відповідній процедурі для
секвенційних числень логік квазіарних предикатів [3]. Розглянемо її на прикладі
числень ММЛ.
Побудову дерева ведемо паралельно із побудовою схеми моделі світу. Ця схема
оновлюється при застосуванні −| Кi-форм (інколи |−Кi-форм), які додають нові ста-
ни. Побудова дерева розбита на етапи. На початку побудови зафіксуємо
нескінченний список TN «нових» тотально неістотних імен, які не зустрічаються в
початковій секвенції. Кожне застосування форми здійснюється до скінченної
множини доступних на даний момент формул. Перед застосуванням основної
форми при потребі застосовуємо належну кількість разів форми типів RT, ΦN,
R∃R, R∃p.
На кожному етапі спочатку виконуємо всі |–∃-форми та |–∃R-форми (при
цьому беремо нове у∈TN у відповідному стані). Потім виконуємо інші основні
форми, окрім елімінації модальностей. Форми –|∃-та |–∃R застосовуємо багато-
кратно – для усіх імен доступних формул даної секвенції та її наступників. Далі
ви-конуємо −| Кi-форми, потім багатократно (згідно схеми моделі світу) – |− Кi-
форми.
Процедура побудови завершена позитивно, якщо отримано замкнене дерево.
Якщо маємо скінченне незамкнене дерево або процедура не завершується, то
в дереві існує скінченний чи нескінченний незамкнений шлях. Кожна з формул
початкової секвенції зустрінеться на ньому і стане доступною.
Теорема 4 (коректності). Нехай секвенція |–Γ–|∆ вивідна. Тоді Γ |= ∆.
Нехай |–Γ–|∆ вивідна, тоді для неї побудоване замкнене секвенційне дерево.
Усі його листи – замкнені секвенції, тому для кожного такого листа |–Χ–|Ζ маємо
Χ |= Ζ. Рух від листів дерева до його кореня здійснюється за допомогою секвен-
ційних форм. За теоремою 3 при переході від засновків до висновків форм збері-
гається відношення |=. Тому для кожної вершини секвенційного дерева |–Λ–|Κ
маємо Λ|= Κ. Зокрема, для секвенції |–Γ–|∆ – кореня дерева – теж маємо Γ |= ∆.
Теорема повноти. Для доведення повноти секвенційних числень ТМЛ
використовується метод систем модельних множин. Система модельних множин
– це пара ({Нα | α∈S}, M), де Нα – модельна множина стану α, M – схема моделей
світу, яка задається R. Такі Нα визначаються умовою коректності (індукується
умовою замкненості секвенції) та умовами переходу (індукуються виконанням
відповідних форм). Для ЗТМЛ і ТмМЛ такі умови наведені в [5], тому вкажемо
лише умови, повязані з елімінацією кванторів та модальностей (для випадку ММЛ):
M∃) Якщо α|–∃хΦ∈Нα, то існує у∈Wα таке: | ( )x
yRα − Φ ∈Нα;
СЕМАНТИЧНІ МОДЕЛІ ТА СЕКВЕНЦІЙНІ ЧИСЛЕННЯ ТРАНЗИЦІЙНИХ МОДАЛЬНИХ ЛОГІК
Компьютерная математика. 2013, № 1 149
якщо α–|∃хΦ∈Нα, то | ( )x
yRα− Φ ∈Нα для всіх у∈Wα;
M∃R) якщо | ( )u
vR xα − ∃ Φ ∈Нα, то існує у∈Wα таке: ,
| , ( )u x
v yRα − Φ ∈Нα;
якщо | ( )u
vR xα− ∃ Φ ∈Нα, то ,
| , ( )u x
v yRα− Φ ∈Нα для всіх у∈Wα.
MК) якщо α|– Кi Φ∈Нα, то β|–Φ∈Нβ для всіх β∈S таких, що α>i β (тут Кi∈Ms);
якщо α–| Кi Φ∈Нα, то β–|Φ∈Нβ для деякого β∈S: α>i β (тут Кi∈Ms).
Теорема 5 (про контрмодель). Нехай ℘ – незамкнений шлях у секвен-
ційному дереві, Нα – множина всіх специфікованих α|– чи α–| формул секвенцій
шляху ℘, M – об'єднання усіх схем моделей світу секвенцій шляху ℘,
НM = ({Нα | α∈S}, M) та W = nт(НM). Тоді існують ТМС M = (S, R, А, Jт) та δ∈VA
з asn(δ) = W такі:
1) α|–Φ∈Нα ⇒ Φα(δ) = Т; 2) α–|Φ∈Нα ⇒ Φα(δ) = F.
Теорема доводиться індукцією за складністю формули згідно умов побудови
системи модельних множин НM (подібне доведення див. [5]).
Теорема 6 (повноти). Нехай Γ |= ∆. Тоді секвенція |–Γ–|∆ вивідна.
Припустимо супротивне: Γ |= ∆ (тобто Γ |=M ∆ для кожної узгодженої ТМС M),
проте |–Γ–|∆ невивідна. Тоді в секвенційному дереві для |–Γ–|∆ існує незамкнений
шлях. За теоремою 5 існують ТМС M = (S, R, А, Jт) та δ∈VA: α|–Φ∈Нα ⇒ Φα(δ) = Т,
α–|Φ∈Нα ⇒ Φα(δ) = F, де НM = ({Нα | α∈S}, M). Зокрема, це правильно для формул
секвенції |–Γ–|∆. Тому для всіх Φα∈Γ маємо Φα(δ) = Т та для всіх Ψβ∈∆ маємо
Ψβ(δ) = F. Це заперечує Γ |=M ∆, тому Γ |≠ ∆. Отримали суперечність, що й доводить
теорему.
Висновки. Досліджено нові класи програмно-орієнтованих логічних форма-
лізмів – чисті першопорядкові транзиційні модальні логіки еквітонних частко-
вих предикатів. У їх межах виділено мультимодальні, темпоральні, епістемічні
КНМЛ. Описано семантичні моделі та мови цих логік. На основі властивостей
відношення логічного наслідку для множин специфікованих станами формул
для пропонованих логік побудовано числення секвенційного типу. Характерною
особливістю цих числень є використання спрощених секвенційних форм елімі-
нації модальностей та елімінації кванторів під реномінаціями. Для побудованих
числень доведено теореми коректності та повноти.
1. Handbook of Logic in Computer Science. Edited by S. Abramsky, Dov M. Gabbay and T. S. E.
Maibaum. – Oxford Univ. Press. – Vol. 1–5, 1993–2000.
2. Андон Ф.И., Яшунин А.Е., Резниченко В.А. Логические модели интеллектуальных инфор-
мационных систем. – Киев: Наукова думка, 1999. – 396 с.
3. Нікітченко М.С., Шкільняк С.С. Математична логіка та теорія алгоритмів. – К., 2008. – 528 с.
О.С. ШКІЛЬНЯК
150 Компьютерная математика. 2013, № 1
4. Шкільняк О.С. Семантичні властивості композиційно-номінативних модальних логік //
Проблеми програмування. – 2009. – № 4. – C. 11–23.
5. Шкільняк О.С. Секвенційні числення композиційно-номінативних модальних і темпо-
ральних логік // Наук. записки НаУКМА. Серія: Комп. науки. – 2009. – Т. 99. – C. 37–44.
6. Нікітченко М.С., Шкільняк О.С., Шкільняк С.С. Побудова модальних логік темпорального
та епістемічного типу на основі композиційно-номінативного підходу // Вісник Київського
ун-ту. Серія: фіз.-мат. науки. – 2011. – Вип. 3. – С. 204–211.
Одержано 14.02.2013
О.C. Шкильняк
СЕМАНТИЧЕСКЕ МОДЕЛИ И СЕКВЕНЦИАЛЬНЫЕ ИСЧИСЛЕНИЯ
ТРАНЗИЦИОННЫХ МОДАЛЬНЫХ ЛОГИК
Исследованы чистые первопорядковые транзиционные модальные логики частичных преди-
катов. Описаны семантические модели и языки таких логик. Для предложенных логик
построены исчисления секвенциального типа. Для этих исчислений доказаны теоремы кор-
ректности и полноты.
O.S. Shkilniak
SEMANTIC MODELS AND SEQUENT CALCULI OF TRANSITIONAL MODAL LOGICS
Pure first-order transitional modal logics of partial predicates are studied. For the introduced logics,
we describe semantic models and languages and we construct sequent calculi. The correctness and
completeness theorems are proved for such calculi.
Про автора:
Шкільняк Оксана Степанівна,
кандидат фізико-математичних наук, асистент кафедри інформаційних систем
факультету кібернетики Київського національного університету імені Тараса Шевченка.
|
| id | nasplib_isofts_kiev_ua-123456789-84739 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | ХХХХ-0003 |
| language | Ukrainian |
| last_indexed | 2025-12-07T17:54:13Z |
| publishDate | 2013 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Шкільняк, О.С. 2015-07-14T12:06:21Z 2015-07-14T12:06:21Z 2013 Семантичні моделі та секвенційні числення транзиційних модальних логік / О.С. Шкільняк // Компьютерная математика. — 2013. — № 1. — С. 141-150. — Бібліогр.: 6 назв. — укр. ХХХХ-0003 https://nasplib.isofts.kiev.ua/handle/123456789/84739 004.42:510.69 Досліджено чисті першопорядкові транзиційні модальні логіки часткових предикатів. Описано семантичні моделі та мови таких логік Для пропонованих логік побудовано числення секвенційного типу. Для цих числень доведено теореми коректності й повноти. Исследованы чистые первопорядковые транзиционные модальные логики частичных предикатов. Описаны семантические модели и языки таких логик. Для предложенных логик построены исчисления секвенциального типа. Для этих исчислений доказаны теоремы корректности и полноты. Pure first-order transitional modal logics of partial predicates are studied. For the introduced logics, we describe semantic models and languages and we construct sequent calculi. The correctness and completeness theorems are proved for such calculi. uk Інститут кібернетики ім. В.М. Глушкова НАН України Компьютерная математика Экспертные системы, методы индуктивного вывода Семантичні моделі та секвенційні числення транзиційних модальних логік Семантическе модели и секвенциальные исчисления транзиционных модальных логик Semantic models and sequent calculi of transitional modal logics Article published earlier |
| spellingShingle | Семантичні моделі та секвенційні числення транзиційних модальних логік Шкільняк, О.С. Экспертные системы, методы индуктивного вывода |
| title | Семантичні моделі та секвенційні числення транзиційних модальних логік |
| title_alt | Семантическе модели и секвенциальные исчисления транзиционных модальных логик Semantic models and sequent calculi of transitional modal logics |
| title_full | Семантичні моделі та секвенційні числення транзиційних модальних логік |
| title_fullStr | Семантичні моделі та секвенційні числення транзиційних модальних логік |
| title_full_unstemmed | Семантичні моделі та секвенційні числення транзиційних модальних логік |
| title_short | Семантичні моделі та секвенційні числення транзиційних модальних логік |
| title_sort | семантичні моделі та секвенційні числення транзиційних модальних логік |
| topic | Экспертные системы, методы индуктивного вывода |
| topic_facet | Экспертные системы, методы индуктивного вывода |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/84739 |
| work_keys_str_mv | AT škílʹnâkos semantičnímodelítasekvencíiníčislennâtranzicíinihmodalʹnihlogík AT škílʹnâkos semantičeskemodeliisekvencialʹnyeisčisleniâtranzicionnyhmodalʹnyhlogik AT škílʹnâkos semanticmodelsandsequentcalculioftransitionalmodallogics |