Compositional-nominative modal logics of the functional-equational level
Composition nominative modal and temporal logics of functional-equational level are introduced in this paper. Transition and temporal modal systems are specified for such logics, and their semantic properties are investigated. Prombles in programming 2010; 2-3: 42-47
Gespeichert in:
| Datum: | 2026 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainisch |
| Veröffentlicht: |
PROBLEMS IN PROGRAMMING
2026
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/863 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Institution
Problems in programming| _version_ | 1866844886768025600 |
|---|---|
| author | Shkilniak, O.S. |
| author_facet | Shkilniak, O.S. |
| author_institution_txt_mv | [
{
"author": "O.S. Shkilniak",
"institution": "Kiev Taras Shevchenko National University"
}
] |
| author_sort | Shkilniak, O.S. |
| baseUrl_str | https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| collection | OJS |
| datestamp_date | 2026-06-01T06:02:58Z |
| description | Composition nominative modal and temporal logics of functional-equational level are introduced in this paper. Transition and temporal modal systems are specified for such logics, and their semantic properties are investigated. Prombles in programming 2010; 2-3: 42-47 |
| first_indexed | 2026-06-02T01:00:20Z |
| format | Article |
| fulltext |
Теоретичні та методологічні основи програмування
© О.С. Шкільняк, 2010
42 ISSN 1727-4907. Проблеми програмування. 2010. № 2–3. Спеціальний випуск
УДК 681.3.06
КОМПОЗИЦІЙНО-НОМІНАТИВНІ МОДАЛЬНІ ЛОГІКИ
ФУНКЦІОНАЛЬНО-ЕКВАЦІЙНОГО РІВНЯ
О.С. Шкільняк
Київський національний університет імені Тараса Шевченка
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 259 0511
e-mail: me.oksana@gmail.com
Пропонуються композиційно-номінативні модальні та темпоральні логіки функціонально-екваційного рівня. Для цих логік
визначаються транзиційні та темпоральні модальні системи, досліджуються їх семантичні властивості.
Composition nominative modal and temporal logics of functional-equational level are introduced in this paper. Transition and temporal
modal systems are specified for such logics, and their semantic properties are investigated.
Модальні та темпоральні логіки є потужним і ефективним засобом специфікації програм, моделювання
складних динамічних систем. Композиційно-номінативні модальні логіки (КНМЛ) [1] синтезують можливості
модальних логік та композиційно-номінативних логік квазіарних предикатів. Центральним поняттям КНМЛ є
поняття композиційно-номінативної модальної системи (КНМС) [1]. На базі інтегрованого інтенсіонально-
екстенсіонального підходу [2] в роботі [3] запропоноване спеціальне уточнення поняття КНМС для логік
номінативних рівнів. Семантичні та синтаксичні властивості транзиційних та темпоральних КНМЛ
реномінативного, кванторного та кванторно-екваційного рівнів досліджуються в [3–6], зокрема, для таких логік
пропонуються числення секвенційного типу.
В даній роботі дослідження семантичних властивостей КНМЛ продовжується на функціонально-
екваційному рівні. Для таких логік розглядається спеціальне уточнення поняття композиційно-номінативної
модальної системи, визначаються і досліджуються транзиційні та темпоральні КНМС функціонально-
екваційного рівня.
Поняття, які тут не визначаються, будемо тлумачити в сенсі робіт [1, 3, 6].
1. КНМС функціонально-екваційного рівня
На функціонально-екваційному рівні за допомогою явно заданих (базових) функцій маємо розширені
можливості формування нових аргументів для функцій і предикатів та можливість ототожнювати й розрізняти
предметні значення, вироблені функціями. Це дає змогу ввести [1] композиції суперпозиції vS та рівності =.
Виділення спеціальних функцій деномінації (розіменування) 'v для кожного vV дозволяє
промоделювати композицію реномінації за допомогою композиції суперпозиції: для довільної gFn
Pr маємо
1
1
,...,
,..., ( )n
n
v v
x xR g = 1 ,..., nv v
S (g, 'х1,..., 'хn).
Спеціальні предикати рівності =xy можна промоделювати за допомогою деномінаційних функцій та
композиції рівності. Справді, для кожного d
V
А маємо =xy(d) = =('x, 'y)(d).
Як і для випадку КНЛ квазіарних предикатів [1], до базових загальнологічних композицій КНМЛ
функціонально-екваційного рівня відносимо , , x, vS , =.
Спеціальні функції деномінації 'v можна трактувати як спеціальні параметризовані за іменами 0-арні
композиції.
Уточнимо поняття КНМС на функціонально-екваційному рівні.
Мова КНМЛ функціонально-екваційного рівня описується наступним чином.
Алфавіт мови складається з множини V предметних імен, множин Dns, Fns, Ps відповідно деномінаційних,
функціональних, предикатних символів, а також множини символів базових композицій , , x, vS , = і множини
Мs символів базових модальних композицій. Множину FпsDns позначимо Fs.
Множини термів Тr і формул Fт формул мови КНМЛ функціонально-екваційного рівня визначаємо
індуктивно.
Т1. Кожний ФНС та кожний ДНС є термом. Такі терми назвемо атомарними.
Т2. Нехай t, t1,..., tn – терми. Тоді 1 ,..., nv v
S t t1...tn – терм.
Ф1. Кожний ПС є формулою. Такі формули назвемо атомарними.
Ф2. Нехай t та s – терми. Тоді =ts – формулa
Теоретичні та методологічні основи програмування
43
Ф3. Нехай – формулa, t1,..., tn – терми. Тоді 1 ,..., nv v
S t1...tn – формулa.
Ф4. Нехай – формула. Тоді – формула.
Ф5. Нехай та – формули. Тоді та – формули.
Ф6. Нехай – формула. Тоді x – формула.
Ф7. Нехай – формула, – символ базової модальної композиції. Тодi – формула.
Для кожного gFsPs множина синтетично неістотних предметних імен [1] визначаємо за допомогою
тотальної функції : FsPs2
V
. При цьому для кожного 'xDns покладемо ('x) = V \{x}. Продовжимо таку
функцію до : Tr Fr2
V
так:
– ( 1 ,..., nv v
S t t1...tn) = ((t){v1,...,vn})
{ | ( )}
( )
i
i
i v t
t
;
– ( 1 ,..., nv v
S t1...tn) = ((){v1,...,vn})
{ | ( )}
( )
i
i
i v t
t
;
– (=ts) = (t)(s);
– () = ();
– () = ()();
– (x) = (){x};
– () = ().
Пару (FsPs, ) назвемо сигнатурою синтетичної неістотності функціонально-екваційної КНМС.
Символи модальних композицій утворюють модальну сигнатуру функціонально-екваційної КНМС.
Для уточнення Dпs задамо відображення інтерпретації атомарних термів та формул на світах
I : FsРs S FnPr. При цьому для кожних fFs та pРs маємо I(f, ) Fn та I(p, ) Pr, I('v) = 'v для
кожного 'vDns.
Символи базових композицій , , x, vS , = та символи базових модальних композицій інтерпретуються
як відповідні композиції.
Відображення I продовжимо до Jт : ТrFт S FnPr.
IT1) Jт(f, ) = I(f, ) для кожного fFs;
IT2) Jт( 1 ,..., nv v
S t t1...tn, ) = 1 ,..., nv v
S (Jт(t, ), Jт(t1, ), ..., Jт(tn, )).
I1) Jт(p, ) = I(p, ) для кожного pPs;
I2) J(=ts ) = =(J(t ), J(s )).
I3) Jт( 1 ,..., nv v
S t1...tn, ) = 1 ,..., nv v
S (Jт(, ), Jт(t1, ), ..., Jт(tn, )).
I4) Jт(, ) = (Jт(, ));
I5) Jт(, ) = (Jт(, ), Jт(, ));
I6) Jт(x, )(d) =
, якщо ( , )( ) для деякого ,
, якщо ( , )( ) для всіх ,
невизначене в усіх інших випадках.
T Jm d x a T a A
F Jm d x a F a A
I7) Значення Jт(, )(d) визначається значеннями Jт(, )(d) для певних станів таких, що та ці
перебувають у відповідних пов'язаних із відношеннях з R.
При цьому виконуються умови Jт(t, ) Fn та Jт(, ) Pr.
Предикат Jт(t, ), який є значенням терма tу стані , будемо позначати t.
Предикат Jт(, ), який є значенням формули у стані , будемо позначати .
Таким чином, поняття КНМС функціонально-екваційного рівня можна уточнити як об'єкт вигляду
M = ((S, R, FnPr, C), ТrFт, Jт).
Поняття істинної в стані , істинної в КНМС формули та всюди істинної формули для КНМС
функціонально-екваційного рівня аналогічні відповідним визначенням для КНМС кванторного та кванторно-
екваційного рівнів [3, 6].
Семантичні властивості КНМС функціонально-екваційного рівня, не пов’язані з модальностями,
успадковують властивості КНМС кванторного та кванторно-екваційного рівнів.
До властивостей власне функціонально-екваційного рівня належать в першу чергу загальнологічні
властивості, притаманні як КНМЛ, так і КНЛ квазіарних предикатів. Це пов'язані з суперпозиціями властивості
ZN, Z, S, S, SS, S, S та пов'язані з суперпозиціями й рівністю властивості ZT, DD, DS, ZNT, SST, SE
(див. [1]). До таких властивостей належать також специфічні властивості рівності:
Rf) рефлексивність: |= t = t;
Sm) cиметричність: |= s = t t = s;
Tr) транзитивність: |= s = t t = h s = h;
Зазначені властивості справджуються для кожного конкретного стану кожної КНМС функціонально-
екваційного рівня,
Терм нормальний [1], якщо всі його символи суперпозиції застосовані тільки до ФНС, згорнуті неістотні
імена й виконані спрощення на основі SST, ZNT, ZT, DS, DD.
Теоретичні та методологічні основи програмування
44
Атомарні формули й формули вигляду ( , )vS p t чи t = s називають [1] елементарними.
Елементарна формула примітивна [1], якщо вона атомарна, або в її символах суперпозиції згорнуті неістотні
імена та всі її терми нормальні.
Будемо писати , якщо терм є підтермом терма чи формули .
Аналогічно пишемо Ф, якщо формула є підформулою формули Ф.
Нехай t та s – нормальні [1] терми, причому |= t = s. Нехай невірно ts та невірно st.
Примітивні формули та назвемо t=s-еквівалентними, якщо при заміні в них усіх входжень t та s на
один і той же ФНС отримаємо однакові формули.
Неформально це означає, що формулу можна отримати із формули замінами деяких входжень терма t
на s і навпаки.
Якщо формули та t=s-еквівалентні, то будемо говорити, що є t=s-варіантою формули , а – t=s-
варіантою формули .
Якщо |= t = s та ts, то визначення t=s-еквівалентних примітивних формул треба модифікувати: та t=s-
еквівалентні, якщо при заміні в них усіх входжень s та t (можливо, за декілька кроків) отримаємо одну і ту ж
формулу .
Неважко переконатись, що справджується наступне твердження, яке фактично успадковане від КНЛ
квазіарних предикатів:
Теорема 1. Нехай |= t = s, нехай примітивні формули та t=s-еквівалентні. Тоді |= t = s ( ).
Звідси як наслідок отримуємо наступну властивість:
EPr) |= t = s ( ) при умові, що примітивні формули та – t =s-еквівалентні.
2. ТМС функціонально-екваційного рівня
Для транзиційних модальних систем (ТМС) [1] множина R відношень на станах світу складається з
відношень вигляду R S S.
ТМС із єдиним бінарним відношенням на станах та базовими модальними композиціями і
називають [1] загальними ТМС.
ТМС із єдиним бінарним відношенням та базовими модальними композиціями , , і
називають [1] темпоральними КНМС, а також темпоральними ТМС (ТмМС).
КНМС, в яких із (d) випливає d
V
A, називають [6] КНМС із сильною умовою визначеності на
станах. В таких КНМС при d
V
A маємо (d).
ТМС із сильною умовою визначеності називають St-ТМС.
У випадку St-ТМС модальні композиції не зберігають еквітонність, проте зберігають слабку еквітонність
(див. [6]).
Ослабимо вимогу (d) при d
V
A. Будемо тепер вважати, що умова d
V
A не є обов’язковою для
(d). Для цього при d
V
A задаємо (d) = (d
V
A).
ТМС із такою загальною умовою визначеності називають [6] Gn-ТМС.
Множину вигляду d
V
A, де d
V
A, позначаємо d.
Для Gn-ТМС справджується [6]
Теорема 2. 1. У випадку загальних Gn-ТМС композиція зберігає еквітонність.
2. У випадку темпоральних Gn-ТМС композиції та зберігають еквітонність.
Таким чином, базові композиції загальних Gn-ТМС та темпоральних Gn-ТМС зберігають еквітонність.
Розглянемо властивості функціонально-екваційних Gn-ТМС, пов’язані з модальними композиціями та
рівністю.
Твердження 1. Формула t = s
,x vS (, t, t ) =
,x vS (, s, t ) всюди істинна.
Припустимо супротивне: для деяких S та d
V
A маємо ( t = s)(d) = T та
( ,x vS (, t, t ) =
,x vS (, s, t ))(d) = F. Друга умова означає: для деякого S такого, що , маємо
( ,x vS (, t, t ) =
,x vS (, s, t ))(d) = F. Тоді отримуємо ( ,x vS (, t, t ))(d) = a, ( ,x vS (, s, t ))(d) = b для деяких
a, bA: a b. Звідси (d v ( t )(d)xt(d)) = a, (d v ( t )(d)xs(d)) = b для деяких a b. Але
(t = s)(d) = T означає (t = s)(d) = T для такого , звідки t(d) = s(d) = cA. Тоді
(d v ( t )(d)xt(d)) = (d v ( t )(d)xc) = (d v ( t )(d)xs(d)) – суперечність.
Твердження 2. Формула t = s ( ,x vS (, t, t )
,x vS (, s, t )) всюди істинна.
Припустимо супротивне: для деяких S та d
V
A маємо ( t = s)(d) = T та
((, t, t )
,x vS (, s, t ))(d) = F. Друга умова означає, що для деякого S такого, що , маємо
( ,x vS (, t, t )
,x vS (, s, t ))(d) = F. Звідси ( ,x vS (, t, t ))(d) (
,x vS (, s, t ))(d), звідки отримуємо
(d v ( t )(d)xt(d)) = a, (d v ( t )(d)xs(d)) = b для a, bBool таких, що a b.
Теоретичні та методологічні основи програмування
45
Але (t = s)(d) = T означає (t = s)(d) = T для такого , звідки маємо t(d) = s(d) = cA. Тоді
(d v ( t )(d)xt(d)) = (d v ( t )(d)xc) = (d v ( t )(d)xs(d)) – суперечність.
Семантичні властивості ТМС функціонально-екваційного рівня відрізняються від семантичних
властивостей ТМС кванторного та кванторного-екваційного рівнів.
Приклад 1. Формула t = s t = s не є всюди істинною.
Побудуємо загальну ТМС, в якій спростовується формула вигляду t = s t = s. Нехай S = {, }, де
A = A = {0, 1}. Нехай R = {}. Візьмемо ФС + та , для яких неістотні всі імена, окрім x та y. Визначимо
+([x1, y1]) = 0, ([x1, y1]) = 0, +([x1, y1) = 0, ([x1, y1]) = 1. Для всіх інших d{0, 1}
{x, y}
значення +(d), +(d), (d), (d) покладемо рівним 0. Тоді (+ = )([x1, y1]) = T. (+ = )([x1, y1]) = F,
звідки (+ = + = )([x1, y1]) = F, тому | + = + = .
Приклад 2. Формула t = s t = s не є всюди істинною.
Побудуємо загальну ТМС, в якій спростовується формула вигляду t = s t = s. Нехай S = {, }, де
A = A = {0, 1}. Нехай R = {}. Візьмемо ФС + та , для яких неістотні всі імена, окрім x та y. Визначимо
+([x1, y1]) = 0, ([x1, y1]) = 1, +([x1, y1) = 0, ([x1, y1]) = 0. Для всіх інших d{0, 1}
{x, y}
значення +(d), +(d), (d), (d) покладемо рівним 0. Тоді (+ = )([x1, y1]) = F. (+ = )([x1, y1]) = T,
звідки ( + = + = )([x1, y1]) = F, тому | + = + = .
Приклад 3. Формули вигляду xS (, t )
xS (, t ) і xS (, t )
xS (, t ) не є всюди
істинними.
Побудуємо загальну ТМС, в якій спростовується формула xS (р, f)
xS (р, f).
Нехай S = {, }, де A = A = {0, 1}, R = {}. Нехай для р та f неістотні усі імена, окрім x. Задамо
f([x0]) = 0, f([x0]) = 1, р([x1]) = T, р([x0]) = F. Для всіх інших d{0, 1}
{x}
значення f(d), f(d), р(d),
р(d) задамо довільним чином. Тоді ( xS (р, f))([x0]) = р([x0xf([x0]]) = р([x0x1]) = р([x1]) = T,
звідки маємо ( xS (р, f))([x0]) = T. Проте р([x0xf([x0]]) = р([x0x0]) = р([x0]) = F, тому
р([x0xf([x0]]) = F, звідки ( xS (р, f))([x0]) = F. Отже, ( xS (р, f)
xS (р, f))([x0]) = F.
Тепер будуємо загальну ТМС, в якій спростовується формула xS (р, f)
xS (р, f).
Нехай S = {, }, де A = A = {0, 1}, R = {}. Нехай для р та f неістотні всі імена, окрім x. Задамо
f([x0]) = 0, f([x0]) = 1, р([x1]) = F, р([x0]) = T. Для всіх інших d{0, 1}
{x}
значення f(d), f(d), р(d),
р(d) задамо довільним чином. Тоді ( xS (р, f))([x0]) = р(x0xf([x0]) = р(x0x1]) = р([x1]) = F,
звідки маємо ( xS (р, f))([x0]) = F. Проте р([x0xf([x0]]) = р([x0x0]) = р([x0]) = T, тому
р([x0xf([x0]]) = T, звідки ( xS (р, f))([x0]) = T. Отже, ( xS (р, f)
xS (р, f))([x0]) = F.
Таким чином, для ТМС функціонально-екваційного рівня вже не можна проносити символи суперпозиції
через символи модальних композицій. Це пов’язане із тим фактом, що один і той же терм, навіть один і той же
функціональний символ, на одних і тих же даних може по-різному інтерпретуватись в різних станах. Це не так
для деномінаційних символів, які мають загальнологічний статус та інтерпретуються однаково в різних станах,
в різних модальних системах. Тому символи реномінації можна [3] проносити через символи модальних
композицій, а символи суперпозиції – не можна.
Зауважимо, що подібні ефекти, пов’язані з підстановками термів замість вільних входжень предметних
імен, проявляються і для традиційних модальних логік при побудові прикладів вигляду x[t] для формул
вигляду x(x). Неважко побудувати традиційну реляційну модель, в якій спростовується формула вигляду
x(x) x[t].
Приклад 4. Нехай S = {, }, де A = {0}, A = {0, 1}, R = {}. Нехай р та f 1-арні. Задамо f(0) = 0,
f(0) = 1, р(0) = T, р(0) = T, р(1) = F. Згідно р(0) = T маємо р(0) = T, звідки, враховуючи A = {0}, маємо
(xр(x)) = T. Проте (рx[f])(0) = р(f(0)) = р(1) = F, звідки (рx[f])(0) = F, тому (xр(x)рx[f])(0) = F.
Отже, |xр(x)рx[f].
Аналогічно будуємо загальну ТМС, в якій спростовується формула вигляду x xS (, t).
Приклад 5. Нехай S = {, }, де A = {0}, A = {0, 1}, R = {}. Нехай для р та f неістотні всі імена, окрім
x. Задамо f([x0]) = 0, f([x0]) = 1, f([x1] = 1, р([x0]) = T, р([x0]) = T. р([x1) = F. Згідно р([x0]) = T
маємо р([x0]) = T, звідки, враховуючи A = {0}, маємо (xр)([x0]) = T. тому |=xр. Проте
( xS (р, f))([x0]) = р([x0xf([x0]]) = р([x0x1]) = р([x1]) = F, звідки ( xS (р, f))([x0]) = F, тому
| xS (р, t) та (xр
xS (р, f))([x0]) = F. Отримали |=xр, | xS (р, t), |xр
xS (р, t).
Таким чином, в загальному випадку виникають труднощі при побудові прикладів формул вигляду x
(а також x). Очевидним чином можна отримати приклади вигляду xS (, t), але подальше пронесення
через суперпозицію некоректне. Як бачимо, не допомагає і “безпосередня” побудова прикладів xS (, t) для
x.
Теоретичні та методологічні основи програмування
46
Зазначену неприємну особливість ТМС функціонально-екваційного рівня можна обійти ціною введення
додаткової умови збереження значень функціональних символів при русі за станами. Такі ТМС назвемо
функціонально стабільними.
ТМС M назвемо функціонально стабільною, якщо для всіх S, для всіх : , для всіх fFns, для всіх
d
V
A з умови f(d) та f(d
V
A) випливає f(d) = f(d
V
A).
Покажемо, що умова функціональної стабільності ТМС продовжується на терми.
Теорема 3. Якщо ТМС M функціонально стабільна, то для всіх S, для всіх : , для всіх Tr тa
d
V
A з умови (d) та (d
V
A) випливає (d) = (d
V
A).
Доводимо індукцією за побудовою терма .
Для ДНС твердження теореми очевидне.
Для ФНС твердження теореми – це умова функціональної стабільності.
Нехай терм t має вигляд S
x
(t, s). Для загального випадку, коли терм має вигляд 1 ,...,
1( , ,..., )nx x
nS t s s
доведення аналогічне.
Припустимо супротивне: нехай для деяких станів , таких, що , для деякого d
V
A маємо
S
x
(t, s)(d) = a та S
x
(t, s)(d
V
A) = b, причому a b.
1. Нехай s(d). Тоді S
x
(t, s)(d) = t(dxs(d)) = t(d ||–x) = a.
1.1. Якщо s(d
V
A), то
S
x
(t, s)(d
V
A) = t((d
V
A)xs(d
V
A)) = t((d
V
A)||–x) = t((d||–x)
V
A) = b.
Але t(d ||–x) = a, тому згідно припущення індукції для t тоді необхідно a = b – суперечність.
1.2. Якщо s(d
V
A) = c, то
S
x
(t, s)(d
V
A) = t((d
V
A)xc) = t((dxc)
V
A) = b
Із t(d ||–x) = a за еквітонністю маємо t(dxc) = a. Згідно припущення індукції для t тоді необхідно a = b
– суперечність.
2. Нехай s(d) = e. Тоді S
x
(t, s)(d) = t(dxs(d)) = t(dxe) = a.
2.1. Якщо s(d
V
A), то
S
x
(t, s)(d
V
A) = t((d
V
A)xs(d
V
A)) = t((d
V
A)||–x) = t((d||–x)
V
A) = b.
Але (d||–x)
V
A (dxe)
V
A, тому за еквітонністю t((dxe)
V
A) = b. Але t(dxe) = a, тому згідно
припущення індукції для t тоді необхідно a = b – суперечність.
2.2. Якщо s(d
V
A) = c, то згідно припущення індукції для s із s(d) = e отримуємо c = e. Звідси
S
x
(t, s)(d
V
A) = t((d
V
A)xe) = t((dxe)
V
A) = b
Але t(dxe) = a, тому згідно припущення індукції для t тоді необхідно a = b – суперечність.
Теорема 4. Для кожної функціонально стабільної ТМС M маємо M |=
xS (, t )
xS (, t )
та M |=
xS (, t )
xS (, t ).
Доводимо для формул вигляду S
x
(, t). Для загального випадку (див. формулювання теореми) доведення
аналогічне.
1. Показуємо M |= S
x
(, t) S
x
(, t).
Припустимо супротивне: для деяких стану та d
V
A маємо (S
x
(, t) S
x
(, t))(d) = F. Звідси
(S
x
(, t))(d) = T та (S
x
(, t))(d) = F.
Iз (S
x
(, t))(d) = F маємо (dxt(d)) = F, звідки для деякого такого, що , маємо
((dxt(d))
V
A) = F. Із (S
x
(, t))(d) = T для такого тоді S
x
(, t)(d
V
A)) = T, звідки
((d
V
A)xt(d
V
A)) = T.
1-1. Нехай t(d). Тоді ((dxt(d))
V
A) = F дає ((d||–x)
V
A) = F, звідки ((d
V
A)||–x) = F. При
t(d
V
A) тоді ((d
V
A)xt(d
V
A)) = T дає ((d
V
A)||–x) = T – суперечність. При t(d
V
A) = c із
((d
V
A)xt(d
V
A)) = T маємо ((d
V
A)xc) = T, але згідно (d
V
A)||–x) (d
V
A)xc за
еквітонністю знову маємо суперечність із ((d
V
A)||–x) = F.
1-2. Нехай t(d) = e. Із ((dxt(d))
V
A) = F тоді ((dxe)
V
A) = F ((d
V
A)xe) = F. При
t(d
V
A) тоді ((d
V
A)xt(d
V
A)) = T дає ((d
V
A)||–x) = T, звідки згідно (d
V
A)||–x) (d
V
A)xe за
еквітонністю маємо суперечність із ((d
V
A)||–x) = F. При t(d
V
A) згідно припущення індукції для t маємо
t(d
V
A) = t(d) = e, тому ((d
V
A)xt(d
V
A)) = T дає ((d
V
A)xe) = T – маємо суперечність із
((d
V
A)xe) = F.
2. Показуємо M |= S
x
(, t) S
x
(, t).
Припустимо супротивне: для деяких стану та d
V
A маємо (S
x
(, t) S
x
(, t))(d) = F. Звідси
(S
x
(, t))(d) = F та (S
x
(, t))(d) = T. Далі дослівно повторюємо доведення п.1, тільки істиннісні значення T
та F міняються місцями.
Фактично доведення теореми 4 показує, що у випадку функціонально стабільної ТМС M для довільного
стану та d
V
A маємо ( xS (, t ))(d) (
xS (, t )(d)), що дає M |= S
x
(, t) S
x
(, t).
Таким чином, умова функціональної стабільності ТМС дає змогу проносити символи суперпозиції через
символи модальних композицій.
Теоретичні та методологічні основи програмування
47
Теорема 5. Для кожної функціонально стабільної ТМС M для довільного стану та d
V
A маємо
(t = s)(d) ( t = s)(d).
Припустимо супротивне: існує функціонально стабільна ТМС M така, що для деяких та d
V
A маємо
(t = s)(d) ( t = s)(d). Розглянемо можливі два випадки:
1) (t = s)(d) = T та ( t = s)(d) = F. Перше означає, що t(d), s(d), t(d) = s(d). Із другої умови випливає,
що для деякого такого, що , маємо (t = s)(d
V
A) = F. Звідси t(d
V
A) s(d
V
A). Згідно теореми 3
маємо t(d
V
A) = t(d), s(d
V
A) = s(d), звідки в силу t(d) = s(d) отримуємо t(d
V
A) = s(d
V
A) –
суперечність;
2) (t = s)(d) = F та ( t = s)(d) = T. Перше означає, що t(d), s(d), t(d) s(d). Із другої умови випливає,
що для всіх таких, що , маємо (t = s)(d
V
A) = T. Візьмемо довільний такий стан , для нього маємо
t(d
V
A) = s(d
V
A). Але згідно теореми 3 маємо t(d
V
A) = t(d), s(d
V
A) = s(d), звідки в силу
t(d
V
A) = s(d
V
A) отримуємо t(d) = s(d) – суперечність.
Наслідок. Для функціонально стабільних ТМС маємо M |= t = s t = s.
3. Tемпоральні КНМС функціонально-екваційного рівня
Для ТмМС функціонально-екваційного рівня відповідним чином переформульовуються твердження
розділу 2. Зокрема, для таких ТмМС не можна проносити символи суперпозиції через символи модальних ком-
позицій. Тому будемо розглядати ТмМС функціонально-екваційного рівня із умовою збереження значень функ-
ціональних символів при русі за станами. Такі ТмМС назвемо функціонально стабільними. Умова функціо-
нальної стабільності вже дає змогу проносити символи суперпозиції через символи модальних композицій.
Для функціонально стабільних ТмМС справджуються аналоги теорем 3–5:
Теорема 6. Якщо ТмМС M функціонально стабільна, то для всіх S, для всіх : , для всіх Tr тa
d
V
A з умови (d) та (d
V
A) випливає (d) = (d
V
A).
Теорема 7. Для кожної функціонально стабільної ТмМС M маємо M |=
xS (, t )
xS (, t ),
M |=
xS (, t )
xS (, t ), та M |=
xS (, t )
xS (, t ), M |=
xS (, t )
xS (, t ).
Теорема 8. Для кожної функціонально стабільної ТмМС M для довільного стану та d
V
A маємо
(t = s)(d) ( t = s)(d) та (t = s)(d) ( t = s)(d).
Наслідок. Для функціонально стабільних ТмМС маємо M |= t = s t = s та M |= t = s t = s.
Висновки
На основі інтегрованого інтенсіонально-екстенсіонального підходу до побудови логічних та програмних
систем пропонуються та досліджуються композиційно-номінативні модальні та темпоральні логіки
функціонально-екваційного рівня. Для цих логік розглядається спеціальне уточнення поняття композиційно-
номінативної модальної системи, визначаються транзиційні та темпоральні модальні системи, вивчаються їх
семантичні властивості.
1. Нікітченко М.С., Шкільняк С.С. Математична логіка та теорія алгоритмів. – К.: ВПЦ "Київський університет", 2008. – 528 с.
2. Нікітченко М.С., Шкільняк С.С. Інтенсіонально-орієнтований підхід до побудови логічних систем // Проблеми програмування. – 2007. –
№ 2. – C. 15–40.
3. Шкільняк О.С. Композиційно-номінативні модальні та темпоральні логіки: семантичні властивості, секвенційні числення // Наукові
записки НаУКМА. Серія: Комп’ютерні науки. – 2008. – Т. 6. – C. 25–34.
4. Shkilnyak O.S. Composition nominative modal and temporal logics. – Proceedings of the 10th International Conference on Informatics
“Informatics 2009”. – Herlany, Slovakia, 2009. – P. 148–153.
5. Шкільняк О.С. Композиційно-номінативні модальні та темпоральні логіки номінативних рівнів. // Міжнар. конф. "Теоретичні та
прикладні аспекти побудови програмних систем". – TAAPSD'2009. Тези доповідей. – К., 2009. – С. 100–107.
6. Шкільняк О.С. Семантичні властивості композиційно-номінативних модальних логік // Проблеми програмування. – 2009. – № 4. –
C. 11–24.
|
| id | pp_isofts_kiev_ua-article-863 |
| institution | Problems in programming |
| keywords_txt_mv | keywords |
| language | Ukrainian |
| last_indexed | 2026-06-02T01:00:20Z |
| publishDate | 2026 |
| publisher | PROBLEMS IN PROGRAMMING |
| record_format | ojs |
| resource_txt_mv | ppisoftskievua/db/f06dd3d8e665aeebe74a557631e862db.pdf |
| spelling | pp_isofts_kiev_ua-article-8632026-06-01T06:02:58Z Compositional-nominative modal logics of the functional-equational level Композиційно-номінативні модальні логіки функціонально-екваційного рівня Shkilniak, O.S. UDC 681.3.06 УДК 681.3.06 Composition nominative modal and temporal logics of functional-equational level are introduced in this paper. Transition and temporal modal systems are specified for such logics, and their semantic properties are investigated. Prombles in programming 2010; 2-3: 42-47 Пропонуються композиційно-номінативні модальні та темпоральні логіки функціонально-екваційного рівня. Для цих логік визначаються транзиційні та темпоральні модальні системи, досліджуються їх семантичні властивості.Prombles in programming 2010; 2-3: 42-47 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2026-06-01 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/863 PROBLEMS IN PROGRAMMING; No 2-3 (2010); 42-47 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2010); 42-47 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2010); 42-47 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/863/915 Copyright (c) 2026 PROBLEMS IN PROGRAMMING |
| spellingShingle | UDC 681.3.06 Shkilniak, O.S. Compositional-nominative modal logics of the functional-equational level |
| title | Compositional-nominative modal logics of the functional-equational level |
| title_alt | Композиційно-номінативні модальні логіки функціонально-екваційного рівня |
| title_full | Compositional-nominative modal logics of the functional-equational level |
| title_fullStr | Compositional-nominative modal logics of the functional-equational level |
| title_full_unstemmed | Compositional-nominative modal logics of the functional-equational level |
| title_short | Compositional-nominative modal logics of the functional-equational level |
| title_sort | compositional-nominative modal logics of the functional-equational level |
| topic | UDC 681.3.06 |
| topic_facet | UDC 681.3.06 УДК 681.3.06 |
| url | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/863 |
| work_keys_str_mv | AT shkilniakos compositionalnominativemodallogicsofthefunctionalequationallevel AT shkilniakos kompozicíjnonomínativnímodalʹnílogíkifunkcíonalʹnoekvacíjnogorívnâ |