First-order logics with partial predicates for checking variable definedness
We study semantic properties of new classes of program-oriented logics of partial quasiary predicates without monotonicity restriction. A feature of these logics is the use of special 0-ary parametric compositions – partial predicates which checks whether a subject name (variable) has a value in a g...
Збережено в:
| Дата: | 2025 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2025
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/671 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-671 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/57/83b0b4cab48fe134726998ed9f8d0957.pdf |
| spelling |
pp_isofts_kiev_ua-article-6712025-04-16T13:57:48Z First-order logics with partial predicates for checking variable definedness Першопорядкові логіки з частковими предикатами для перевірки означенності змінної Shkilniak, S.S. logic; semantics; partial predicate; logical consequence UDC 004.42:510.64 логіка; семантика; частковий предикат; логічний наслідок УДК 004.42:510.64 We study semantic properties of new classes of program-oriented logics of partial quasiary predicates without monotonicity restriction. A feature of these logics is the use of special 0-ary parametric compositions – partial predicates which checks whether a subject name (variable) has a value in a given data. Such predicates-indicators are needed for quantifier elimination: from formulas of the form x we come to formulas of the form To perform such elimination in logics of non-monotonic predicates, the condition of definedness of a name z is needed, meaning a component with the name zis contained in the input data. We propose two types of pure first-order logics with partial predicates-indicators: LQ and LQ. Logics LQ use extended renominations, while LQ use traditional renominations. In this paper we describe composition algebras and languages of these logics, and introduce and investigate logical consequence relations for formulas and sets of formulas of the language: irrefutability (IR), truth (T), falsity (F) and strong (TF) logical consequences. Conditions that guarantee the logical consequence relation are considered, and their main properties are specified. Special attention is paid to the properties related to predicates-indicators and quantifier elimination. Logical consequence relations’ properties are the semantic basis for sequent calculi’s construction. Basic properties of a given logical consequence relation induce respective sequent forms for the corresponding calculus; properties that guarantee the logical consequence relation induce closedness conditions for sequents in this calculus. Construction of such sequent calculi is planned in the future works.Prombles in programming 2024; 4: 23-33 В роботі досліджено нові класи програмно-орієнтованих логічних формалізмів – чисті першопорядковілогіки часткових квазіарних предикатів без обмеження монотонності. Їхньою характерною особливістю є наявність спеціальних 0-арних композицій – часткових предикатів, які визначають наявність у вхідних даних компоненти з відповідним предметним іменем (змінною), тобто з’ясовують означеність цього імені. Такі предикати-індикатори необхідні для елімінації кванторів у логіках немонотонних предикатів. Запропоновано два різновиди логік із частковими предикатами-індикаторами: LQ (із традиційними реномінаціями) та LQ (із розширеними реномінаціями). Описано композиційні алгебри та мови цих логік, дослідженовідношення логічного наслідку. Розглянуто умови гарантованої наявності цих відношень, наведено їхні основні властивості. Увагу акцентовано на властивостях, пов’язаних із предикатами-індикаторами та з елімінацією кванторів. Властивості відношень логічного наслідку є семантичною основою побудови для пропонованих логік відповідних числень секвенційного типу, що буде зроблено в наступних роботах.Prombles in programming 2024; 4: 23-33 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-04-16 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/671 10.15407/pp2024.04.023 PROBLEMS IN PROGRAMMING; No 4 (2024); 23-33 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 4 (2024); 23-33 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 4 (2024); 23-33 1727-4907 10.15407/pp2024.04 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/671/723 Copyright (c) 2025 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2025-04-16T13:57:48Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
logic semantics partial predicate logical consequence UDC 004.42:510.64 |
| spellingShingle |
logic semantics partial predicate logical consequence UDC 004.42:510.64 Shkilniak, S.S. First-order logics with partial predicates for checking variable definedness |
| topic_facet |
logic semantics partial predicate logical consequence UDC 004.42:510.64 логіка семантика частковий предикат логічний наслідок УДК 004.42:510.64 |
| format |
Article |
| author |
Shkilniak, S.S. |
| author_facet |
Shkilniak, S.S. |
| author_sort |
Shkilniak, S.S. |
| title |
First-order logics with partial predicates for checking variable definedness |
| title_short |
First-order logics with partial predicates for checking variable definedness |
| title_full |
First-order logics with partial predicates for checking variable definedness |
| title_fullStr |
First-order logics with partial predicates for checking variable definedness |
| title_full_unstemmed |
First-order logics with partial predicates for checking variable definedness |
| title_sort |
first-order logics with partial predicates for checking variable definedness |
| title_alt |
Першопорядкові логіки з частковими предикатами для перевірки означенності змінної |
| description |
We study semantic properties of new classes of program-oriented logics of partial quasiary predicates without monotonicity restriction. A feature of these logics is the use of special 0-ary parametric compositions – partial predicates which checks whether a subject name (variable) has a value in a given data. Such predicates-indicators are needed for quantifier elimination: from formulas of the form x we come to formulas of the form To perform such elimination in logics of non-monotonic predicates, the condition of definedness of a name z is needed, meaning a component with the name zis contained in the input data. We propose two types of pure first-order logics with partial predicates-indicators: LQ and LQ. Logics LQ use extended renominations, while LQ use traditional renominations. In this paper we describe composition algebras and languages of these logics, and introduce and investigate logical consequence relations for formulas and sets of formulas of the language: irrefutability (IR), truth (T), falsity (F) and strong (TF) logical consequences. Conditions that guarantee the logical consequence relation are considered, and their main properties are specified. Special attention is paid to the properties related to predicates-indicators and quantifier elimination. Logical consequence relations’ properties are the semantic basis for sequent calculi’s construction. Basic properties of a given logical consequence relation induce respective sequent forms for the corresponding calculus; properties that guarantee the logical consequence relation induce closedness conditions for sequents in this calculus. Construction of such sequent calculi is planned in the future works.Prombles in programming 2024; 4: 23-33 |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2025 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/671 |
| work_keys_str_mv |
AT shkilniakss firstorderlogicswithpartialpredicatesforcheckingvariabledefinedness AT shkilniakss peršoporâdkovílogíkizčastkovimipredikatamidlâperevírkioznačennostízmínnoí |
| first_indexed |
2025-07-17T09:53:05Z |
| last_indexed |
2025-07-17T09:53:05Z |
| _version_ |
1850409856969736192 |
| fulltext |
Програмна інженерія – теоретичні методи
23
УДК 004.42:510.64 http://doi.org/10.15407/pp2024.04.023
С.С. Шкільняк
ПЕРШОПОРЯДКОВІ ЛОГІКИ З ЧАСТКОВИМИ
ПРЕДИКАТАМИ ДЛЯ ПЕРЕВІРКИ ОЗНАЧЕНОСТІ ЗМІННОЇ
В роботі досліджено нові класи програмно-орієнтованих логічних формалізмів – чисті першопорядкові
логіки часткових квазіарних предикатів без обмеження монотонності. Їхньою характерною особливіс-
тю є наявність спеціальних 0-арних композицій – часткових предикатів, які визначають наявність у вхі-
дних даних компоненти з відповідним предметним іменем (змінною), тобто з’ясовують означеність
цього імені. Такі предикати-індикатори необхідні для елімінації кванторів у логіках немонотонних пре-
дикатів. Запропоновано два різновиди логік із частковими предикатами-індикаторами: L
Q (із традицій-
ними реномінаціями) та L⊥
Q (із розширеними реномінаціями). Описано композиційні алгебри та мови
цих логік, досліджено відношення логічного наслідку. Розглянуто умови гарантованої наявності цих ві-
дношень, наведено їхні основні властивості. Увагу акцентовано на властивостях, пов’язаних із преди-
катами-індикаторами та з елімінацією кванторів. Властивості відношень логічного наслідку є семантич-
ною основою побудови для пропонованих логік відповідних числень секвенційного типу, що буде зроб-
лено в наступних роботах.
Ключові слова: логіка, семантика, частковий предикат, логічний наслідок
Shkilniak S. S.
FIRST-ORDER LOGICS WITH PARTIAL PREDICATS FOR
CHECKING VARIABLE DEFINEDNESS
We study semantic properties of new classes of program-oriented logics of partial quasiary predicates without
monotonicity restriction. A feature of these logics is the use of special 0-ary parametric compositions – partial
predicates which checks whether a subject name (variable) has a value in a given data. Such predicates-
indicators are needed for quantifier elimination: from formulas of the form x we come to formulas of the
form ( ).x
zR To perform such elimination in logics of non-monotonic predicates, the condition of definedness
of a name z is needed, meaning a component with the name z is contained in the input data. We propose two
types of pure first-order logics with partial predicates-indicators: L
Q and L⊥
Q. Logics L⊥
Q use extended re-
nominations, while L
Q use traditional renominations. In this paper we describe composition algebras and lan-
guages of these logics, and introduce and investigate logical consequence relations for formulas and sets of
formulas of the language: irrefutability (IR), truth (T), falsity (F) and strong (TF) logical consequences. Condi-
tions that guarantee the logical consequence relation are considered, and their main properties are specified.
Special attention is paid to the properties related to predicates-indicators and quantifier elimination. Logical
consequence relations’ properties are the semantic basis for sequent calculi’s construction. Basic properties of
a given logical consequence relation induce respective sequent forms for the corresponding calculus; properties
that guarantee the logical consequence relation induce closedness conditions for sequents in this calculus. Con-
struction of such sequent calculi is planned in the future works.
Keywords: logic, semantics, partial predicate, logical consequence.
Вступ
Апарат математичної логіки успіш-
но використовується для опису й моделю-
вання різноманітних предметних областей,
cистем штучного інтелекту, інформацій-
них та програмних систем (див., напр.,
[1]). Водночас обмеження класичної логіки
предикатів, роблять вельми актуальною
задачу побудови нових, програмно-орієн-
тованих логічних формалізмів.
Метою пропонованої роботи є дос-
лідження нових класів програмно-орієн-
тованих логік – чистих першопорядкових
композиційно-номінативних логік частко-
вих квазіарних предикатів (ЧКНЛ) зі зня-
тою умовою монотонності (еквітонності).
У побудові виведень в секвенційних чис-
леннях таких логік необхідно робити елі-
мінацію кванторів. Це означає еквівалент-
© С.С. Шкільняк, 2024
ISSN 1727-4907. Проблеми програмування. 2024. №4
Програмна інженерія – теоретичні методи
24
ний перехід у секвенційних формах від
формул вигляду x до їхніх прикладів –
формул вигляду ( ).x
zR В логіках немоно-
тонних предикатів це можливо за умови
означеності предметного імені (змінної) z,
тобто наявності у вхідних даних компонен-
ти з іменем z. Тому для елімінації кванто-
рів у логіках немонотонних предикатів по-
трібні спеціальні предикати-індикатори
наявності у вхідних даних компоненти з
відповідним предметним іменем. Можна
виділити два їхніх різновиди: тотальні
предикати-індикатори Ez, які визначають
наявність чи відсутність компоненти з
іменем z, та часткові, які визначають лише
наявність такої компоненти.
Низку ЧКНЛ з тотальними преди-
катами-індикаторами Ez описано, зокрема,
в роботах [2–5]. В даній роботі ми пропо-
нуємо логіки з частковими предикатами-
індикаторами z.
Залежно від використання тради-
ційних [2, 3] чи розширених [4, 5] реномі-
націй виділимо два різновиди ЧКНЛ з час-
тковими предикатами-індикаторами: L
Q
(із традиційними реномінаціями) та L⊥
Q
(із розширеними реномінаціями). Тради-
ційні реномінації є окремим випадком ро-
зширених реномінацій, тому логіки L
Q є
окремим випадком логік L⊥
Q.
Описані в [3] ЧКНЛ, збагачені пре-
дикатами слабкої рівності =xy та строгої рі-
вності xy, використовують предикати Ez.
Водночас в ЧКНЛ зі слабкою рівністю ок-
ремі предикати-індикатори не потрібні,
адже z, та =zz – це один і той же предикат!
В даній роботі досліджено семанти-
чні властивості L⊥
Q та L
Q. Описано мови
цих логік, досліджено відношення логічно-
го наслідку. Розглянуто умови гарантова-
ної наявності цих відношень, наведено їхні
основні властивості. Особливу увагу при-
ділено властивостям, пов’язаним з преди-
катами z та з елімінацією кванторів. Такі
властивості є семантичною основою побу-
дови для L⊥
Q та L
Q відповідних числень
секвенційного типу.
1. Композиційні предикатні
алгебри логік L⊥
Q та L
Q
Для полегшення читання наведемо
необхідні для подальшого викладу визна-
чення. Поняття, які тут не визначені, тлу-
мачимо в сенсі робіт [2, 5].
V-A-квазіарний предикат – це част-
кова неоднозначна, взагалі кажучи, функ-
ція Q : VA → {T, F}, VA – множина всіх V-A-
іменних множин (V-A-ІМ), {T, F} – множи-
на істиннісних значень, V та A – множини
предметних імен (змінних) та предметних
значень (базових даних). V-A-ІМ формаль-
но визначають [2] як однозначну функцію
d : V → A. Подаємо V-A-ІМ у вигляді
[ ] ,i i i Iv a де vіV, aіA, vі vj при і j.
Для V-A-ІМ вводимо (див. [5]) опе-
рації ||–Z, де ZV, та (розширеної) реномі-
нації 1 1
1
,..., , ,...,
,..., , ,...,r ,n m
n
v v u u
x x ⊥ ⊥ де vі, xi, ujV, а cимвол
⊥V означає відсутність значення:
||–Z(d) = { v a d | vZ};
1 1
1
,..., , ,...,
,..., , ,...,r ( )n m
n
v v u u
x x d⊥ ⊥ =
1 11 1 ,..., , ,...,[ ( ),..., ( )] || .
n mn n v v u uv d x v d x d −=
Порядок пар імен у цьому позна-
ченні неістотний. Наприклад, , , , ,
, , , ,r та rv y u v u y
x z x z⊥ ⊥
– це позначення однієї й тієї ж операції.
Замість 1 1
1
,..., , ,...,
,..., , ,...,r n m
n
v v u u
x x ⊥ ⊥ стисло пишемо ,
,r .v u
x ⊥
Кожний R-предикат Q однозначно
задається парою таких множин:
– область істинності T(Q) = {d | TQ[d]};
– область хибності F(Q) = {d | FQ[d]}.
V-A-квазіарний R-предикат Q:
– частковий однозначний, або P-пре-
дикат, якщо T(Q)F(Q) =;
– тотальний, або T-предикат, якщо
T(Q)F(Q) = VA;
– TS-предикат, якщо T(Q)F(Q) = та
T(Q)F(Q) = VA;
– неспростовний, якщо F(Q) = ;
– виконуваний, якщо T(Q) ;
– тотожно істинний (позн. T), якщо
F(Q) = та T(Q) = VА;
– тотожно хибний (позн. F), якщо
T(Q) = та F(Q) = VА;
– тотально невизначений (позн. ),
якщо T(Q) = F(Q) = ;
– тотально амбівалентний (позн. ),
якщо T(P) = F(P) = VА;
Програмна інженерія – теоретичні методи
25
– монотонний: d1 d2 Q[d1]Q[d2];
– антитонний: d1 d2 Q[d1]Q[d2].
Для P-предикатів монотонність стає
еквітонністю: Q еквітонний, якщо з умови
Q(d) та d d' випливає Q(d')= Q(d).
Класи V-A-квазіарних R-, P-, T-, TS-
предикатів позначатимемо PrRV–A, PrPV–A,
PrTV–A, PrTS V–A. Усі TS-предикати, окрім
константних T та F, немонотонні.
Монотонні R-предикати, антитонні
R-предикати, еквітонні P-предикати, анти-
тоннi T-предикати названо RM-, RА-, PE-,
TА-предикатами. Класи V-A-квазіарних
RM-, RА-, PE-, TА-предикатів позначають
PrRMV–A, PrRAV–A, PrPEV–A, PrTAV–A.
Ім'я хV неістотне для R-предиката
Q, якщо для всіх d1, d2VA маємо:
d1 ||–х = d2 ||–х Q[d1] = Q[d2].
Опишемо базові композиції L⊥
Q.
Пропозиційні композиції (логічні
зв’язки) і та композицію квантифікації
(квантор) x задамо так:
T(P) = F(P); F(P) = T(P);
T(PQ) = T(P)T(Q); F(PQ) = F(P)F(Q);
T(xP) = { | || ( )};x
a A
d d x a T P−
F(xP) = { | || ( )}.x
a A
d d x a F P−
Композицію реномінації ,
,R v u
x ⊥ зада-
мо через відповідну операцію реномінації:
, ,
, ,R ( )[ ] [r ( )].v u v u
x xQ d Q d⊥ ⊥=
Традиційні [2, 3] операція реноміна-
ції r v
x та композиція реномінації R v
x є ок-
ремими випадками ,
,rv u
x ⊥ та ,
,R .v u
x ⊥
Спеціальні 0-арні композиції – част-
кові предикати-індикатори z – задамо так:
T(z) = {d | d(z)}; F(z) = .
Предикати z еквітонні. Усі xV та-
кі, що x z, неістотні для z.
Отримуємо такі множини базових
композицій для LI
Q та LI
Q:
– C⊥Q = {,, ,
,R ,v u
x ⊥ х, z} для LI
Q;
– CQ = {,, R ,v
x х, z} для LI
Q.
Нагадаємо, що для тотальних пре-
дикатів-індикаторів Ez маємо (див. [2, 5]):
T(Ez) = {d | d(z)} та F(Ez) = {d | d(z)}.
Звідси T(z) = T(Ez).
Зауважимо, що в ЧКНЛ зі слабкою
рівністю [3] предикати-індикатори вже є:
T(=zz) = {d | d(z)) = T(z), F(=zz) == F(z).
Це означає: предикати z та =zz збігаються.
Асиметрія предикатів x щодо іс-
тинності та хибності індукує таку асимет-
рію в логіках L⊥
Q та L
Q. Це надає логікам
L⊥
Q та L
Q певних ознак девіантності.
Властивості пропозиційних компо-
зицій та кванторів, не пов’язані з реномі-
націями, аналогічні властивостям класич-
них логічних зв’язок та кванторів [6]. Ма-
ємо [4, 5] такі базові властивості, пов’язані
з композицією реномінації: Ren, R, R⊥I,
R⊥U, R1, R2, R⊥, R⊥, R⊥R, R⊥s, R⊥.
Для традиційної реномінації маємо (див.
[2]) Ren, R, RI, RU, R, R, RR, Rs, R.
Властивості предикатів z, пов'язані
з логічними зв’язками та кванторами:
– z z = z→ z = z z = z;
– z & z = z;
– xx = xx = T,
– xx = xx = F;
– yx = yx = x за умови x y;
– yx = yx = x за умови x y.
Властивості реномінації предикатів-
індикаторів z:
R⊥⊥) , ,
, ,R ( ) ;v u z
x z⊥ ⊥ =
R⊥v) , ,
, ,R ( ) ;v u z
x y z y⊥ =
R⊥t) ,
,R ( )v u
x z z⊥ = за умови { , }.z v u
Для традиційної реномінації маємо:
Rv) ,
,R ( ) ;v z
x y z y=
Rt) R ( )v
x z z= за умови { }.z v
Маємо T(z) = T(Ez), тому наведені
в [4, 5]). властивості, на яких базується
елімінація кванторів, можна переформу-
лювати із використанням предикатів z.
, ,
, ,(R ( ))u w x
v yT P⊥ T(y) ,
,(R ( ))u w
vT xP⊥ (T)
,
,(R ( ))u w
vF xP⊥ T(y) , ,
, ,(R ( ))u w x
v yF P⊥ (F)
Ці співвідношення переформулює-
мо, записуючи F(y) замість T(y):
, ,
, ,(R ( ))u w x
v yT P⊥ F(y) ,
,(R ( ))u w
vT xP⊥ (T)
,
,(R ( ))u w
vF xP⊥ F(y) , ,
, ,(R ( ))u w x
v yF P⊥ (F)
Семантичними моделями певного
класу ЧКНЛ є композиційні предикатні
системи вигляду (VA, PrV–A, CB), де CB –
множина базових композицій, PrV–A – клас
квазіарних предикатів. Кожна така система
задає дві алгебри: алгебру (структуру) да-
Програмна інженерія – теоретичні методи
26
них (VA, PrV–A) та композиційну алгебру
предикатів (PrV–A, CB). Для L⊥
Q і L
Q отри-
муємо композиційні системи R-предикатів
(VA, PrRV–A, C⊥Q) і (VA, PrRV–A, CQ) та
композиційні алгебри предикатів
A⊥Q = (PrRV–A, C⊥Q) і AQ = (PrRV–A, CQ).
Необхідна умова того, що певний
клас квазіарних предикатів утворює алгеб-
ру – його замкненість щодо операцій алге-
бри. 0-арні композиції – предикати z –
однозначні й монотонні (еквітонні), а це
означає незамкненість класів T-, TS-, RА-,
TА-предикатів щодо композицій C⊥Q та
CQ. Водночас щодо композицій C⊥Q та
CQ замкнені класи P-предикатів, а також
RM- та PE-предикатів. Тому можна виді-
лити такі підалгебри алгебр A⊥Q та AQ:
A⊥QP = (PrPV–A, C⊥Q), AQP = (PrPV–A, CQ);
A⊥QM =(PrRMV–A,C⊥Q), AQM =(PrRMV–A,CQ);
A⊥QPE =(PrPEV–A,C⊥Q), AQPE =(PrPEV–A,CQ).
Логіки монотонних та еквітонних
предикатів тут не розглядаємо, тому зосе-
редимо увагу на алгебрах R-предикатів
A⊥Q і AQ та P-предикатів A⊥QP і AQP.
2. Мови логік L⊥
Q та L
Q
Терми композиційної алгебри пре-
дикатів трактуємо як формули мови.
При зафіксованій множині базових
композицій мови ЧКНЛ відрізняються
множинами імен базових предикатів
(сигнатурою) і способами запису формул.
Опишемо мову L⊥
Q. Використо-
вуємо префіксну форму запису формул.
Алфавiт мови:
– множина V предметних імен (змінних),
– множина Ps предикатних символів,
– множина Cs = {,, ,
, ,v u
xR ⊥ x, z} симво-
лів базових композицій.
Дамо індуктивне визначення мно-
жини Fr формул мови:
Fa) PsFr;
F) {z | z V}Fr;
Fp) ,Fr Fr, Fr;
FR⊥) Fr ,
, ;v u
xR Fr⊥
F) Fr xFr.
Формули рPs та z – атомарні.
В мовах ЧКНЛ задаємо множину
VTV імен, неістотних для всіх рPs –
тотально неістотних [2] імен.
Для визначення множин гаранто-
вано неістотних для формул мови L⊥
Q
імен задамо функцію : Fr→2V. Для кож-
ного xV задаємо (x) = V \{x}, для кож-
ного рPs задаємо (р), водночас має ви-
конуватись VT(р), а далі визначаємо
так, як описано в [2].
Розширена сигнатура мови – це
= (V, VT, Cs, Ps).
Fr – СF-формула (constant free),
якщо не містить символів композицій-
констант, тобто не містить символів x.
Для Fr вводимо позначення:
– () – це множина всіх рРs, які
входять до складу формул ;
– nm() – це множина всіх xV, які
фігурують у формулax .
– ( ) ( )
= .
Зокрема, для Fr вводимо позна-
чення () та nm().
Мову L⊥
Q інтерпретуємо на компо-
зиційних системах CS = (VA, PrRV–A, C⊥Q).
Символи базових композицій інтер-
претуємо як відповідні композиції, симво-
ли x – як відповідні предикати-індикато-
ри. Для позначення символами Рs базових
предикатів задамо тотальне однозначне
I : Ps PrRV–A та продовжимо його до ві-
дображення інтерпретації I : Fr PrRV–A:
Ip) I() = (I());
I() = (I(), I());
IR⊥) , ,
, ,( ) R ( ( ));v u v u
x xI R I⊥ ⊥ =
I) I(х) = х(I()).
Трійку J = (CS,, I) назвемо інтер-
претацією мови L⊥
Q. Кожна (CS, , I) ви-
значається алгеброю із доданою сигнату-
рою A = ((VА, PrRV–A), , I). Такі алгебри
пов'язують мову логіки з алгеброю даних,
вони визначають композиційні системи
CS = (VA, PrRV–A, CI⊥Q). Тому вважатимемо
зазначені алгебри з доданою сигнатурою
інтерпретаціями мови L⊥
Q та скорочено
позначатимемо їх A = (A, I).
Програмна інженерія – теоретичні методи
27
Мова L
Q визначається аналогічно
мові L⊥
Q, лише замість символів ,
,
v u
xR ⊥ ви-
користовуємо символи .v
xR
Предикат J() – значення формули
при інтерпретації J – позначимо J.
Ім’я хV неістотне для формули ,
якщо х неістотне для J для кожної J.
Теорема 1. Якщо х(), то х неіс-
тотне для формули .
Для Fr та Fr визначимо
fu() = VT \ nm() та fu() = VT \ nm().
Теорема 2. уfu() у().
Наслідок. Нехай Fr та уfu(),
тоді у неістотне для кожної .
В алгебрах R-предикатів A⊥Q та AQ
виділено підалгебри P-предикатів A⊥QP та
AQP, а також підалгебри RM-предикатів
A⊥QM, AQM, та PE-предикатів A⊥QPE,
AQPE. Це виділяє класи R-інтерпретацій та
підкласи P-інтерпретацій, а також RM- та
PE-інтерпретацій. Такі класи інтерпрета-
цій називають семантиками.
Таким чином, в L⊥
Q маємо семан-
тики ⊥R, ⊥P, ⊥RM, ⊥PE. В L
Q маємо се-
мантики R, P, RM, PE.
⊥R та R назвемо R-семантиками.
⊥P та P назвемо P-семантиками.
В цій роботі вивчаємо логіки без
обмеження монотонності предикатів, тому
семантики типів RM та PE не розглядаємо,
увагу зосередимо на R- та P-семантиках.
Нехай – певна семантика.
Формула неспростовна за ін-
терпретації J, або J-неспростовна (позн.
J |=), якщо предикат J – неспростовний.
Формула неспростовна в семантиці
(позн. |=), якщо J |= при кожній J.
В логіках L⊥
Q та L
Q неспростовни-
ми є усі предикати-індикатори x.
Формула виконувана за інтер-
претації J, або J-виконувана, якщо преди-
кат J виконуваний. виконувана в семан-
тиці , якщо виконувана за певної J.
Для R-семантик поняття виконува-
ної формули малозмістовне. Справді, в R-
семантиці візьмемо J таку, що pJ =
для кожної pPs, тому T(J) для кож-
ної Fr. Звідси кожна формула вико-
нувана в R-семантиці .
Формула тотожно істинна при
інтерпретації J (позн. J |=id), якщо пре-
дикат J = T. Формула тотожно істин-
на в семантиці (позн. |=id), якщо
J |=id при кожній J.
Подібним чином можна дати визна-
чення тотожно хибної за інтерпретації J та
тотожно хибної в семантиці формули.
Якщо семантика зафіксована, то
замість |=, |=id пишемо |=, |=id .
Маємо J |=id J |=, |=id |=.
Формули, які завжди інтерпрету-
ються як константні предикати, назвемо
константними формулами. Такими є:
– T-формули, які завжди інтерпре-
туються як T; позначаємо їх T;
– F-формули, які завжди інтерпре-
туються як F; позначаємо їх F;
– ⊥-формули, які завжди інтерпре-
туються як ; позначаємо їх ⊥.
Приклад 1. 1) xx є T-формулами;
2) xx є F-формулами;
3) , ,
, , ( ) та ( )v u z z
xR z R z⊥ ⊥ ⊥ є ⊥-формулами.
Остання властивість засвідчує істо-
тну відмінність L⊥
Q від L
Q.
Якщо – T-формула, то |=id.
Формули, які завжди інтерпретую-
ться як частково константні предикати, на-
звемо частково константними. Такими є:
– pF-формули, в яких T(J) = для
всіх J; зокрема, це F-формули.
– pT-формули, в яких F(J) = для
всіх J; зокрема, це T-формули.
Для pT-формул маємо |=.
До pT-формул в L⊥
Q та L
Q належать
символи z. Справді, F(zJ) = для всіх J.
3. Відношення логічного наслідку
На основі різних співвідношень між
областями істинності та хибності предика-
тів можна ввести низку відношень логіч-
ного наслідку на множині формул мови.
Спочатку задаємо (див. [2, 5]) такі “при-
родні” відношення наслідку для двох фор-
мул та за умови фіксованої інтер-
претації J:
Програмна інженерія – теоретичні методи
28
– істинний, або T-наслідок J|=T :
J|=T T(J) T(J);
– хибний, або F-наслідок J|=F :
J|=F F(J)F(J);
– сильний, або TF-наслідок J|=TF :
J|=TF J|=T та J|=F;
– неспростовний, або IR-наслідок
J|=IR : J|=IR T(J)F(J) = .
– дуальний до IR, або DI-наслідок
J|=DI : J|=DI F(J)T(J) = VA.
Зазначені відношення індукують
відповідні відношення еквівалентності
формул та за умови інтерпретації J.
Задаємо їх за такою схемою:
J, якщо J|= та J|= .
Для відношення J TF маємо:
JTF T(J) = T(J) та F(J) = F(J).
Отже, JTF означає, що J та J
– це один і той же предикат.
Відношення логічного -наслідку в
семантиці та логічної еквівалентності в
семантиці задаємо за схемами:
|=, якщо J|= для кожної J;
, якщо J для кожної J.
На основі відношень наслідку J|=IR,
J|=DI, J|=T, J|=F, J|=TF для двох формул при
фіксованій J для семантик R, P (мова L
Q)
та ⊥R, ⊥P (мова L⊥
Q) загалом отримуємо
такі відношення логічного наслідку:
R
|=IR, R
|=DI, R
|=T, R
|=F, R
|=TF;
P
|=IR, P
|=DI, P
|=T, P
|=F, P
|=TF;
R
⊥|=IR, R
⊥|=DI, R
⊥|=T, R
⊥|=F, R
⊥|=TF;
P
⊥|=IR, P
⊥|=DI, P
⊥|=T, P
⊥|=F, P
⊥|=TF.
Деякі з цих відношень вироджені.
Твердження 1. 1) Не існує СF-фор-
мул та : R
|=IR чи R
⊥|=IR.
2) Не існує СF-формул та :
R
|=DI чи R
⊥|=DI чи P
|=DI чи
P
⊥|=DI.
Візьмемо інтерпретацію J, в якій усі
Ps інтерпретуються як . Тоді J = та
J = T(J) = T(J) = F(J) = F(J) = VA
T(J)F(J) = VA. Це доводить п. 1.
Візьмемо інтерпретацію J, в якій усі
Ps інтерпретуються о як . Тоді J = та
J = T(J) = T(J) = F(J) = F(J) =
F(J) T(J) = . Це доводить п. 2.
Таким чином, відношення типу DI
та відношення R|=IR, R
⊥|=IR вироджені.
Розглянемо властивості, пов’язані з
предикатами z та відношеннями |=T і |=F
(тут – одне з R, R
⊥, P
, P
⊥).
Маємо F(x) = та x x = T, звідки
Твердження 2. 1) для довільних
Fr та yV маємо |=F y та |=IR y,
водночас xx |T y;
2) y |=T та y |=IR для довіль-
них Fr та yV, проте y |Fxx;
3) x Fy та x IRy для всіх x, yV.
Це засвідчує, що в L
Q та L⊥
Q від-
ношення типів T, F та TF істотно різні.
Отже, в L
Q та L⊥
Q маємо по 7 різних не-
вироджених відношень логічного наслідку:
P
|=IR, P
|=T, P
|=F, P
|=TF, R
|=T, R
|=F, R
|=TF;
P
⊥|=IR, P
⊥|=T, P
⊥|=F, P
⊥|=TF, R
⊥|=T, R
⊥|=F, R
⊥|=TF.
Графічно співвідношення між ними
можна подати так (тут – це чи ⊥, а за-
мість вживаємо →):
R
*|=T → P
*|=T
R
*|=TF → P
*|=TF
P
*|=IR
R
*|=F → P
*|=F
Відношення логічного наслідку ін-
дукують відношення логічної еквівалент-
ності. Отримуємо 7+7 відповідних відно-
шень P*IR, P
*T, P
*F, P
*TF, R
*T, R
*F, R
*TF.
Далі індекси та ⊥ в позначенні ві-
дношень зазвичай опускаємо, із контексту
буде зрозуміло, про яку семантику йде мова.
Теорема 3. Зазначені відношення
логічного наслідку рефлексивні й транзи-
тивні; відношення логічної еквівалентності
рефлексивні, транзитивні та симетричні.
Описані в [2] властивості пропо-
зиційного рівня справджуються для введе-
них тут відношень в L
Q й L⊥
Q. Зокрема:
Теорема 4. 1) & P|=T, проте
& P|F;
2) P|=F, проте P|T;
3) & P|=TF;
4) & R|TF.
Основа еквівалентних перетворень
формул – теорема еквівалентності. Вона
виконується для відношень типів TF та IR,
проте невірна для відношень типів T та F.
Програмна інженерія – теоретичні методи
29
Теорема 5. Нехай ' отримано з
формули заміною деяких входжень
1, ..., n на 1, ..., n. Якщо 1 1, ...,
n n, то '.
Тут одне з RTF, PTF, PIR.
На основі властивостей предикатів
Ren, R, R⊥I, R⊥U, R1, R2, R⊥, R⊥, R⊥R,
R⊥s, R⊥ (логіка L⊥
Q) та Ren, R, RI, RU,
R, R, RR, Rs, R (логіка L
Q) отримує-
мо однойменні властивості формул. Для
їхнього опису використаємо відношення
типу TF.
Для формул мов L
Q та L⊥
Q маємо
специфічні властивості пов’язані з z. Во-
ни отримуються на основі наведених вище
відповідних властивостей предикатів:
R⊥v) , ,
, , ( ) ;v u z
x y TFR z y⊥
R⊥t) ,
, ( )v u
x TFR z z⊥ за умови { , };z v u
Rv) ,
, ( ) ; v z
x y TFR z y
Rt) ( )v
x TFR z z за умови { }.z v
Пропозиційні властивості z:
|= z; z z TF z; z & z TFz.
Властивості квантифікації:
– |=id xx та |=idx x;
– yxTFx та yxTFx за умови xy.
Відношення наслідку і логічного
наслідку поширимо на пари множин фор-
мул. Назвемо їх відношеннями set-наслід-
ку та логічного set-наслідку.
Нехай деяка Fr, нехай J – інтер-
претація. Далі позначаємо:
( )JT
як T(J), ( )JF
як F(J),
( )JT
як T(J), ( )JF
як F(J).
Нехай ,Fr.
є IR-наслідком при інтерпретації J
(позн. J|=IR), якщо T(J)F(J) =.
є DI-наслідком при інтерпретації J
(позн. J|=DI), якщо F(J)T(J) = VA.
є T-наслідком при інтерпретації J
(позн. J|=T), якщо T(J)T(J).
є F-наслідком при інтерпретації J
(позн. J|=F), якщо F(J)F(J).
є TF-наслідком при інтерпретації J
(позн. J|=TF), якщо J|=T та J|=F.
Відношення логічного -set-наслідку
в семантиці задамо за схемою:
|= , якщо J|= для кожної J.
В R- та P-семантиках логік L
Q та
L⊥
Q маємо по 7 різних невироджених від-
ношень логічного set-наслідку. Їхні назви
та співвідношення між ними такі ж, як для
відповідних відношень для двох формул.
Відношення типів DI та IR в R-се-
мантиках вироджені. Відношення типів T,
F та TF в R-семантиках істотно різні.
Твердження теореми 4 для відно-
шень set-наслідку узагальнюється так.
Теорема 6. 1) ,& P|=T,,
проте ,& P|F,;
2) , P|=F,, проте
, P|T,;
3) ,& P|=TF,;
4) ,& R|TF,.
Аналогом теореми еквівалентності
для відношень є теорема заміни еквівален-
тних. Вона справджується для відношень
логічної еквівалентності типів RTF, PTF,
PIR та відношень логічного наслідку від-
повідних типів: R|=TF, P|=TF, P|=T, P|=F, P|=IR
у випадку RTF; P|=TF, P|=T, P|=F, P|=IR у ви-
падку PTF; P|=IR у випадку PIR.
Теорема 7. Нехай , тоді:
, |= , |= ;
|= , |= ,.
Для введених відношень логічного
set-наслідку маємо властивість монотонно-
сті, для них виконуються властивості де-
композиції формул L, R, L, R, L,
R, L, R (див. [2, 5])
Bластивості відношень логічного
set-наслідку, пов'язані з еквівалентними пе-
ретвореннями, базуються на властивостях
формул, пов’язаних з композиціями рено-
мінації. В L⊥
Q ці властивості отримуємо на
основі властивостей R, R⊥I, R⊥U, R1, R2,
R⊥, R⊥, R⊥R, R⊥s, R⊥; в L
Q такі влас-
тивості отримуємо на основі R, RI, RU,
R, R, RR, Rs, R. Кожна така влас-
тивість формул R продукує 4 відповідні
властивості R⊥L, R⊥R, R⊥L, R⊥R для
відношення логічного set-наслідку, коли
виділена формула чи її заперечення – у лі-
вій чи правій частині цього відношення.
У використанні властивостей елімі-
нації кванторів під реномінацією власти-
Програмна інженерія – теоретичні методи
30
вості типів Rs та R мають допоміжний
характер і не належать до базових.
Подібним чином властивості R⊥v,
R⊥t в L⊥
Q та властивості Rv, Rt в L
Q
продукують по 4 властивості спрощення за
реномінації предикатів-індикаторів.
Для прикладу наведемо властивості,
індуковані R⊥v:
, ,
vL , ,R ) ( ), | , | ;v u z
x yR z y⊥ ⊥ = =
, ,
vR , ,R ) | ( ), | , ;v u z
x yR z y⊥ ⊥ = =
, ,
vL , ,R ) ( ), | , | ;v u z
x yR z y⊥ ⊥ = =
, ,
vR , ,R ) | ( ), | , .v u z
x yR z y⊥ ⊥ = =
У L⊥ маємо властивості елімінації
для константних ⊥-формул , ,
, , ( )v u z
xR z⊥ ⊥ :
ElL) , ,
, , *( ), |v u z
xR z⊥ ⊥ = , ,
, , *( ), | ;v u z
xR z⊥ ⊥ =
ElR) , ,
* , ,| ( ),v u z
xR z⊥ ⊥ = , ,
* , ,| ( ), .v u z
xR z⊥ ⊥ =
Для ⊥-формул , ,
, , ( )v u z
xR z⊥ ⊥ маємо вла-
стивості елімінації ⊥-формул:
ElRF) , ,
, , ( ),v u z
xR z⊥ ⊥ |=F |=F;
ElRT) |=T, , ,
, , ( )v u z
xR z⊥ ⊥ |=T.
У L⊥ та L⊥ маємо властивості елі-
мінації pT-формул z та pF-формул z:
ElF) z, |=F |=F;
ElT) |=T,z |=T.
Опишемо похідні властивості від-
ношень логічного set-наслідку, пов'язані з
T-формулами xx та F-формулами xx.
Зняття в xx та xx:
L) xx, |= |= , xx;
R) |= ,xx xx, |= ;
L) xx, |= |= , xx;
R) |= ,xx xx, |= .
Елімінація xx та xx:
El) xx, |= |= ;
El) |= , xx |= .
Також маємо елімінацію z зі “сві-
жим” неістотним іменем z, якщо z – зліва
у відношенні логічного set-наслідку. Якщо
ж z – справа у цьому відношенні, то для
F-наслідку така елімінація некоректна,
адже гарантовано виконується |=F, z,
проте не завжди |=F: xx R
|F xx.
Отже, маємо такі похідні властиво-
сті елімінації z за “свіжим” неістотним z:
ElL) z, |= |= , якщо zfu(,);
ElR) |=T,z |=T, якщо zfu(,).
Опишемо властивості елімінації
кванторів в L
Q та L⊥
Q. Важливо, що тут
маємо різні описи елімінації кванторів для
відношень логічного T-наслідку (вживаємо
z) та F-наслідку (вживаємо z).
В L⊥
Q маємо такі властивості елі-
мінації кванторів (тут – P
⊥ чи R⊥):
R⊥TL) за умови ,
,( , , ( ))v u
wz fu R x⊥
,
, ( ),v u
wR x⊥ |=T , ,
, , ( ), ,v u x
w zR z⊥ |=T;
R⊥TR) за умови ,
,( , , ( ))v u
wz fu R x⊥
|=T ,
, ( ),v u
wR x⊥ ,z |=T , ,
, , ( ),v u x
w zR ⊥ ;
R⊥vTR) , y ,
,| , ( )v u
T wR x
⊥=
, y , , ,
, , ,| , ( ), ( )v u v u x
T w w yR x R
⊥ ⊥= ;
R⊥vTL) ,
, ( ), ,v u
wR x y⊥ |=T
, , ,
, , ,( ), ( ), ,v u v u x
w w yR x R y⊥ ⊥ |=T;
R⊥FL) за умови ,
,( , , ( ))v u
wz fu R x⊥
,
, ( ),v u
wR x⊥ |=F , ,
, , ( ),v u x
w zR ⊥ |=F,z;
R⊥FR) за умови ,
,( , , ( ))v u
wz fu R x⊥
|=F ,
, ( ),v u
wR x⊥ |=F , ,
, , ( ), , ;v u x
w zR z⊥
R⊥vFR) ,
,| , , ( )v u
F wy R x
⊥ =
, , ,
, , ,| , , ( ), ( )v u v u x
F w w yy R x R
⊥ ⊥ = ;
R⊥vFL) ,
, ( ),v u
wR x⊥ |=Fy,
, , ,
, , ,( ), ( ),v u v u x
w w yR x R⊥ ⊥ |=Fy,.
У випадку відношення P
⊥|=IR для
опису елімінації кванторів достатньо влас-
тивостей R⊥TL та R⊥vTR.
В L
Q маємо аналогічні властивості
елімінації кванторів RTL, RTR, RvTR,
RvTL, RFL, RFR, RvFR, RvFL .
Відмінність описів елімінації кван-
торів для відношень логічного T-наслідку
та логічного F-наслідку робить неможли-
вим подібний опис одним рядком для від-
ношень типу TF.
Допоміжні властивості -розподілу
та первісного означення в L
Q та L⊥
Q теж
різні для відношень типу T та типу F.
Для відношень типу T маємо:
vT) |=T z, |=T;
dT) |=T |=T , y та y, |=T.
Для відношень типу F маємо:
vF) |=F |=Fz,
Програмна інженерія – теоретичні методи
31
dF) |=F |=F ,y та y,|=F.
Властивості vT, dT, vF, dF та-
кож виконуються для відношень типу IR,
водночас як базові властивості для цих ві-
дношень доцільно взяти простіші vT та
dT.
Опис в L
Q та L⊥
Q властивостей від-
ношень логічного наслідку типу TF зво-
диться до паралельного опису таких влас-
тивостей для відношень типу T та типу F.
Таким чином, в логіках L
Q та L⊥
Q
відношення типу TF мають ознаки девіан-
тності, тому окремо розглядати ці відно-
шення далі не будемо.
Опишемо тепер властивості, які га-
рантовано виконуються для відношень
логічного set-наслідку певного типу.
Для усіх розглянутих відношень ло-
гічного set-наслідку маємо:
С) , |= ,.
Додатково гарантують наявність від-
ношення певного типу такі властивості.
СL) ,, P
|=T;
СR) P
|=F,,;
СLR) ,, P
|=TF,,.
В логіці L⊥
Q маємо властивосгі га-
рантованої наявності відношень логічного
set-наслідку на базі ⊥-формул , ,
, , ( ) :v u z
xR z⊥ ⊥
С⊥L) , ,
, , ( ),v u x
wR x⊥ ⊥ |=T;
С⊥R) |=F, , ,
, , ( ).v u x
wR x⊥ ⊥
В L⊥
Q й L
Q маємо властивості га-
рантованої наявності F-наслідку і T-наслі-
дку на базі pT-формул z та pF-формул z:
С) |=F z,;
С) z,, |=T.
На основі описаних властивостей
гарантованої наявності певного відношен-
ня |=* отримуємо однойменні умови га-
рантованої наявності деякого |=*:
С) існує формула : та ;
СL) існує формула : та ;
СR) існує формула : та ;
С⊥L) існує формула , ,
, , ( )v u x
wR x⊥ ⊥ ;
С⊥R) існує формула , ,
, , ( )v u x
wR x⊥ ⊥ ;
С) існує формула x;
С) існує формула x.
Тепер для конкретного відношення
логічного set-наслідку отримуємо наступні
умови його гарантованої наявності:
P
⊥|=IR: умова ССС⊥LС⊥R;
P
⊥|=T: умова ССLСС⊥L;
P
⊥|=F: умова ССRСС⊥R;
R
⊥|=T: умова ССС⊥L;
R
⊥|=F: умова ССС⊥R;
P
|=IR: умова СС;
P
|=T: умова ССLС;
P
|=F: умова ССRС;
R
|=T: умова СС;
R
|=F: умова СС.
Ці умови індукують умови замкне-
ності секвенції в численні, яке формалізує
відповідне відношення set-наслідку.
Підсумовуючи, для кожного з розг-
лянутих відношень логічного set-наслідку
типів IR, T, F, наведемо базові властивості,
які продукують секвенційні форми відпо-
відного числення. Для виразності ці влас-
тивості поєднаємо в групи, а потім укаже-
мо такі групи для кожного з відношень.
Властивості декомпозиції формул:
DIR = {L, R, L, R};
DTF = {L, R, L, R, L, R}.
Властивості елімінації кванторів:
⊥IR = {R⊥TL, R⊥vTR, dT, vT};
⊥T = {R⊥TL, R⊥TR, R⊥vTR,
R⊥vTL, dT, vT};
⊥F = {R⊥FL, R⊥FR, R⊥vFR,
R⊥vFL, dF, vF};
IR = {RTL, RvTR, dT, vT};
T = {RTL, RTR, RvTR,
RvTL, dT, vT};
F = {RFL, RFR, RvFR,
RvFL, dF, vF}.
Властивості еквівалентних перетво-
рень:
R⊥IR = {RL, RR, R⊥IL, R⊥IR, R⊥UL, R⊥UR,
R⊥RL, R⊥RR, , R⊥L, R⊥|R, R⊥L, R⊥R};
R⊥TF = {RL, RR, RL, RR, R⊥IL, R⊥IR,
R⊥IL, R⊥IR, R⊥UL, R⊥UR, R⊥UL, R⊥UR,
R⊥RL, R⊥RR, R⊥RL, R⊥RR, R⊥L, R⊥|R,
R⊥L, R⊥R, R⊥L, R⊥R, R⊥L, R⊥R};
RIR = {RL, RR, RIL, RIR, RUL, RUR, RRL,
RRR, RL, R|R, RL, R};
Програмна інженерія – теоретичні методи
32
RTF = {RL, RR, RL, RR, RIL, RIR,
RIL, RIR, RUL, RUR, RUL, RUR, RRL,
RRR, RRL, RRR, RL, R|R, RL,
RR, RL, RR, RL, RR}.
Властивості, пов’язані з предиката-
ми-індикаторами z:
I⊥IR = {R⊥vL, R⊥vR, R⊥tL, R⊥Tr;
R1L, R1R, R2L, R2R; ElRF, ElRT; ElF};
I⊥T = I⊥B{ElRT, ElT};
I⊥F = I⊥B{ElRF, ElF};
IIR = {R⊥vL, R⊥vR, R⊥tL, R⊥Tr; ElF}.
IT = IB{ElT};
IF = IB{ElF}.
Тут I⊥B = {R⊥vL, R⊥vR, R⊥vL,
R⊥vR, R⊥tL, R⊥tR, R⊥tL, R⊥tR; R1L,
R1R, R1L, R1R, R2L, R2R, R2L,
R2R; ElL, ElR};
IB = {RvL, RvR, RvL, RvR, RtL,
RtR, RtL, RtR}.
Маємо такі групи базових властиво-
стей для відношень логічного set-наслідку.
P
⊥|=IR: DIRR⊥IRI⊥IR⊥IR;
P
⊥|=T та R⊥|=T: DTFR⊥TFI⊥T⊥T;
P
⊥|=F та R⊥|=F: DTFR⊥TFI⊥F⊥F;
P
|=IR: DIRRIRIIRIR;
P
|=T та R|=T: DTFRTFITT;
P
|=F та R|=F: DTFRTFIFF.
Зауважимо, що 4 пари відношень
логічного set-наслідку мають однакові ба-
зові властивості; в цих парах відношення
типу T та типу F відрізняються різними
умовами гарантованої наявності.
Висновки
У роботі досліджено семантичні
властивості нових класів програмно-орієн-
тованих логік часткових квазіарних преди-
катів без обмеження монотонності. Їхньою
характерною особливістю є використання
часткових предикатів-індикаторів, які ви-
значають наявність у вхідних даних ком-
поненти з відповідним предметним іме-
нем, тобто з’ясовують означеність цього
імені. Описано композиційні алгебри та
мови цих логік, досліджено відношення
логічного наслідку для формул та для
множин формул мови. Розглянуто умови
гарантованої наявності цих відношень, на-
ведено їхні основні властивості. Особливу
увагу приділено властивостям, пов’язаним
із предикатами-індикаторами, та властиво-
стям елімінації кванторів. Властивості від-
ношень логічного наслідку є семантичною
основою побудови відповідних числень
секвенційного типу, що буде зроблено в
наступних роботах. Базові властивості пе-
вного відношення логічного наслідку про-
дукують секвенційні форми відповідного
числення, а умови гарантованої наявності
такого відношення індукують умови за-
мкненості секвенції в цьому численні.
Література
1. S. Abramsky, D.M. Gabbay, and
T.S.E. Maibaum (eds), Handbook of
Logic in Computer Science, Vol. 1–5,
Oxford University Press, 1993–2000.
2. М. С. Нікітченко, O. С. Шкільняк,
С. С. Шкільняк, Чисті першопорядкові
логіки квазіарних предикатів, Пробле-
ми програмування, 2016, № 2–3, C. 73–
86.
3. С. С. Шкільняк, Першопорядковi ком-
позиційно-номінативні логіки з преди-
катами слабкої та строгої рівності,
Проблеми програмування, 2019, № 3,
C. 28–44.
4. М. С. Нікітченко, O. С. Шкільняк,
C. С. Шкільняк, Cеквенційні числення
першопорядкових логік часткових пре-
дикатів з розширеними реномінаціями
та композицією предикатного допов-
нення, Проблеми програмування, 2020,
№ 2–3, C. 182–197.
5. O. Shkilniak, S. Shkilniak. First-Order
Sequent Calculi of Logics of Quasiary
Predicates with Extended Renominations
and Equality, UkrPROG2022, CEUR
Workshop Proceedings (CEUR-WS.org),
2023, pp. 3–18.
6. S.C. Kleene, Mathematical Logic, Dower
Publications, 2013.
References
1. S. Abramsky, D.M. Gabbay, and
T.S.E. Maibaum (eds), Handbook of
Logic in Computer Science, Vol. 1–5,
Oxford University Press, 1993–2000.
2. M. Nikitchenko, O. Shkilniak,
S. Shkilniak, Pure first-order logics of
quasiary predicates, in Problems in
Progamming, 2016, No 2–3. pp. 73–86.
Програмна інженерія – теоретичні методи
33
3. S. Shkilniak, First-order composition-
nominative logics with predicates of
weak equality and of strong equality, in
Problems in Progamming, 2019, No 3,
pp. 28–44.
4. M. Nikitchenko, O. Shkilniak,
S. Shkilniak, Sequent Calculi of First-
order Logics of Partial Predicates with
Extended Renominations and
Composition of Predicate Complement, in
Problems in Progamming, 2020, No 2–3,
pp. 182–197.
5. O. Shkilniak, S. Shkilniak. First-Order
Sequent Calculi of Logics of Quasiary
Predicates with Extended Renominations
and Equality, UkrPROG2022, CEUR
Workshop Proceedings (CEUR-WS.org),
2023, pp. 3–18.
6. S.C. Kleene, Mathematical Logic, Dower
Publications, 2013.
Одержано: 06.09.2024
Внутрішня рецензія отримана: 13.09.2024
Зовнішня рецензія отримана: 16.09.2024
Про автора:
Шкільняк Степан Степанович,
доктор фізико-математичних наук,
професор,
http://orcid.org/0000-0001-8624-5778.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
Тел. (+38) (044) 521-33-45
E-mail: ss.sh@knu.ua,
Сайт: csc.knu.ua
|