Sequent calculi of composition nominative modal logics of functional-equational level
Composition nominative modal and temporal logics of functional-equational level are studied in this paper. Basing on properties of relation of logical consequence for sets of formulas, sequent calculi are constructed for general and temporal logics of such level. The soundness and completeness theor...
Збережено в:
| Дата: | 2025 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2025
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/794 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-794 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/d9/803b3b0ed8ad4cb704e0f43fed05d3d9.pdf |
| spelling |
pp_isofts_kiev_ua-article-7942025-09-02T15:47:58Z Sequent calculi of composition nominative modal logics of functional-equational level Секвенциальные исчисления композиционно-номинативных модальных логик функционально-эквационального уровня Shkilnyak, O.S. UDC 510.69 УДК 510.69 Composition nominative modal and temporal logics of functional-equational level are studied in this paper. Basing on properties of relation of logical consequence for sets of formulas, sequent calculi are constructed for general and temporal logics of such level. The soundness and completeness theorems for these calculi are proved.Problems in programming 2011; 1: 17-28 Исследуются композиционно-номинативные модальные и темпоральные логики функционально-эквационального уровня. На основе свойств отношения логического следствия для множеств формул построены исчисления секвенциального типа для общих и темпоральных композиционно-номинативных модальных логик такого уровня. Для построенных исчислений доказаны теоремы корректности и полноты. Problems in programming 2011; 1: 17-28 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-08-28 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/794 PROBLEMS IN PROGRAMMING; No 1 (2011); 17-28 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2011); 17-28 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2011); 17-28 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/794/846 Copyright (c) 2025 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2025-09-02T15:47:58Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
UDC 510.69 |
| spellingShingle |
UDC 510.69 Shkilnyak, O.S. Sequent calculi of composition nominative modal logics of functional-equational level |
| topic_facet |
UDC 510.69 УДК 510.69 |
| format |
Article |
| author |
Shkilnyak, O.S. |
| author_facet |
Shkilnyak, O.S. |
| author_sort |
Shkilnyak, O.S. |
| title |
Sequent calculi of composition nominative modal logics of functional-equational level |
| title_short |
Sequent calculi of composition nominative modal logics of functional-equational level |
| title_full |
Sequent calculi of composition nominative modal logics of functional-equational level |
| title_fullStr |
Sequent calculi of composition nominative modal logics of functional-equational level |
| title_full_unstemmed |
Sequent calculi of composition nominative modal logics of functional-equational level |
| title_sort |
sequent calculi of composition nominative modal logics of functional-equational level |
| title_alt |
Секвенциальные исчисления композиционно-номинативных модальных логик функционально-эквационального уровня |
| description |
Composition nominative modal and temporal logics of functional-equational level are studied in this paper. Basing on properties of relation of logical consequence for sets of formulas, sequent calculi are constructed for general and temporal logics of such level. The soundness and completeness theorems for these calculi are proved.Problems in programming 2011; 1: 17-28 |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2025 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/794 |
| work_keys_str_mv |
AT shkilnyakos sequentcalculiofcompositionnominativemodallogicsoffunctionalequationallevel AT shkilnyakos sekvencialʹnyeisčisleniâkompozicionnonominativnyhmodalʹnyhlogikfunkcionalʹnoékvacionalʹnogourovnâ |
| first_indexed |
2025-09-17T09:23:00Z |
| last_indexed |
2025-09-17T09:23:00Z |
| _version_ |
1850413151485427712 |
| 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
|