Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня
Досліджуються композиційно-номінативні модальні та темпоральні логіки функціонально-екваційного рівня. На основі властивостей відношення логічного наслідку для множин формул збудовані числення секвенційного типу для загальних та темпоральних композиційно-номінативних модальних логік такого рівня. Дл...
Gespeichert in:
| Datum: | 2011 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
Інститут програмних систем НАН України
2011
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/50919 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня/ О.С. Шкільняк // Пробл. програмув. — 2011. — № 1. — С. 17-28. — Бібліогр.: 8 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-50919 |
|---|---|
| record_format |
dspace |
| spelling |
Шкільняк, О.С. 2013-11-06T17:35:38Z 2013-11-06T17:35:38Z 2011 Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня/ О.С. Шкільняк // Пробл. програмув. — 2011. — № 1. — С. 17-28. — Бібліогр.: 8 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/50919 510.69 Досліджуються композиційно-номінативні модальні та темпоральні логіки функціонально-екваційного рівня. На основі властивостей відношення логічного наслідку для множин формул збудовані числення секвенційного типу для загальних та темпоральних композиційно-номінативних модальних логік такого рівня. Для побудованих числень доведені теореми коректності та повноти. uk Інститут програмних систем НАН України Теоретичні та методологічні основи програмування Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня |
| spellingShingle |
Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня Шкільняк, О.С. Теоретичні та методологічні основи програмування |
| title_short |
Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня |
| title_full |
Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня |
| title_fullStr |
Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня |
| title_full_unstemmed |
Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня |
| title_sort |
секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня |
| author |
Шкільняк, О.С. |
| author_facet |
Шкільняк, О.С. |
| topic |
Теоретичні та методологічні основи програмування |
| topic_facet |
Теоретичні та методологічні основи програмування |
| publishDate |
2011 |
| language |
Ukrainian |
| publisher |
Інститут програмних систем НАН України |
| format |
Article |
| description |
Досліджуються композиційно-номінативні модальні та темпоральні логіки функціонально-екваційного рівня. На основі властивостей відношення логічного наслідку для множин формул збудовані числення секвенційного типу для загальних та темпоральних композиційно-номінативних модальних логік такого рівня. Для побудованих числень доведені теореми коректності та повноти.
|
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/50919 |
| citation_txt |
Секвенційні числення композиційно-номінативних модальних логік функціонально-екваційного рівня/ О.С. Шкільняк // Пробл. програмув. — 2011. — № 1. — С. 17-28. — Бібліогр.: 8 назв. — укр. |
| work_keys_str_mv |
AT škílʹnâkos sekvencíiníčislennâkompozicíinonomínativnihmodalʹnihlogíkfunkcíonalʹnoekvacíinogorívnâ |
| first_indexed |
2025-11-26T00:09:38Z |
| last_indexed |
2025-11-26T00:09:38Z |
| _version_ |
1850593944098832384 |
| fulltext |
Теоретичні та методологічні основи програмування
17
УДК 510.69
О.С. Шкільняк
CЕКВЕНЦІЙНІ ЧИСЛЕННЯ КОМПОЗИЦІЙНО-
НОМІНАТИВНИХ МОДАЛЬНИХ ЛОГІК
ФУНКЦІОНАЛЬНО-ЕКВАЦІЙНОГО РІВНЯ
Досліджуються композиційно-номінативні модальні та темпоральні логіки функціонально-екваційного
рівня. На основі властивостей відношення логічного наслідку для множин формул збудовані числення
секвенційного типу для загальних та темпоральних композиційно-номінативних модальних логік
такого рівня. Для побудованих числень доведені теореми коректності та повноти.
Вcтуп
Модальні та темпоральні логіки є
потужним засобом моделювання різнома-
нітних предметних областей, специфікації
та верифікації програм. Композиційно-
номінативні модальні логіки (КНМЛ) [1]
поєднують можливості традиційних мод-
альних логік [2, 3] та композиційно-номі-
нативних логік (КНЛ) квазіарних предика-
тів [4].
Центральним поняттям КНМЛ є [1]
поняття композиційно-номінативної мо-
дальної системи (КНМС). Спеціальне
уточнення КНМС для логік номінативних
рівнів запропоноване в [5]. Композиційно-
номінативні модальні та темпоральні логі-
ки на пропозиційному, реномінативному,
кванторному та кванторно-екваційному рів-
нях досліджені в [5–7], для цих логік збу-
довані числення секвенційного типу. Ком-
позиційно-номінативні модальні та темпо-
ральні логіки функціонально-екваційного
рівня розглянуті в [8]. Для таких логік
визначені транзиційні (ТМС), загальні та
темпоральні модальні системи, досліджені
їх семантичні властивості.
У даній роботі продовжується до-
слідження функціонально-екваційних ком-
позиційно-номінативних модальних та
темпоральних логік. На основі властиво-
стей відношення логічного наслідку для
множин специфікованих станами формул
будуються числення секвенційного типу
для загальних транзиційних та темпораль-
них КНМЛ функціонально-екваційного
рівня. Для таких числень доводяться тео-
реми коректності та повноти.
Поняття, які тут не визначаються,
будемо тлумачити в сенсі робіт [4, 6–8].
1. Відношення логічного наслідку
для множин формул КНМЛ
функціонально-екваційного рівня
Нагадаємо визначення відношення
логічного наслідку для множин специфіко-
ваних станами формул. Нехай Δ та Γ –
множини таких формул.
Δ є логічним наслідком Γ в КНМС
M (позначаємо Γ |=M Δ), якщо для всіх d∈VA
із того, що Φα(d ∩VAα) = T для всіх Φα∈Γ,
випливає, що неможливо Ψβ(d ∩VAβ) = F для
всіх Ψβ∈Δ.
Δ є логічним наслідком Γ (щодо
КНМС певного типу), якщо Γ |=M Δ для
всіх КНМС M відповідного типу.
Те, що Δ є логічним наслідком Γ,
позначаємо Γ |= Δ.
Приклад 1. Для випадку функціо-
нально стабільних [8] ТМС можливо:
1) t = sα, Γ |=M Δ та t = sα, Γ |≠M Δ;
2) t = sα, Γ |=M Δ та t = sα, Γ |≠M Δ.
Задамо КНМС M такого вигляду:
S = {α, β}, R = {α>
.
β}. Покладемо Γ = ∅,
Δ = {Ψα}.
1. Нехай Aα = {a, b}, Aβ = {b}, для Ψ
неістотні всі імена, окрім x та y. Візьмемо
‘x та ‘y як терми t та s. Задамо
Ψα([xaa, yaa]) = F; задамо Ψα(δ) = T при
умові δ∈{a, b}{x, y} та b∈den(δ).
© О С. Шкільняк, 2011
ISSN 1727-4907. Проблеми програмування. 2011. № 1
Теоретичні та методологічні основи програмування
18
Нехай d = [xaa, yaa]. Тоді dα= d.
Маємо dα(x)↓ = dα(y)↓ = a, звідки отримуємо
‘x =‘yα(dα) = T, тому ‘x =‘yα |≠M Ψα. Проте
dα∉VAβ, звідки ‘x =‘yβ(dα)↑, що дає
‘x =‘yα(dα)↑. У випадку δ∈{a, b}{x, y} та
b∈den(δ) отримуємо Ψα(δ) = T; у випадку
δ∈{a, b}{x, y} та b∉den(δ) маємо δ = dα = d,
тоді dα∉VAβ, звідки ‘x =‘yβ(dα)↑, що дає
‘x =‘yα(dα)↑. Отже, ‘x =‘yα |=M Ψα.
2. Нехай Aα = Aβ = {0}, для t, s, Ψ
неістотні всі імена, окрім x. Для довільного
d ⊇ [xa0] задамо tα(d)↑, sα(d)↑, Ψα(d) = F,
tβ(d) = sβ(d) = 0, Ψβ(d)↑. Тоді (t = s)β(d) = T,
звідки ( t = s)α(d) = T. Звідси отримуємо,
що ( t = s →Ψ)α(d) = F, (t = s →Ψ)α(d)↑,
(t = s →Ψ)β(d)↑. Для усіх інших δ вважаємо
tα(δ)↑, sα(δ)↑, Ψα(δ)↑, tβ(δ)↑, sβ(δ)↑, Ψβ(δ)↑.
Тоді отримуємо α |= t = s →Ψ, β |= t = s →Ψ,
α |≠ t = s →Ψ, звідки M |= t = s →Ψ та
M |≠ t = s →Ψ, що дає t = sα |=M Ψα та
t = sα |≠M Ψα.
До успадкованих із пропозиційного
рівня властивостей ПС, П1–П4 та модаль-
них властивостей [7] додаємо властивості,
які формулюються на основі семантичних
властивостей ФЕНКЛ [4]. Вони є розвит-
ком відповідних семантичних властиво-
стей КНМЛ кванторного рівня з рівністю.
ZNΦ|−) , ( , , ) ,x vS s t αΦ Γ |=M Δ ⇔
⇔ ( , ) ,vS t αΦ Γ |=M Δ при умові x∈μ(Φ).
ZNΦ–|) Γ |=M Δ, , ( , , )x vS s t αΦ ⇔
⇔ Γ |=M Δ, ( , )vS t αΦ при умові x∈μ(Φ).
ZΦ|−) , ( , ' , ) ,x vS x t αΦ Γ |=M Δ ⇔
⇔ ( , ) ,vS t αΦ Γ |=M Δ.
ZΦ–|) Γ |=M Δ, , ( , ' , )x vS x t αΦ ⇔
⇔ Γ |=M Δ, ( , ) .vS t αΦ
TrN|−) Φα, Γ |=M Δ ⇔ Ψα, Γ |=M Δ.
TrN−|) Γ |=M Δ, Φα ⇔ Γ |=M Δ, Ψα.
Для TrN формула Ψ отримана із
формули Φ нормалізацією термів на основі
властивостей ZT, ZNT, DD, DS, SST [4].
S¬|−) ( , )xS t α¬Φ
S¬–|) Γ |=M Δ, ( , )xS t α¬Φ ⇔
⇔ Γ |=M Δ, ( , )xS t α¬ Φ .
S∨|−) ( , )xS αΦ∨Ψ ,t Γ |=M Δ ⇔
⇔ ( , ) ( , ) ,x xS t S t αΦ ∨ Ψ Γ |=M Δ.
S∨–|) Γ |=M Δ, ( ,xS t αΦ∨Ψ ) ⇔
⇔ Γ |=M Δ, ( , ) ( , )x xS t S t αΦ ∨ Ψ .
SSΦ|−) , ,( ( , , ), , )u x x vS S r s t w ,αΦ Γ
|=M Δ ⇔ Ξα, Γ |=M Δ.
SSΦ–|) Γ |=M Δ,
, ,( ( , , ), , )u x x vS S r s t w αΦ ⇔ Γ |=M Δ, Ξα.
Для SSΦ Ξ – це формула
, , , ,
1( , , ( , , ),..., ( , , ),u x v u x u x
kS t S r t w S r t wΦ
, ,
1( , , ),..., ( , , )).u x u x
mS s t w S s t w
S∃|−) ( , )vS x t α∃ Φ ,Γ |=M Δ ⇔
⇔ ( , ) ,vxS t α∃ Φ Γ |=M Δ.
S∃–|) Γ |=M Δ, ( , )vS x t α∃ Φ ⇔
⇔ Γ |=M Δ, ( , )vxS t α∃ Φ .
Для властивостей S∃ умова x∉{ }v
та x неістотне для t .
S∃∃|−) ( , )vS x t α∃ Φ ,Γ |=M Δ ⇔
⇔ , ( , , ' ) ,v xyS t y α∃ Φ Γ |=M Δ.
S∃∃–|) Γ |=M Δ, ( , )vS x t α∃ Φ ⇔
⇔ Γ |=M Δ, , ( , , ' ) .v xyS t y α∃ Φ
Для S∃∃ умова ( ( , ))vy ndn S x t∉ ∃ Φ
та y тотально неістотне.
∃|–) ∃хΦα, Γ |=M Δ ⇔
⇔ ( , ' )xS y αΦ , Γ |=M Δ при у тотально
неістотному та у∉пdn(Γ, Δ,Φ).
∃–|) Γ |=M Δ, ∃хΦα ⇔
⇔ Γ |=M Δ, 1( , ) ,..., ( , ) ,x x
nS t S tα αΦ Φ ∃хΦα.
SE|−) ( , )vS r s t α= ,Γ |=M Δ ⇔
⇔ ( , ) ( , ) ,v vS r t S s t α= Γ |=M Δ.
SE−|) Γ |=M Δ, ( , )vS r s t α= ⇔
⇔ Γ |=M Δ, ( , ) ( , ) .v vS r t S s t α=
ESm) t = sα, Γ |=M Δ ⇔
⇔ t = sα, s = tα, Γ |=M Δ. ,Γ |=M Δ ⇔
⇔ ( , ) ,xS t α¬ Φ Γ |=M Δ. ETr) t = sα, s = rα, Γ |=M Δ ⇔
⇔ t = sα, s = rα, t = rα, Γ |=M Δ.
Теоретичні та методологічні основи програмування
19
EPr|−) t = sα, ϕα, Γ |=M Δ ⇔
⇔ t = sα, ϕα, ξα, Γ |=M Δ.
EPr−|) t = sα, Γ |=M Δ, ϕα ⇔
⇔ t = sα, Γ |=M Δ, ϕα, ξα.
Тут ϕ та ξ – t = s-еквівалентні
примітивні формули.
Для функціонально стабільних ТМС
згідно теореми 4 [8] отримуємо наступні
властивості:
S |−) Γ, ( , )vS t αΦ |=M Δ ⇔
⇔ Γ, ( , )vS t αΦ |=M Δ.
S −|) Γ |=M Δ, ( , )vS t αΦ ⇔
⇔ Γ |=M Δ, ( , )vS t αΦ .
2. Секвенційні форми числень
функціонально-екваційного рівня
Cеквенційні числення КНМЛ функ-
ціонально-екваційного рівня можна трак-
тувати як прикладні секвенційні числення.
Виведення в таких численнях є виведен-
нями збагачених секвенцій – секвенцій з
доданими аксіомами для рівності. До них
належать:
– аксіома рефлексивності ∀x('x = 'x);
– аксіома симетричності
∀x∀y('x = 'y → 'y = 'x);
– аксіома транзитивності
∀x∀y∀z('x = 'y → 'y = 'z → 'x = 'z).
Тут x, y, z – тотально неістотні.
– аксіоми заміни рівних у нормаль-
них термах (для всіх f∈Fns та , ,z u t )
∀x∀y ('x = 'y →
,z uS (f, 'x, t ) =
,z uS (f, 'y, t ));
– аксіоми заміни рівних в елемен-
тарних формулах (для всіх p∈Ps та , ,z u t )
∀x∀y ('x = 'y →( ,z uS (p, 'x, t ) ↔
,z uS (p, 'y, t )).
Тут x, y – тотально неістотні, причо-
му x, y відмінні від ,z t та x, y ∉ nm( t ).
Секвенційні форми числень КНМЛ
функціонально-екваційного рівня індуко-
вані відповідними властивостями відно-
шення |=. До базових секвенційних форм
таких числень найперше віднесемо форми,
успадковані від числень КНЛ [4]. Вони не
змінюють схему моделі світу. Це |–¬, –|¬,
|–∨, –|∨, |–SSΦ, –|SSΦ, |–S¬, –|S¬, |–S∨, –|S∨,
|–S∃, –|S∃, |–S∃∃, –|S∃∃, |–∃, –|∃,|–ZNΦ, –|ZNΦ,
|–ZΦ,–|ZΦ, |–SЕ, –|SЕ, а також форми, при-
значені для нормалізації термів.
Наведемо ці секвенційні форми:
|– ¬ |
|
, // //
;
, // //
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
α− α−
α−
Σ
∨ Σ
Нехай B отримана з A згорткою супер-
позицій згідно із SSΦ. Відповідні форми:
|–SSΦ |
|
, // //
;
, // //
B St M
A St M
α −
α −
Σ
Σ
–|SSΦ |
|
, // //
.
, // //
B St M
A St M
α−
α−
Σ
Σ
Секвенційні форми для пронесення
суперпозицій через ¬ та ∨:
|–S¬ |
|
( , ), // //
;
( , ), // //
v
v
S A t St M
S A t St M
α −
α −
¬ Σ
¬ Σ
–|S¬ |
|
( , ), // //
;
( , ), // //
v
v
S A t St M
S A t St M
α−
α−
¬ Σ
¬ Σ
|–S∨ |
|
( , ) ( , ), // //
;
( , ), // //
v v
v
S A t S B t St M
S A B t St M
α−
α−
∨ Σ
∨ Σ
–|S∨ |
|
( , ) ( , ), // //
.
( , ), // //
v v
v
S A t S B t St M
S A B t St M
α−
α−
∨ Σ
∨ Σ
Секвенційні форми для елімінації
неістотних імен і спрощення формул:
|–ZN |
,
|
( , ), // //
;
( , , ), // //
v
x v
S p t St M
S p t t St M
α−
α−
Σ
Σ
–|ZN |
,
|
( , ), // //
.
( , , ), // //
v
x v
S p t St M
S p t t St M
α−
α−
Σ
Σ
Для форм типу ZN умова: x∈μ(p).
|–ZΦ |
,
|
( , ), // //
;
( , ' , ), // //
v
x v
S A t St M
S A x t St M
α−
α−
Σ
Σ
Теоретичні та методологічні основи програмування
20
–|ZΦ |
,
|
( , ), // //
.
( , ' , ), // //
v
x v
S A t St M
S A x t St M
α−
α−
Σ
Σ
Секвенційні форми для пронесення
суперпозиції через рівність:
|–SЕ |
|
( , ) ( , ), // //
;
( , ), // //
v v
v
S t t S s t St M
S t s t St M
α−
α−
= Σ
= Σ
–|SЕ |
|
( , ) ( , ), // //
.
( , ), // //
v v
v
S t t S s t St M
S t s t St M
α−
α−
= Σ
= Σ
Задамо секвенційні форми для норма-
лізації термів.
Нехай B отримана з A виконанням
кроку нормалізації термів на основі власти-
востей SST, ZNT, ZT, DS, DD. Отримуємо
секвенційні форми |–SST, –|SST, |–ZNT,
–|ZNT, |–ZT, –|ZT, |–DS, –|DS, |–DD, –|DD.
Вони мають наступний вигляд (тут тип
означає SST, ZNT, ZT, DS, DD):
|– тип |
|
, // //
;
, // //
B St M
A St M
α −
α −
Σ
Σ
–| тип |
|
, // //
.
, // //
B St M
A St M
α−
α−
Σ
Σ
Базові секвенційні форми |–SST та
–|SST, |–ZNT та –|ZNT, |–ZT та –|ZT, |–DS та
–|DS, |–DD та–|DD індукують похідні форми
нормалізації термів |–TrN та –|TrN:
|–TrN |
|
, // //
;
, // //
B St M
A St M
α −
α −
Σ
Σ
–|TrN |
|
, // //
.
, // //
B St M
A St M
α−
α−
Σ
Σ
Тут B отримана з A нормалізацією
термів на основі властивостей SST, ZNT, ZT,
DS, DD.
Секвенційні форми для пронесення
суперпозицій через квантор:
|–S∃ |
|
( , ), // //
;
( , ), // //
v
v
xS A t St M
S xA t St M
α −
α −
∃ Σ
∃ Σ
–|S∃ |
|
( , ), // //
;
( , ), // //
v
v
xS A t St M
S xA t St M
α−
α−
∃ Σ
∃ Σ
|–S∃∃
,
|
|
( , , ' ), // ' //
;
( , ), // //
v x
v
yS A t y St M
S xA t St M
α−
α−
∃ Σ
∃ Σ
–|S∃∃
,
|
|
( , , ' ), // ' //
.
( , ), // //
v x
v
yS A t y St M
S xA t St M
α−
α−
∃ Σ
∃ Σ
Для |–S∃ та –|S∃ умови: х∉{ v } та
x∈μ( t ). Для |–S∃∃ та –|S∃∃ умови: х∈{ v }
або x∉μ( t ), причому y тотально неістотне
та y∉ndn( vS (∃xΦ, t )).
Наведемо секвенційні форми для
елімінації кванторів.
|–∃ |
|
( , ' ), // //
.
, // //
xS A y St M
xA St M
α −
α −
Σ
∃ Σ
Для |–∃ умова: у тотально неістотне та
у∉пdn(Σ, А).
–|∃ | 1 | |
|
( , ),..., ( , ), , // //
.
, // //
x x
nS A t S A t xA St M
xA St M
α− α− α−
α−
Σ ∃
∃ Σ
Для –|∃ терми t1,…, tn нормальні, по-
будовані з ФНС і ДНС-дублів імен доступ-
них формул секвенції α−|∃xА, Σ та її наступ-
ників.
Для пронесення модальності через
суперпозицію необхідна умова функціо-
нальної стабільності. Тому семантичними
моделями секвенційних числень КНМЛ
функціонально-екваційного рівня ввжаємо
функціонально стабільні ТМС. Звідси має-
мо форми:
|–S |
|
( , ), // //
;
( , ), // //
v
v
S A t St M
S A t St M
α−
α−
Σ
Σ
–|S |
|
( , ), // //
.
( , ), // //
v
v
S A t St M
S A t St M
α−
α−
Σ
Σ
Наявність аксіом рівності означає,
що для кожного наявного в секвенції стану
α в ній мусять бути присутні α|–∀x('x = 'x),
α|–∀x∀y('x = 'y → 'y = 'x),
α|–∀x∀y∀z('x = 'y → 'y = 'z → 'x = 'z), а також
α|–∀x∀y('x = 'y →
,z uS (f, 'x, t ) =
,z uS (f, 'y, t )) та
α|–∀x∀y('x = 'y →( ,z uS (p, 'x, t ) ↔
,z uS (p, 'y, t ))
для всіх f∈Fns, p∈Ps та , ,z u t .
Поява нового стану α веде до яв-
ного виписування таких специфікованих
формул. Проте не будемо явно вносити до
Теоретичні та методологічні основи програмування
21
формул секвенції зазначені аксіоми, а бу-
демо враховувати їх при потребі. При
цьому замість продукування всеможливих
елементарних формул-рівностей та еквіва-
лентних елементарних формул на основі
аксіом заміни рівних, використаємо влас-
тивість EPr [8], яка при умові α|= t = s дає
змогу продукувати t=s-варіанти доступних
примітивних формул стану α. Це означає
наступну модифікацію процедури побудо-
ви секвенційного дерева.
Аксіома рефлексивності вимагає,
щоб при появі в стані α кожного нового
терма t до секвенції додавалась α|– t = t. Тому
цю аксіому можна врахувати введенням
додаткової умови замкненості секвенції:
наявність специфікованої формули вигляду
α–| t = t.
Нехай на попередньому кроці була
отримана формула α|–t= s, або формула
α|–t = s стала доступною на початку етапу
(тут s та t – нормальні терми). Далі робимо
наступні додаткові кроки.
Для врахування аксіоми симетричності
додаємо формулу α|–s = t. Для цього викори-
стовуємо допоміжну секвенційну форму:
ЕSm | |
|
, , // //
.
, // //
t s s t St M
t s St M
α− α−
α−
= = Σ
= Σ
Нехай невірно t∠s та невірно s∠t
(σ∠ρ означає [8], що терм σ є підтермом
терма чи формули ρ). Тоді для кожної дос-
тупної специфікованої примітивної форму-
ли α|–ϕ чи α–|ϕ, до складу якої входить t або
s, будуємо t=s-еквівалентні їй формули
(t=s-варіанти формули ϕ) з тією ж специ-
фікацією, всеможливими способами замі-
нюючи деякі входження t на s та s на t.
Нехай t∠s. Тоді для кожної доступ-
ної специфікованої примітивної формули
α|–ϕ чи α–|ϕ, до складу якої входить s, буду-
ємо її t=s-варіанти з тією ж специфікацією,
всеможливими способами замінюючи де-
які входження s на t (можливо, за декілька
кроків, адже при заміні s на t може виник-
нути нове входження s, яке замінимо на t і
т.д.). Заміни t на s не робимо, адже тоді
процес заміни не обірветься.
Аналогічно робимо у випадку s∠t,
тоді виконуємо заміни t на s.
Допоміжні секвенційні форми для
отримання t=s-варіант:
|–ЕPr | | |
| |
, , , // //
;
, , // //
t s St M
t s St M
α− α− α−
α− α−
= ϕ ψ Σ
= ϕ Σ
–|ЕPr | | |
| |
, , , // //
.
, , // //
t s St M
t s St M
α− α− α−
α− α−
= ϕ ψ Σ
= ϕ Σ
Тут ϕ та ψ – t=s-еквівалентні примі-
тивні формули, причому ψ отримана із ϕ
так, як вищеописано.
Для врахування аксіоми транзитив-
ності при появі α|–t = s та α|–s = r додаємо
α|–t = r (фактично, враховуючи симетрич-
ність рівності, до наявних α|–t = s, α|–s = t,
α|–s = r, α|–r = s додаємо α|–t = r, α|–r = t), а далі
робимо так, як вищеописано.
Допоміжна секвенційна форма для
врахування аксіоми транзитивності:
ЕTr | | |
| |
, , , // //
.
, , // //
t s s r t r St M
t s s r St M
α− α − α−
α− α−
= = = Σ
= = Σ
Секвенційні форми для модальних
операторів аналогічні відповідним секвен-
ційним формам пропозиційного та кван-
торного рівнів (див. [5, 6]).
3. Коректність і повнота
секвенційних числень загальних
та темпоральних КНМЛ
Процедура побудови секвенційного
дерева в основному аналогічна відповідній
процедурі для секвенційних числень КНЛ
[4], але побудова дерева ведеться пара-
лельно із побудовою схеми моделей світу.
При цьому схема моделей світу оновлю-
ється при використанні –| -форми, яка
додає нові стани. На початку побудови
зафіксуємо деякий нескінченний список TN
"нових" тотально неістотних імен, такі імена
та відповідні "нові" ДНС не зустрічаються в
початковій секвенції. З кожним листом де-
рева пов’язуємо списки ATr, AFs, ADn від-
повідно активних термів, ФНС, ДНС-дублів
імен. Терми будуються з ФНС та ДНС-дуб-
лів імен доступних формул відповідного
стану для листа та його наступників.
Побудова секвенційного дерева роз-
бита на етапи. Кожне застосування секвен-
ційної форми здійснюється до скінченної
Теоретичні та методологічні основи програмування
22
множини доступних на даний момент фор-
мул. На початку кожного етапу розши-
рюємо список доступних формул, розширю-
ємо AFs та ADn. Спочатку виконуємо –| -
форми, які додають нові стани. Потім
виконуємо всі |–∃-форми, які додають нові
терми (кожне таке виконання задіює нове
z∈TN, далі для відповідного стану додаємо
z’ до ADn та розширюємо ATr так, як
описано в [4]). Після цього виконуємо всі
S∃∃-форми, далі – форми типу |–¬, –|¬, |–∨,
–|∨, |–SSΦ, –|SSΦ, |–S¬, –|S¬, |–S∨, –|S∨, |–SЕ,
–|SЕ, |–S∃, –|S∃, |–S , –|S , –|∃. При застосу-
ванні –|∃ використовуємо терми ATr. До
кожної отриманої таким чином нової фор-
мули як допоміжні застосовуємо, за можли-
вості, форми типу |–ZΦ, –|ZΦ, |–ZNΦ, –|ZNΦ.
Якщо нова формула елементарна, але
непримітивна, то додатково застосовуємо
форми типу |–TrN, –|TrN.
При потребі виконуємо також додат-
кові кроки для продукування нових при-
мітивних формул-рівностей (форми ЕSm і
ЕTr) та отримання t=s-варіант доступних
примітивних формул (форми |–ЕPr і –|ЕPr)
так, як вищеописано. Враховуємо також
наступну умову замкненості секвенції: на-
явність специфікованої формули вигляду
α–| t = t.
На основі семантичних властиво-
стей відношення |= для секвенційних чис-
лень КНМЛ функціонально-екваційного
рівня отримуємо наступну теорему.
Теорема 1. 1) нехай
| |
| |
// ' // '
// //
St M
St M
− −
− −
Λ Κ
Γ Δ
– секвенційна форма.
Тоді якщо Λ |= Κ, то Γ |= Δ;
2) нехай
| | | |
| |
// // // //
// //
St M St M
St M
− − − −
− −
Λ Κ Χ Ζ
Γ Δ
–
секвенційна форма. Тоді якщо Λ |= Κ та
Χ |= Ζ, то Γ |= Δ.
Для секвенційних числень КНМЛ
функціонально-екваційного рівня справ-
джується
Теорема 2 (коректності). Нехай сек-
венція |–Γ–|Δ вивідна. Тоді Γ |= Δ.
Доведення аналогічне доведенню
відповідної теореми традиційних секвен-
ційних числень. Воно здійснюється індук-
цією за побудовою замкненого секвен-
ційного дерева для |–Γ–|Δ. Для гарантування
пронесення суперпозицій через модальні
композиції обмежуємо клас ТМС умовою
функціональної стабільності.
Нехай для |–Γ–|Δ маємо замкнене
тривіальне дерево, тоді воно складається з
єдиної вершини |–Γ–|Δ, яка є замкненою
секвенцією. Звідси Γ |= Δ.
Нехай для |–Γ–|Δ маємо замкнене
секвенційне дерево γ, причому на остан-
ньому кроці виведення була застосована
секвенційна форма | |
| |
// ' // '
// //
St M
St M
− −
− −
Λ Κ
Γ Δ
. За
припущенням індукції маємо Λ |= Κ. За тео-
ремою 1 тоді Γ |= Δ.
Нехай для |–Γ–|Δ маємо замкнене
секвенційне дерево та останньому кроці
виведення застосована секвенційна форма
| | | |
| |
// // // //
// //
St M St M
St M
− − − −
− −
Λ Κ Χ Ζ
Γ Δ
. За
припущенням індукції маємо Λ |= Κ та
Χ |= Ζ для кожної узгодженої ТМС M. За
теоремою 1 тоді Γ |= Δ.
Теорема доведена.
Для доведення повноти секвенційних
числень КНМЛ функціонально-екваційно-
го рівня використовуємо метод систем мо-
дельних множин.
Система модельних множин – це
пара (Ω, R), де Ω = {Нα | α∈S}.
Нехай Trα – множина нормальних
термів, побудованих із ФНС та ДНС-дублів
імен формул множин Нα.
Множина Нα специфікованих фор-
мул із Wα = nm(Нα) – модельна множина
стану α, якщо виконуються такі умови.
HC. Для кожної примітивної Φ лише
одна з формул α|–Φ чи α–|Φ може належати
до Нα .
HN. Нехай Φ – елементарна форму-
ла, Ψ – примітивна формула, отримана з Φ
нормалізацією термів на основі власти-
востей SST, ZNT, ZT, DS, DD. Тоді:
якщо α|–Φ∈Нα, то α|–Ψ∈Нα ;
якщо α–|Φ∈Нα, то α–|Ψ∈Нα .
Теоретичні та методологічні основи програмування
23
HNΦ. Якщо α|–
, ( , , )x vS sΦ t ∈Нα та
у∈μ(Φ), то α|– ( , )vS tΦ ∈Нα ;
якщо α–|
, ( , , )x vS sΦ t ∈Нα та у∈μ(Φ),
то α–| ( , )vS tΦ ∈Нα .
HΦ. Якщо |– , ( , ' , )x vS xΦ t ∈Нα, то
|– ( , )vS tΦ ∈Нα ;
якщо –|
, ( , ' , )x vS xΦ t ∈Нα, то
–| ( , )vS tΦ ∈Нα .
H¬. Якщо α|–¬Φ∈Нα, то α–|Φ∈Нα ;
якщо α–|¬Φ∈Нα, то α|–Φ∈Нα .
H∨. Якщо α|–Φ∨Ψ∈Нα, то α|–Φ∈Нα
або α|–Ψ∈Нα ;
якщо α–|Φ∨Ψ∈Нα, то α–|Φ∈Нα та
α–|Ψ∈Нα .
HSΦ. Якщо
α|–
, ,( ( , , ), ,u x x vS S r s t wΦ )∈Нα, то
α|–
, , , ,
1( , , ( , , ),..., ( , , ),u x v u x u x
kS t S r t w S r t wΦ
, ,
1( , , ),..., ( , , ))u x u x
mS s t w S s t w ∈Нα ;
якщо α–|
, ,( ( , , ), ,u x x vS S r s t wΦ )∈Нα, то
α–|
, , , ,
1( , , ( , , ),..., ( , , ),u x v u x u x
kS t S r t w S r t wΦ
, ,
1( , , ),..., ( , , ))u x u x
mS s t w S s t w ∈Нα .
HS¬. Якщо α|– ( ,xS ¬Φ )t ∈Нα, то
α|– ( , )xS t¬ Φ ∈Нα ;
якщо α–| ( ,xS ¬Φ )t ∈Нα, то
α–| ( , )xS t¬ Φ ∈Нα .
HS∨. Якщо α|– ( ,xS Φ∨Ψ )t ∈Нα, то
α|– ( , ) ( , )x xS t S tΦ ∨ Ψ ∈Нα ;
якщо α–| ( ,xS Φ∨Ψ )t ∈Нα, то
α–| ( , ) ( , )x xS t S tΦ ∨ Ψ ∈Нα .
HSE. Якщо α|– ( ,vS r s t= )∈Нα, то
α|– ( , ) ( , )v vS r t S s t= ∈Нα ;
якщо α–| ( ,vS r s t= )∈Нα, то
α–| ( , ) ( , )v vS r t S s t= ∈Нα .
HS∃. Якщо х∉{ }v та x∈μ( t ), то:
якщо α|– ( ,vS x t∃ Φ )∈Нα, то
α|– ( , )vxS t∃ Φ ∈Нα ;
якщо α–| ( ,vS x t∃ Φ )∈Нα, то
α–| ( , )vxS t∃ Φ ∈Нα .
HS∃∃. Якщо х∈{ }v або x∉μ( t ), то
для деякого тотально неістотного у∈Wα
такого, що ( ( , ))vy ndn S x t∉ ∃ Φ , маємо:
якщо α|– ( ,vS x t∃ Φ )∈Нα, то
α|–
, ( , , ' )v xyS t y∃ Φ ∈Нα ;
якщо α–| ( ,vS x t∃ Φ )∈Нα, то
α–|
, ( , , ' )v xyS t y∃ Φ ∈Нα .
HS . Якщо α|– ( ,vS Φ )t ∈Нα, то
α|– ( , )vS tΦ ∈Нα ;
якщо α–| ( ,vS Φ )t ∈Нα, то
α–| ( , )vS tΦ ∈Нα .
H∃. Якщо α|–∃xΦ∈Нα, то існує t∈Trα
таке, що α|– ( , )xS tΦ ∈Нα ;
якщо α–|∃xΦ∈Нα, то для всіх t∈Trα
маємо α–| ( , )xS tΦ ∈Нα .
HERf. Кожна формула вигляду
|– t = t, де t∈Trα, належить до Нα .
HESm. Якщо α|– t = s∈Нα, то
α|– s = t∈Нα .
HETr. Якщо α|– t = s∈Нα тa
α|– s = r∈Нα, то |– t = r∈Нα .
HЕPr. Нехай ξ – t=s-варіанта при-
мітивної формули ϕ.
Якщо α|– t = s∈Нα та α|–ϕ∈Нα, то
α|–ξ∈Нα ;
якщо α|– t = s∈Нα та α–|ϕ∈Нα, то
α–|ξ∈Нα .
У випадку загальних ТМЛ додаємо:
H . Якщо α|– Φ∈Нα, то β|–Φ∈Нβ
для всіх станів β∈S таких, що α>β;
якщо α–| Φ∈Нα, то β–|Φ∈Нβ для
деякого стану β∈S такого, що α>β.
У випадку темпоральних КНМЛ до-
даємо:
H ↑. Якщо α|– ↑Φ∈Нα, то
β|–Φ∈Нβ для всіх β∈S таких, що α>β;
якщо α–| ↑Φ∈Нα, то β–|Φ∈Нβ для
деякого β∈S такого, що α>β.
H ↓. Якщо α|– ↓Φ∈Нα, то
β|–Φ∈Нβ для всіх β∈S таких, що β>α;
якщо α–| ↓Φ∈Нα, то β–|Φ∈Нβ для
Теоретичні та методологічні основи програмування
24
деякого β∈S такого, що β>α.
Процедура побудови секвенційного
дерева може завершуватися або не завер-
шуватися.
Якщо процедура завершена пози-
тивно, то маємо замкнене дерево. Якщо
процедура завершена негативно або не за-
вершується, то маємо скінченне чи не-
скінченне незамкнене дерево. Тоді в дереві
існує скінченний або нескінченний незамк-
нений шлях. Кожна з формул початкової
секвенції зустрінеться на цьому шляху і ста-
не доступною.
Теорема 3. Нехай ℘ – незамкнений
шлях в секвенційному дереві, Нα – мно-
жина всіх специфікованих α|– чи α–| формул
секвенцій цього шляху, де α∈S, M – схема
моделі світу. Тоді НM = ({Нα | α∈S}, M) –
система модельних множин.
Для переходу від нижчої вершини
шляху до вищої використовується одна з
базових секвенційних форм. Переходи
згідно таких форм точно відповідають
пунктам визначення системи модельних
множин. Допоміжні специфіковані фор-
мули (їхній префікс містить символ ∗) для
модельних множин не беремо до уваги.
Кожна непримітивна формула, що зустрі-
чається на шляху ℘, рано чи пізно буде
розкладена згідно відповідної секвенційної
форми. Всі секвенції шляху ℘ незамкнені,
тому виконується пункт HС визначення
системи модельних множин.
Теорема доведена.
Теорема 4. Нехай НM – система
модельних множин, W – множина імен,
відповідних до ДНС-дублів імен формул
НM. Тоді існують TМС M = (S, R, А, І) та
функція δ∈VA з im(δ) = W такі:
1) α|–Φ∈Нα ⇒ Φα(δα) = Т;
2) α–|Φ∈Нα ⇒ Φα(δα) = F.
Доводимо для випадку загальних
ТМЛ функціонально-екваційного рівня.
Для темпоральних КНМЛ доведення ана-
логічне, з тією лише відмінністю, що за-
мість двох пунктів, пов’язаних з ↑, дода-
ємо чотири пункти, пов’язані з ↑ та ↓.
Відмінності між ТМС із сильною та
загальною умовами визначеності на станах
[7, 8] не впливають на доведення тео-
реми 4 і подальше доведення теореми 5.
Водночас для пронесення суперпозицій
через модальні композиції необхідно обме-
жити клас ТМС умовою функціональної
стабільності [8].
Нехай Wα – множина імен, відпо-
відних до ДНС-дублів імен формул мно-
жини Нα, Dnα – множина ДНС-дублів імен
усіх формул Нα, Trα = {t0, t1, ..., tn, …} –
множина нормальних термів, побудованих із
ФНС та елементів Dnα. Зрозуміло, що
Dnα = {'v | v∈Wα} ⊆ Trα. Тоді отримуємо
S
W Wα
α∈
= U ,
S
Dn Dnα
α∈
= U ,
S
Tr Trα
α∈
= U .
Рівність індукує на Trα відношення
еквівалентності: t ∼α s ⇔ α|– t = s∈Нα.
Задамо Aα = α
α~
Tr – фактор-
множину Trα за відношенням ~α.
Позначимо [t]α клас еквівалентності
з представником t.
Тепер задамо δα = [va['v]α | v∈Wα].
Нехай Wα = {v0, …, vn, … }, причому
кожне 'vj – це tkj .
Тоді δα= [v0a[tk0]α, …, vja[tkj]α, …].
Позначимо [ti]α як aі.
Визначимо fα так, щоб виконувалась
умова (ti)α(δα) = aі для всіх ti∈Trα.
Нехай tm = 'х. Тоді
(tm)α(δα) = ('х)α(δα) = ['x]α = [tm]α = am.
Нехай tm = f. Тоді задаємо
fα(δα) = (tm)α(δα) = am.
Нехай . Тоді маємо 1,...,
1...nv v
m nt S ft t=
(tm)α(δα) =
= fα(δα∇v1a(tj1)α(δα)∇…∇vna(tjn)α(δα)) = am.
Проте (tj1)α(δ) = аj1, …, (tjn)α(δ) = аjn.
Тому покладемо
fα(δα∇v1aaj1∇…∇vnaajn) = am.
Визначимо тепер рα, ураховуючи,
що (ti)α(δα) = ai.
Якщо α|–р∈Нα, то рα(δα) = Т.
Якщо α–|р∈Нα, то рα(δα) = F.
Якщо α|– 1
1
,..., ...n
n
v v
j jS pt t ∈Нα, то
рα(δα∇v1aaj1∇…∇vnaajn) = Т.
Якщо α–| 1
1
,..., ...n
n
v v
j jS pt t ∈Нα, то
рα(δα∇v1aaj1∇…∇vnaajn) = F.
Теоретичні та методологічні основи програмування
25
Для всіх інших d∈ значення fWA α
α α та
рα задаємо довільно, враховуючи еквітон-
ність та обмеження щодо неістотності імен:
для всіх d, h∈ із умови d║-μ(f) =
= h║-μ(f) випливає f
WA α
α
α(d) = fα(h) та з умови
d║-μ(p) = h║-μ(p) випливає рα(d) = рα(h).
Так визначені значення fα та рα про-
довжимо за еквітонністю, враховуючи умо-
ви неістотності імен, на відповідні h∈WAα.
Доведення тверджень 1) та 2) даної
теореми ведемо індукцією за складністю
формули згідно з побудовою НM.
Для примітивних формул твер-
дження 1) та 2) випливають з визначення
значень базових функцій і предикатів. При
цьому предикати на станах α, що є значен-
нями таких формул, еквітонні та тотальні
на відповідних . WA α
α
HN. Нехай Φ – елементарна
формула, Ψ – примітивна формула, отрима-
на з Φ нормалізацією. Якщо Ψα еквітонний
та тотальний на , то ΦWA α
α α еквітонний та
тотальний на , причому ΦWA α
α α(δα) = Ψα(δα).
Нехай α|–Φ∈Нα. За визначенням НM
маємо α|–Ψ∈Нα. За припущенням індукції
Ψα(δα) = Т, звідки Φα(δα) = Т.
Нехай α–|Φ∈Нα. За визначенням НM
маємо α–|Ψ∈Нα. За припущенням індукції
Ψα(δα) = F, звідки Φα(δα) = F.
HNΦ. Нехай α|–
, ( , , )x vS sΦ t ∈Нα та
у∈μ(Φ). За визначенням НM тоді
α|– ( , )vS tΦ ∈Нα За припущенням індукції
( ( , ))vS tΦ α(δα) = Т, звідки отримуємо
,( ( , , )x vS s tΦ ) α(δα) = Т.
Нехай α–|
, ( , , )x vS sΦ t ∈Нα та у∈μ(Φ).
За визначенням НM α–| ( , )vS tΦ ∈Нα. За
припущенням індукції ( ( , ))vS tΦ α(δα) = F,
звідки отримуємо ,( ( , , )x vS s tΦ ) α(δα) = F.
HΦ. Нехай α|–
, ( , ' , )x vS xΦ t ∈Нα. За
визначенням НM маємо α|– ( , )vS tΦ ∈Нα. За
припущенням індукції ( ( , ))vS tΦ α(δα) = Т,
тому ,( ( , ' ,x vS xΦ ))t α(δα) = Т.
Нехай α–|
, ( , ' , )x vS xΦ t ∈Нα. За ви-
значенням НM маємо α–| ( , )vS tΦ ∈Нα. За
припущенням індукції ( ( , ))vS tΦ α(δα) = F,
тому ,( ( , ' ,x vS xΦ ))t α(δα) = F.
H¬. Нехай α|–¬Φ∈Нα. За визначен-
ням НM маємо α–|Φ∈Нα. За припущенням
індукції Φα(δα) = F, звідки (¬Φ)α(δα) = Т.
Нехай α–|¬Φ∈Нα. За визначенням
НM маємо α|–Φ∈Нα. За припущенням ін-
дукції Φα(δα) = Т, звідки (¬Φ)α(δα) = F.
H∨. Нехай α|–Φ∨Ψ∈Нα. За визна-
ченням НM маємо α|–Φ∈Н або α|–Ψ∈Н. За
припущенням індукції Φα(δα) = Т або
Ψα(δα) = Т, звідки (Φ∨Ψ)α(δα) = Т.
Нехай α–|Φ∨Ψ∈Нα. За визначенням
НM маємо α–|Φ∈Нα та α–|Ψ∈Нα. За припу-
щенням індукції Φα(δα) = F та Ψα(δα) = F,
звідки (Φ∨Ψ)α(δα) = F.
HSΦ. Позначимо Ξ та Ψ формули
, ,( ( , , ), ,u x x vS S r s t wΦ ) та
, , ,
1( , , ( , , ),...,u x v u xS t S r t wΦ
, , ,
1( , , ), ( , , ),..., ( , , )).u x u x u x
k mS r t w S s t w S s t w
Нехай α|–Ξ∈Нα. За визначенням НM
маємо α|–Ψ∈Нα. За припущенням індукції
тоді Ψα(δα) = Т, звідки Ξα(δα) = Т.
Нехай α–|Ξ∈Нα. За визначенням НM
маємо α–|Ψ∈Нα. За припущенням індукції
тоді Ψα(δα) = F, звідки Ξα(δα) = F.
HS¬. Нехай α|– ( ,xS ¬Φ )t ∈Нα. За
визначенням НM тоді α|– ( , )xS t¬ Φ ∈Нα. За
припущенням індукції ( ( ,xS t¬ Φ )) α(δα) = Т,
звідки ( ( , )xS ¬Φ )t α(δα) = Т.
Нехай α–| ( ,xS ¬Φ )t ∈Нα. За визна-
ченням НM тоді α–| ( , )xS t¬ Φ ∈Нα. За при-
пущенням індукції ( ( ,xS t¬ Φ )) α(δα) = F,
звідки ( ( , )xS t¬Φ ) α(δα) = F.
HS∨. Нехай α|– ( ,xS Φ∨Ψ )t ∈Нα. За
визначенням НM α|– ( , ) ( , )x xS t S tΦ ∨ Ψ ∈Нα.
За припущенням індукції отримуємо
( ( , ) ( , )x xS t S tΦ ∨ Ψ ) α(δα) = Т, звідки
( ( , )xS Φ∨Ψ )t α(δα) = Т.
Теоретичні та методологічні основи програмування
26
Нехай α–| ( ,xS Φ∨Ψ )t ∈Нα. За ви-
значенням НM α–| ( , ) ( , )x xS t S tΦ ∨ Ψ ∈Нα.
За припущенням індукції отримуємо
( ( , ) ( , ))x xS t S tΦ ∨ Ψ α(δα) = F, звідки
( ( , )xS Φ∨Ψ )t α(δα) = F.
HSE. Нехай α|– ( ,vS r s t= )∈Нα. За
визначенням НM α|– ( , ) ( , )v vS r t S s t= ∈Нα.
За припущенням індукції отримуємо
( ( , ) ( , ))v vS r t S s t= α(δα) = Т, звідки маємо
( ( , ))vS r s t= α(δα) = Т.
Нехай α–| ( ,vS r s t= )∈Нα. За визна-
ченням НM маємо α–| ( , ) ( , )v vS r t S s t= ∈Нα.
За припущенням індукції отримуємо
( ( , ) ( , ))v vS r t S s t= α(δα) = F, звідки маємо
( ( , ))vS r s t= α(δα) = F.
HS∃. Нехай α|– ( ,vS x t∃ Φ )∈Нα,
причому х∉{ }v та x∈μ( t ). За визначенням
НM маємо α|– ( , )vxS t∃ Φ ∈Нα . За припу-
щенням індукції ( ( ,v ))xS t∃ Φ α(δα) = Т,
звідки ( ( , ))vS x t∃ Φ α(δα) = Т.
Нехай α–| ( ,S x t∃ Φ )v ∈Нα, причому
х∉{ та x∈μ(}v t ). За визначенням НM
маємо α–| ( , )vxS t∃ Φ ∈Нα . За припущенням
індукції ( ( , ))vxS t∃ Φ α(δα) = F, звідки
( ( , )S x t∃ Φ )v
α(δα) = F.
HS∃∃. Нехай α|– ( ,S x t∃ Φ )v ∈Нα,
причому х∈{ або x∉μ(}v t ). За визна-
ченням НM маємо α|–
, ( , , ' )yS t y∃ Φv x ∈Нα
для деякого тотально неістотного у∈Wα
такого: ( ( , )y n )vS x t∃ Φdn∉ . За припущен-
ням індукції , ))v x( ( , , 'yS t y∃ Φ α(δα) = Т,
звідки ( ( , ))S x tv ∃ Φ α(δα) = Т.
Нехай α–| ( , )vS x t∃ Φ ∈Нα, причому
х∈{ або x∉μ(
HS . Нехай α|– ( ,vS Φ )t ∈Нα. За ви-
значенням НM α|– ( , )vS tΦ ∈Нα. За припу-
щенням індукції ( ( , )vS tΦ ) α(δα) = Т,
звідки ( ( , ))vS tΦ α(δα) = Т.
Нехай α–| ( ,vS Φ )t ∈Нα. За визна-
ченням НM α–| ( , )vS tΦ ∈Нα. За припущен-
ням індукції ( ( , )vS tΦ ) α(δα) = F, звідки
( ( , ))vS tΦ α(δα) = F.
H∃. Нехай α|–∃хΦ∈Нα. За визна-
ченням НM тоді існує t∈Trα таке, що
α|– ( , )xS tΦ ∈Нα . За припущенням індукції
( ( , ))xS tΦ α(δα) = Т, тому Φα(δα∇хatα(δα)) = Т.
Для а = tα(δα) тоді маємо Φα(δα∇хaа) = Т,
звідки (∃хΦ)α(δα) = Т.
Нехай α–|∃хΦ∈Нα. За визначенням
НM для всіх t∈Trα тоді α–| ( , )xS Φ t ∈Нα . За
припущенням індукції ( ( , ))xS tΦ α(δα) = F
для всіх t∈Trα. Звідси Φα(δα∇хatα(δα)) = F
для всіх t∈Trα. Однак кожне аі∈Аα – це
(ti)α(δα) для відповідного tі∈Trα. Отже,
Φα(δα∇хab) = F для всіх b∈Аα, звідки
дістаємо (∃хΦ)α(δα) = F.
Із побудови НM випливає: якщо
предикат (предикати), який є значенням
простішої формули (права частина відпо-
відних пунктів визначення Нα), еквітонний
та тотальний на WA α
α , то предикат, який є
значенням формули, утвореної відповід-
ною композицією (ліва частина пунктів
визначення Нα), теж еквітонний та тоталь-
ний на WA α
α . Це гарантує еквітонність усіх
предикатів Φα, якщо такими є базові пре-
дикати на станах.
Доведення для пп. HERf – HЕPr ви-
значення модельної множини стану випли-
ває із AxRf та властивостей ESm, ETr, EPr
відношення |= . }v t ). За визначенням НM
маємо α–|
H . Нехай α–| Φ∈Нα. За визна-
ченням НM маємо β–|Φ∈Нβ для деякого
стану β такого, що α
, , ' )v xyS y∃ Φ( , t ∈Нα для деякого
тотально неістотного у∈Wα такого:
( ( , ))vy nd∉
>β. За припущенням
індукції Φβ(δβ) = F, причому Φβ еквітонний
та тотальний на WA β
β . При побудові сек-
венційного дерева стан β вводиться засто-
n S x t∃ Φ . За припущенням
індукції ,( (v xyS∃ Φ, , ' ))t y α(δα) = F, звідки
( (vS x∃ Φ, ))t α(δα) = F.
Теоретичні та методологічні основи програмування
27
суванням форми −| до формули Φ в
стані α, на цей момент “поточні” значення
W0α, W0β та A0α, A0β множин Wα, Wβ та Aα,
Aβ рівні: W0α = W0β та A0α = A0β; в по-
дальшому ці значення можуть тільки роз-
ширюватися. Звідси δ0α = δ0β. Але δ0β ⊆ δβ ,
δ0α ⊆ δα , тому прийняте на δ0α = δ0β
значення предиката Φβ не зміниться на δα
та на δβ. Отже, якщо Φβ(δβ) = F, то
Φβ(δβ) = F. Звідси ( Φ)α(δα) = F, причому
( Φ)α еквітонний та тотальний на WA α
α .
Нехай α|– Φ∈Нα. За визначенням
НM маємо β|–Φ∈Нβ для всіх станів β таких,
що α>β. За припущенням індукції
Φβ(δβ) = Т для всіх β таких, що α>β, причо-
му такі Φβ еквітонні та тотальні на
WA β
β .
Аналогічно попередньому випадку переко-
нуємось, що тоді Φβ(δα) = Т для всіх β та-
ких, що α>β. Отже, ( Φ)α(δα) = T, причому
( Φ)α еквітонний та тотальний на WA α
α .
Для випадку темпоральних КНМЛ
замість останніх двох випадків маємо:
H ↑. Нехай α|– ↑Φ∈Нα. За визна-
ченням НM маємо β|–Φ∈Нβ для всіх станів
β таких, що α>β. За припущенням індукції
Φβ(δβ) = Т для всіх станів β таких, що α>β,
причому такі Φβ еквітонні та тотальні на
WA β
β . Звідси аналогічно випадку загальних
ТМЛ отримуємо ( ↑Φ)α(δα) = T, причому
( ↑Φ)α еквітонний та тотальний на WA α
α .
Нехай α–| ↑Φ∈Нα. За визначенням
НM маємо β–|Φ∈Нβ для деякого β такого,
що α>β, причому Φβ еквітонний та тоталь-
ний на WA β
β . За припущенням індукції
Φβ(δβ) = F. Звідси аналогічно отримуємо
( ↑Φ)α(δα) = F, причому ( ↑Φ)α еквітон-
ний та тотальний на WA α
α .
H ↓. Нехай α|– ↓Φ∈Нα. За визна-
ченням НM маємо β|–Φ∈Нβ для всіх станів
β таких, що β>α, причому такі Φβ еквітон-
ні та тотальні на WA β
β . За припущенням
індукції Φβ(δβ) = Т для всіх станів β таких,
що β>α. Звідси ( ↓Φ)α(δα) = T, причому
( ↓Φ)α еквітонний та тотальний на WA α
α .
Нехай α–| ↓Φ∈Нα. За визначенням
НM маємо β–|Φ∈Нβ для деякого β такого,
що β>α, причому Φβ еквітонний та тоталь-
ний на WA β
β . За припущенням індукції
Φβ(δβ) = F. Звідси ( ↓Φ)α(δα) = F, причому
( ↓Φ)α еквітонний та тотальний на WA α
α .
На основі теорем 3 і 4 отримуємо тео-
рему повноти секвенційних числень загаль-
них ТМЛ та темпоральних КНМЛ функціо-
нально-екваційного рівня.
Теорема 5. Нехай Γ |= Δ. Тоді сек-
венція |–Γ–|Δ вивідна.
Припустимо супротивне: Γ |= Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то в секвенційному дереві для Σ існує не-
замкнений шлях. Згідно теореми 3 маємо,
що НM = ({Нα | α∈S}, M) – система модель-
них множин (тут Нα – множина всіх специ-
фікованих α|– чи α–| формул секвенцій цьо-
го шляху, де α∈S, M – схема моделі світу).
Згідно теореми 4 існують M = (S, R, А, І)
та δ∈VA такі: з умови α|–Φ∈Нα випливає
Φα(δα) = Т та з умови α–|Φ∈Нα випливає
Φα(δα) = F. Зокрема, це справджується для
формул секвенції |–Γ–|Δ, тому для всіх Φα∈Γ
маємо Φα(δα) = Т та для всіх Ψβ∈Δ маємо
Ψβ(δβ) = F. Це заперечує Γ |=M Δ, тому не-
вірно, що Γ |= Δ. Отже, припущення про
невивідність |–Γ–|Δ невірне, що й доводить
теорему 5.
Висновки
На основі властивостей відношення
логічного наслідку для множин специфіко-
ваних станами формул збудовано числення
секвенційного типу для загальних транзи-
ційних та темпоральних композиційно-но-
мінативних модальних логік функціональ-
но-екваційного рівня. Досліджено власти-
вості побудованих числень. Для цих
числень доведено теореми коректності та
повноти.
1. Нікітченко М.С., Шкільняк С.С. Компози-
ційно-номінативні модальні логіки //
Проблемы программирования. – 2002. –
№ 1–2. – С. 27–33.
Теоретичні та методологічні основи програмування
28
2. Фейс Р. Модальная логика. – M.: Наука,
1974. – 520 с.
3. Семантика модальных и интенсиональных
логик. – M.: Прогресс, 1981. – 494 с.
4. Нікітченко М.С., Шкільняк С.С. Матема-
тична логіка та теорія алгоритмів. – К.:
ВПЦ «Київський університет», 2008. – 528 с.
5. Шкільняк О.С. Композиційно-номінативні
модальні та темпоральні логіки: семан-
тичні властивості, секвенційні числення //
Наукові записки НаУКМА. Том 86. Серія:
Комп’ютерні науки. – 2008. – C. 25–34.
6. Шкільняк О.С. Секвенційні числення ком-
позиційно-номінативних модальних і тем-
поральних логік // Наукові записки
НаУКМА. Том 99. Серія: Комп’ютерні
науки. – 2009. – C. 37–44.
7. Шкільняк О.С. Семантичні властивості
композиційно-номінативних модальних
логік // Проблеми програмування. – 2009. –
№ 4. – C. 11–24.
8. Шкільняк О.С. Композиційно-номінативні
модальні логіки функціонально-еквацій-
ного рівня // Проблеми програмування. –
2010. – № 2–3 – C. 42–47.
Отримано 14.10.2010
Про автора:
Шкільняк Оксана Степанівна,
асистент кафедри інформаційних
систем.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01601, Київ,
вул. Володимирська, 60.
Тел.: (044) 259 0511, (044) 522 0640 (д)
e-mail: me.oksana@gmail.com
mailto:me.oksana@gmail.com
|