Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement
We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are cons...
Збережено в:
| Дата: | 2020 |
|---|---|
| Автори: | , , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2020
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/410 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-410 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/4d/f2c282ab8557fa9a265bb60f2315e64d.pdf |
| spelling |
pp_isofts_kiev_ua-article-4102021-09-29T18:01:01Z Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement Секвенційні числення першопорядкових логік часткових предикатів з розширеними реномінаціями та композицією предикатного доповнення Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. logic; partial predicate; logical consequence; sequent calculus; soundness; completeness UDC 004.42:510.69 логика; частичный предикат; логическое следствие; секвенциальное исчисление; корректность; полнота УДК 004.42:510.69 логіка; частковий предикат; логічний наслідок; секвенційне числення; коректність; повнота УДК 004.42:510.69 We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi.Problems in programming 2020; 2-3: 182-197 Исследованы новые классы программно-ориентированных логик – чистые первопорядковые логики частичных квазиарных предикатов с расширенными реноминациями и композицией предикатного дополнения. Описаны отношення логического следствия в таких логиках, для этих отношений построены исчисления секвенциального типа. Приведены базовые секвенциальные формы этих исчислений и условия замкнутости секвенций. Для предложенных исчислений доказаны теоремы корректности, теоремы о существовании контрмоделей и теоремы полноты.Problems in programming 2020; 2-3: 182-197 Досліджено нові класи програмно-орієнтованих логік – чисті першопорядкові логіки часткових квазіарних предикатів з розширеними реномінаціями та композицією предикатного доповнення. Описано відношення логічного наслідку в таких логіках, для цих відношень побудовано числення секвенційного типу. Наведено базові секвенційні форми цих числень та умови замкненості секвенцій. Для пропонованих числень доведено теореми коректності, теореми про існування контрмоделей та теореми повноти.Problems in programming 2020; 2-3: 182-197 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2020-09-16 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/410 10.15407/pp2020.02-03.182 PROBLEMS IN PROGRAMMING; No 2-3 (2020); 182-197 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2020); 182-197 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2020); 182-197 1727-4907 10.15407/pp2020.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/410/470 Copyright (c) 2020 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2021-09-29T18:01:01Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
logic partial predicate logical consequence sequent calculus soundness completeness UDC 004.42:510.69 |
| spellingShingle |
logic partial predicate logical consequence sequent calculus soundness completeness UDC 004.42:510.69 Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement |
| topic_facet |
logic partial predicate logical consequence sequent calculus soundness completeness UDC 004.42:510.69 логика частичный предикат логическое следствие секвенциальное исчисление корректность полнота УДК 004.42:510.69 логіка частковий предикат логічний наслідок секвенційне числення коректність повнота УДК 004.42:510.69 |
| format |
Article |
| author |
Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. |
| author_facet |
Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. |
| author_sort |
Nikitchenko, M.S. |
| title |
Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement |
| title_short |
Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement |
| title_full |
Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement |
| title_fullStr |
Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement |
| title_full_unstemmed |
Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement |
| title_sort |
sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement |
| title_alt |
Секвенційні числення першопорядкових логік часткових предикатів з розширеними реномінаціями та композицією предикатного доповнення |
| description |
We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi.Problems in programming 2020; 2-3: 182-197 |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2020 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/410 |
| work_keys_str_mv |
AT nikitchenkoms sequentcalculioffirstorderlogicsofpartialpredicateswithextendedrenominationsandcompositionofpredicatecomplement AT shkilniakos sequentcalculioffirstorderlogicsofpartialpredicateswithextendedrenominationsandcompositionofpredicatecomplement AT shkilniakss sequentcalculioffirstorderlogicsofpartialpredicateswithextendedrenominationsandcompositionofpredicatecomplement AT nikitchenkoms sekvencíjníčislennâperšoporâdkovihlogíkčastkovihpredikatívzrozširenimirenomínacíâmitakompozicíêûpredikatnogodopovnennâ AT shkilniakos sekvencíjníčislennâperšoporâdkovihlogíkčastkovihpredikatívzrozširenimirenomínacíâmitakompozicíêûpredikatnogodopovnennâ AT shkilniakss sekvencíjníčislennâperšoporâdkovihlogíkčastkovihpredikatívzrozširenimirenomínacíâmitakompozicíêûpredikatnogodopovnennâ |
| first_indexed |
2025-07-17T09:34:58Z |
| last_indexed |
2025-07-17T09:34:58Z |
| _version_ |
1850412801080688640 |
| fulltext |
Теоретичні і методологічні основи програмування
© М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк, 2020
ISSN 1727-4907. Проблеми програмування. 2020. № 2–3. Спеціальний випуск
УДК 004.42:510.69 https://doi.org/10.15407/pp2020.02-03.184
CЕКВЕНЦІЙНІ ЧИСЛЕННЯ ПЕРШОПОРЯДКОВИХ ЛОГІК
ЧАСТКОВИХ ПРЕДИКАТІВ З РОЗШИРЕНИМИ РЕНОМІНАЦІЯМИ
ТА КОМПОЗИЦІЄЮ ПРЕДИКАТНОГО ДОПОВНЕННЯ
М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк
Досліджено нові класи програмно-орієнтованих логік – чисті першопорядкові логіки часткових квазіарних предикатів з
розширеними реномінаціями та композицією предикатного доповнення. Описано відношення логічного н аслідку в таких
логіках, для цих відношень побудовано числення секвенційного типу. Наведено базові секвенційні форми цих числень та
умови замкненості секвенцій. Для пропонованих числень доведено теореми коректності, теореми про існування контрмоделей
та теореми повноти.
Ключові слова: логіка, частковий предикат, логічний наслідок, секвенційне числення, коректність, повнота.
Исследованы новые классы программно-ориентированных логик – чистые первопорядковые логики частичных квазиарных
предикатов с расширенными реноминациями и композицией предикатного дополнения. Описаны отношення логического
следствия в таких логиках, для этих отношений построены исчисления секвенциального типа. Приведены базовые секвенциальные
формы этих исчислений и условия замкнутости секвенций. Для предложенных исчислений доказаны теоремы корректности,
теоремы о существовании контрмоделей и теоремы полноты.
Ключевые слова: логика, частичный предикат, логическое следствие, секвенциальное исчисление, корректность, полнота.
We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations
and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi
of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness,
completeness, and counter-model existence theorems are proved for the introduced calculi.
Key words: logic, partial predicate, logical consequence, sequent calculus, soundness, completeness.
Вступ
Створено багато різноманітних логічних систем (див., напр., [1]), які з великим успіхом
застосовуються в інформатиці й програмуванні. Зазвичай для цього використовується класична логіка
предикатів [2] та базовані на її основі спеціальні логіки. Проте класична логіка має принципові обмеження,
що ускладнює її використання. Це висуває на перший план проблему побудови нових, програмно-
орієнтованих логік. Такими є логіки часткових квазіарних предикатів, будовані на базі спільного для логіки й
програмування композиційно-номінативного підходу [3]. Низку різноманітних класів логік квазіарних
предикатів описано, зокрема, в [3–6].
Для розв'язання низки задач, що виникають в інформаційних і програмних системах, необхідний
ефективний пошук виведень. Продуктивним апаратом побудови виведень є числення секвенційного
(ґенценівського) типу. Ці числення формалізують фундаментальне поняття логічного наслідку. Розроблено
(див., напр., [4–6]) низку секвенційних числень для різних класів програмно-орієнтованих логік. Побудова
секвенційних числень для нових класів таких логік: чистих першопорядкових логік квазіарних предикатів з
розширеними реномінаціями та композицією предикатного доповнення, – мета даної роботи. Характерна
особливість цих логік – це наявність спеціальної немонотонної операції (композиції) предикатного
доповнення . Операції подібного типу знайшли використання в розширеннях програмних логік
Флойда-Хоара [7, 8] на випадок часткових перед- та після-умов. Логіки часткових предикатів з композицією
предикатного доповнення запропоновано в [9, їх названо LC. Пропозиційні LC детально описано в [9,
реномінативні та чисті першопорядкові LC розглянуто в [10 і [11], різноманітні відношення логічного
наслідку в LC досліджено в [12].
Чисті першопорядкові логіки квазіарних предикатів назвемо L
Q
(logics of quantifier level).
Визначальною їх особливістю є наявність композицій квантифікації. L
Q
із розширеними реномінаціями та
предикатами-індикаторами наявності значення для змінних назвемо L
Q
, L
Q
із композицією предикатного
доповнення назвемо L
QС
. В роботі побудовано низку секвенційних числень в L
Q
та в L
QС
, для таких
числень доведено теореми коректності й повноти. Основний акцент ми робимо на побудові секвенційних
числень в L
QС
.
Поняття, які в цій роботі не визначаються, тлумачимо в сенсі [6, 9, 12]. Для полегшення читання
наведемо потрібні для подальшого викладу визначення.
182
Теоретичні і методологічні основи програмування
1. Композиційні системи та мови чистих першопорядкових логік
V-A-квазіарний предикат – це часткова неоднозначна функція вигляду Q :
V
A {T, F}. Тут
V
A – множина
всіх V-A-іменних множин, {T, F} – множина істиннісних значень. Множину всіх значень, які неоднозначний
предикат Q може приймати на аргументі (даному) d
V
А, позначаємо Q[d].
V-A-іменна множина (V-A-ІМ) – це часткова однозначна функція вигляду d
:
V A. Тут V і A – множини
предметних імен і предметних значень. ІМ подаємо як [v1a1,...,vnan,...], де vіV, aіA, vі vj при і j.
Для ІМ задамо операцію ||–Z видалення компонент з іменами із Z V: d ||–Z = {v ad | vZ}.
Параметризовану операцію розширеної реномінації 1 1
1
,..., , ,...,
,..., , ,...,
r :n m
n
v v u u
x x
V
А
V
A, де усі vi, xi, uj V, задаємо [5]
так: 1 1
1
,..., , ,...,
,..., , ,...,
r ( )n m
n
v v u u
x x
d
1 1{ ,..., , ,..., }||
n mv v u ud 1 1[ ( ),..., ( )]n nv d x v d x . Зокрема, r ( ) || . x
xd d
Символ V означає відсутність значення. Якщо тут d(xі), то компонента з іменем vі відсутня.
Введемо для y1,..., yn позначення y . Тоді замість 1 1
1
,..., , ,...,
,..., , ,...,
r n m
n
v v u u
x x
пишемо ,
,rv u
x .
Традиційна [2–4] операція реномінації r
v
x є окремим випадком операції ,
,rv u
x .
Твердження 1. За умови d(z) маємо
, , , ,
, , , ,r ( ) r ( )
v u y v u y
x z xd d та
, , ,
, , ,r ( ) r ( )v u z v u
x xd d .
Послідовне застосування двох операцій , , , , , ,
, , , , , ,r та ru s w t v s z t
x a y c можна подати [5] у вигляді однієї, яку
позначимо , , , , , ,
, , , , , ,ru s w t v s z t
x a y c і назвемо згорткою
, , ,
, , ,ru s w t
x a та
, , ,
, , ,rv s z t
y c . Для всіх d
V
A маємо
, , , , , , , , , , ,
, , , , , , , , , , ,r ( ) r ( )u s w t v s z t u s v w z t
x a y c p q yd d .
В цій роботі розглядаємо неоднозначні предикати реляційного типу – R-предикати [3, 6]. Їх трактуємо як
відношення між
V
A та множиною {T, F}. Кожний R-предикат Q можна задати за допомогою 2-х множин: області
істинності T(Q) = {d | TQ[d]} та область хибності F(Q) = {d | FQ[d]}. Oбласть невизначеності R-предикатa Q
визначається так: ( ) ( ) ( )Q T Q F Q . R-предикат Q монотонний, якщо маємо: d1 d2 Q[d1] Q[d2].
Ім'я хV неістотне для R-предиката Q, якщо для всіх d1, d2
V
A маємо: d1 ||–х = d2 ||–х Q[d1] = Q[d2].
R-предикат Q частковий однозначний, або P-предикат, якщо T(Q)F(Q) = ;
R-предикат Q тотальний, або T-предикат, якщо T(Q)F(Q) =
V
A;
R-предикат Q тотальний однозначний, або TS-предикат, якщо T(Q)F(Q) = та T(Q)F(Q) =
V
A;
Маємо 4 константних R-предикати T, F, , ; вони задаються так:
T(F) = F(T) = ( ) ( )T F ; T(T) = F(F) = T() = F() =
V
А.
P-предикат Q назвемо частковим константним, якщо F(Q) = або T(Q) = .
Класи V-A-квазіарних R-предикатів, P-предикатів, T-предикатів TS-предикатів далі позначаємо Pr
V–A
,
PrP
V–A
, PrT
V–A
, PrTS
V–A
. Клас PrTS
V–A
вироджений: усі TS-предикати, окрім константних T та F, немонотонні.
Базові композиції. Базовими композиціями L
Q
є пропозиційні композиції (логiчні зв’язки) та ,
розширені реномінації
,
,R ,v u
x квантори x, та спеціальні 0-арні композиції – предикати-індикатори Ez. Базовими
композиціями L
QС
є базові композиції L
Q
та спеціальна композиція предикатного доповнення .
Логічні зв’язки та задамо через області істинності й хибності відповідних предикатів так:
T(P) = F(P); F(P) = T(P); T(PQ) = T(P)T(Q); F(PQ) = F(P)F(Q).
Композиція
,
,R :v u V A V A
x Pr Pr
розширеної реномінації задається умовою:
, ,
, ,R ( )[ ] [r ( )]v u v u
x xP d P d .
Предикати Ez визначають наявність у вхідних даних компоненти з відповідним zV; задаємо їх так:
T(Ez) = {d | d(z)}; F(Ez) = {d | d(z)}.
Предикати-індикатори Ez тотальні, однозначні, немонотонні.
Композиція квантифікації (квантор) xP : V A V APr Pr задається так:
T(xP) = { | || ( )}x
a A
d d x a T P
; F(xP) = { | || ( )}x
a A
d d x a F P
.
183
Теоретичні і методологічні основи програмування
Спеціальна немонотонна 1-арна композиція предикатного доповнення задається так:
( ) ( ) ( ) ( ) ( ) ( )T P P T P F P T P F P ; ( )F P .
Mножинами базових композицій L
Q
та L
QС
є CQ = {, ,
,
,R ,v u
x x, Ex} та CQC = {, ,
,
,R ,v u
x x, , Ex}.
Твердження 2. Композиції , ,
,
,R ,v u
x xP зберігають тотальність і монотонність предикатів.
Таким чином, класи PrP
V–A
, PrT
V–A
, PrTS
V–A
замкнені щодо композицій CQ. Водночас
Твердження 3. QPr
V–A
QPrP
V–A
; QPrT
V–A
Q .
Отже, класи PrT
V–A
та PrTS
V–A
незамкнені щодо . Тому для T-предикатів та TS-предикатів LC не мають
смислу. В силу незамкненості PrTS
V–A
та PrT
V–A
щодо , враховуючи дуальність [6] класів PrP
V–A
та PrT
V–A
і
виродженість PrTS
V–A
, далі будемо розглядати лише логіки R-предикатів та логіки P-предикатів.
Маємо композиційні системи (
V
A, Pr
V–A
, CQ), (
V
A, PrP
V–A
, CQ), (
V
A, Pr
V–A
, CQC), (
V
A, PrP
V–A
, CQC).
задаютьсистемиТакі першопорядковчисті алгебрикомпозиційніі A
Q
= (
V
A, Pr
V–A
, CQ), A
QC
=
= (
V
A, Pr
V–A
, CQC), A
QP
= (
V
A, PrP
V–A
, CQ), A
QCP
= (
V
A, PrP
V–A
, CQC); при цьому A
QP
та A
QCP
– підалгебри
алгебр A
Q
та A
QC
.
Основні властивості пропозиційних композицій та кванторів, не пов’язані з реномінаціями, аналогічні
властивостям класичних логічних зв’язок та кванторів (див. [3]).
Теорема 1. Маємо такі базові властивості, пов’язані з композицією розширеної реномінації:
R) R(P) = P – тотожна реномінація;
RI)
, , ,
, , ,R ( ) R ( )z v u v u
z x xP P – згортка тотожної пари імен у реномінації;
RU) Нехай zV неістотне для предиката Р; тоді , , ,
, , ,R ( ) R ( )z v u v u
y x xP P ;
R) за умови d(z) маємо
, , , ,
, , , ,R ( )( ) R ( )( )
v u y v u y
x z xP d P d та
, , ,
, , ,R ( )( ) R ( )( )v u z v u
x xP d P d ;
RR) , , , ,
, , , ,R (R ( )) R ( )v z u t v z u t
y x y xP P – згортка реномінацій; тут , , , ,
, , , ,R ( )( ) ( ( ))v z u t u t v z
y x x yP d P r d ;
R)
, ,
, ,R ( ) R ( )v u v u
x xP P – R-дистрибутивність;
R)
, , ,
, , ,R ( ) R ( ) R ( )v u v u v u
x x xP Q P Q – R-дистрибутивність;
R )
, ,
, ,R ( ) R ( )v u v u
x xQ Q – R -дистрибутивність.
Теорема 2. Маємо такі властивості, пов’язані з композиціями реномінації та квантифікації:
Ren) якщо z неістотне для P, то R ( )y
zyP z P – перейменування кванторного імені;
Rs)
, ,
, ,R ( ) R ( )v u v u
x xy P yP за умови { , , }y v x u – проста (обмежена) R-дистрибутивність;
R)
, ,
, ,R ( ) R ( ),v u v u y
zx xyP z P якщо z неістотне для P та { , , }z v x u – -дистрибутивність;
UR)
, , , ,
, , , ,R ( ) R ( )
y v u y v u
z x z xy P P за умови { , }y z x – неістотність верхніх імен в реномінаціях.
Твердження 4. Маємо такі властивості реномінації предикатів-індикаторів:
, ,
, ,R ( ) F;v u z
x Ez , ,
, ,R ( )v u z
x y Ez Ey ;
, ,
| , , ( ) .v u y
xR p H якщо { , }.z v u
Eлімінація кванторів базується на таких властивостях.
Теорема 3.
, ,
, ,(R ( ))u w x
v yT P T(Ey)
, , ,
, , ,r ( ) r ( ).v u y v u
x x та
,
| , ( ) .v u
xR p H T(Ey) , ,
, ,(R ( ))u w x
v yF P .
Мови L
QC
. Алфавiт мови L
QС
утворюють множини V предметних імен (змінних), Ps предикатних
символів, Cs = {, ,
,
, ,
v u
xR ,x, Ex} символів базових композицій. Індуктивне визначення множини Fr формул:
– кожний рPs та кожний Ex є формулою; такі формули назвемо атомарними;
184
Теоретичні і методологічні основи програмування
– нехай , Fr; тоді Fr, Fr, ,
, ,v u
xR Fr xFr, Fr .
Для L
QС
задамо множину VT
V імен, неістотних для всіх рPs – множину тотально неістотних імен. Для
визначення множин гарантовано неістотних для формул імен таку продовжуємо [3, 6] до : Fr2
V
.
Якщо х(), то (див. [3, 6]) х неістотне для . Розширена сигнатура мови – це = (V, VT, Cs, Ps).
Формула примітивна, якщо вона атомарна або має вигляд ,
,
v u
xR p де рPs,
,
,
v u
xR не має пар тотожних
імен та { , } ( )v u p . Формула – СF-формула (constant free), якщо не містить символів 0-арних
композицій-констант, тобто символів Ex у випадку мови L
QС
. Формули вигляду ,
,
v u
xR назвемо R-формулами.
Інтерпретації. Інтерпретуємо мову L
QC
на композиційних системах CS = (
V
A, Pr
V–A
, CQC). Символи Cs
інтерпретуємо як відповідні композиції, символи Ex – як відповідні предикати-індикатори Ex. Задаємо тотальне
однозначне I : Ps Pr
V–A
, яке продовжимо до відображення інтерпретації формул I : Fr Pr
V–A
:
I() = (I()), I() = (I(), I()),
, ,
, ,( ) R ( ( )),v u v u
x xI R I I(х) = х(I()), ( ) ( ( )) I I .
Трійку J = (CS, , I) назвемо інтерпретацією мови L
QC
. Cкорочено інтерпретації мови позначаємо (A, I).
Ім'я xV неістотне для формули , якщо при кожній інтерпретації J ім'я x неістотне для предиката J.
Kласи інтерпретацій мови називають семантиками. Для L
QС
маємо загальний клас R-інтерпретацій –
семантику RС. Виділення підалгебр P-предикатів виділяє підклас P-інтерпретацій – семантику PС.
Для L
Q
маємо загальний клас R-інтерпретацій – семантику R. Виділення підалгебр P-предикатів,
T-предикатів, TS-предикатів виділяє семантики P, T, TS. Далі семантики T та TS явно не розглядаємо.
Формули, які завжди інтерпретуються як константні предикати, назвемо константними. Можна виділити
T-формули, F-формули, -формули. Наприклад, Ex Ex – T-формулa;
, ,
, , ( )v u z
xR Ez – F-формула, Ez – -
формулa.
Формули, які завжди інтерпретуються як тотальний предикат, позначаємо ; зокрема, це Ez, T-формули
та F-формули. Формули, в яких F(J) = для всіх J, позначаємо F; зокрема, це всі формули . Формули, в
яких T(J) = для всіх J, їх позначаємо T; зокрема, це всі формули .
Мову L
Q
визначаємо аналогічно мові L
QС
, лише опускаємо пункти для символів .
Un-формули. Нехай , , , ,
, , , ,
( )x v u w z
x y t
R
– R-формула така, що { , } ( ) u w , причому не є символом Ez.
R-формулу ,
, ( ),v z
yR утворену із , , , ,
, , , ,
( )x v u w z
x y t
R
всеможливими спрощенням зовнішньої реномінації на основі
R, RI, RU, назвемо Rs-формою R-формули , , , ,
, , , ,
( )x v u w z
x y t
R
. Rs-форми R-формул назвемо Rs-формулами.
Твердження 5. Якщо – Rs-форма R-формули , то J = J для всіх інтерпретацій J.
Нехай Un V – множина імен, які трактуємо як неозначені. Кожну Rs-формулу можна подати у вигляді
, , , ,
, , , ,
r z x u w
s v yR , де { , , , } , { , , } r s y u Un x v w Un . Формулу
, ,
, ,
z x w
vR назвемо Un-формою формули
, , , ,
, , , ,
r z x u w
s v yR .
Примітивні Un-формули мають вигляд
,
, ,
z x
vR p де { , } x v Un , pPs.
Формули та Un-еквівалентні (позн. Un ), якщо для всіх J = (A, І) та d
V
A ||–Un маємо J (d) = J (d).
Твердження 6. Якщо – Un-форма формули , то Un .
Un-форму
, ,
, ,
z x w
vR можна отримати із Rs-формули
, , , ,
, , , ,
r z x u w
s v yR перетвореннями згідно R. Звідси
Твердження 7. Нехай zUn, тоді
, , , ,
, , , , v u y v u y
x z Un xR R та
, , ,
, , ,
v u z v u
x Un xR R .
2. Відношення логічного наслідку
На множинах формул мов L
Q
та L
QC
, можна визначити низку відношень логічного наслідку. Зокрема, на
ці мови поширюються [12] відомі [6] відношення
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF, визначені в мовах L
Q
.
185
Теоретичні і методологічні основи програмування
Далі для стислості запису в назвах відношень не пишемо символ .
Спочатку задамо відношення наслідку для двох множин формул при фіксованій інтерпретації J.
Нехай , , Fr, нехай J – інтерпретація. Далі позначаємо:
( )
JT як T
(J), ( )JF
як F
(J), ( )
JT як T
(J), ( )
JF як F
(J).
є IR-наслідком при інтерпретації J (позн. J|=IR ), якщо T
(J) F
(J) = .
є T-наслідком при інтерпретації J (позн. J|=T ), якщо T
(J) T
(J).
є F-наслідком при інтерпретації J (позн. J|=F ), якщо F
(J) F
(J).
є TF-наслідком при інтерпретації J (позн. J|=TF ), якщо J|=T та J|=F .
Відповідні відношення логічного -наслідку в семантиці визначаємо за схемою:
|= , якщо J|= для кожної J.
Далі – це одна із R, P, RС, PС. Маємо по 8 відношень логічного наслідку в L
Q
та в L
QC
:
P
|=IR,
P
|=T,
P
|=F,
P
|=TF;
R
|=IR,
R
|=T,
R
|=F,
R
|=TF ;
Pс
|=IR,
Pс
|=T,
Pс
|=F,
Pс
|=TF;
Rс
|=IR,
Rс
|=T,
Rс
|=F,
Rс
|=TF .
Деякі з цих відношень вироджені, деякі відношення збігаються (див. [12]). Зокрема:
Твердження 8. Якщо та складаються з CF-формул, які не мають входжень , то
R
|IR та
Rс
|IR .
Водночас Ez, Ez J|=IR та J|=IR Ez, Ez для кожної J. Отже,
Rс
|=IR та
R
|=IR мають вироджений характер.
Приклад 1. Для всіх Fr та JRС маємо ( ) ,JF ( ) ,JT T(J) ( )JT = (J),
F(J) ( )JF = (J). Звідси
Rc
|=F та
Rс
|=T , проте
Rс
|T та
Rс
|F .
В логіці L
Q
маємо 5 різних невироджених відношень:
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF .
В логіці L
QС
маємо 7 різних невироджених відношень:
Pс
|=IR,
Pс
|=T,
Pс
|=F,
Pс
|=TF,
Rс
|=T,
Rс
|=F,
Rс
|=TF .
Діаграми Гассе для цих відношень можна подати так (тут замість вживаємо стрілку ):
P
|=T
Rc
|=T
Pc
|=T
R
|=TF
P
|=TF
P
|=IR
Rc
|=TF
Pc
|=TF
Pс
|=IR
P
|=F
Rс
|=F
Pс
|=F
Водночас для відношення
Pс
|=IR неможливо зробити декомпозицію (див. [12]). Така декомпозиція
вимагає явного виділення області невизначеності, що веде до загальнішого відношення |=IR
неспростовнісного
логічного наслідку за умов невизначеності (див. [9]). Для відношення |=IR
побудовано [9–11] секвенційні
числення пропозиційного, реномінативного, першопорядкового рівнів.
Введено також [12] відношення логічного наслідку за умов невизначеності
Pс
|=T
,
Pс
|=F
,
Rс
|=T
,
Rс
|=F
. Для
цих відношень доведена [12] теорема про елімінацію умов невизначеності, що дає змогу промоделювати їх за
допомогою відношень
Pc
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F.
Відношення логічного наслідку для пар формул індукують відношення логічної еквівалентності.
Відношення -еквівалентності при інтерпретації J визначаємо так: J , якщо J|= та J|= .
Відношення логічної -еквівалентності в семантиці визначаємо так:
, якщо
|= та
|= .
Особливе значення має відношення J TF . Справді, JTF T(J) = T(J) та F(J) = F(J) J = J .
Основа еквівалентних перетворень в L
Q
та L
QС
– теореми еквівалентності та заміни еквівалентних.
Теорема 4. Нехай ' отримано з формули заміною деяких входжень 1, ..., n на 1, ..., n. Якщо
1
1, ..., n
n, то
' (тут
одне з
R
TF,
P
TF,
P
IR,
Rс
TF,
Pс
TF,
Pс
IR).
Теорема 5. Нехай TF , тоді маємо: , |= , |= ; |= , |=, .
Тут і далі TF – одне з відношень типу TF, |= – довільне відношення логічного наслідку.
186
Теоретичні і методологічні основи програмування
Розглянемо властивості відношень логічного наслідку.
M) Якщо , та |=
, то |= – монотонність.
Теорема 6. Базові властивості декомпозиції формул:
L) , |= , |= ; R) |= , |= , ;
L) , |= , |= та , |= ; R) |= , |= , , ;
L) (), |= , , |= ; R) |= , () |= , та |= , .
Для відношень типу IR додатково маємо (ці властивості невірні для відношень типів T, F, TF):
L) , |=IR |=IR , . R) |=IR , , |=IR .
Далі
с#
|=T – це
Pс
|=T чи
Rc
|=T,
с#
|=F – це
Pc
|=F,
Rc
|=T,
Rc
|=F.
с#
|=TF – це
Pс
|=TF чи
Rc
|=TF.
Теорема 7. Властивості декомпозиції формул :
LT) ,
с#
|=T
с#
|=T , , ; RT)
с#
|=T , ,
с#
|=T та ,
с#
|=T ;
RF)
с#
|=F , , ,
с#
|=F ; LF) ,
с#
|=F
с#
|=T , та
с#
|=T , .
Теорема 8. Властивості елімінації формул :
El)
с#
|=T ,
с#
|=T ; El) ,
с#
|=F
с#
|=F .
Твердження 9. Властивості гарантованої наявності відповідного відношення логічного наслідку:
#) | ,c
FC ; #) , |c
TC .
Aсиметрична поведінка композиції щодо областей істинності й хибності предикатів дає різні
властивості декомпозиції формул для відношень T та типу F, які не можна подати як спільну властивість
для відношень типу TF. Тому для відношень
с#
|=TF декомпозиція можлива лише окремо для
с#
|=T та для
с#
|=F.
Отже, секвенційні числення для відношень
с#
|=TF є поєднаннями числень для відношень
с#
|=T та для
с#
|=F.
Далі розглядаємо такі відношення:
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF в L
Q
та
Pс
|=T,
Pс
|=F,
Rс
|=T,
Rс
|=F в L
QС
.
Важливі для побудови числень властивості еквівалентних перетворень отримуємо на основі властивостей
R, RI, RU, RR, R, R, R для предикатів. Кожна така властивість R продукує 4 відповідні
властивості RL, RR, RL, RR для відношення логічного наслідку, коли виділена формула чи її
заперечення знаходиться у лівій чи правій частині цього відношення, а R продукує 8 властивостей. В кожній
інтерпретації предикати, що є значеннями виділених формул, збігаються. Для прикладу наведемо властивості,
продуковані R:
R1)
, ,
, , ( ),
v u y
x zR |= , Ez
, ,
, , ( ),
v u y
xR |= , Ez; |= ,
, ,
, , ( ),
v u y
x zR Ez |= ,
, ,
, , ( ), ;
v u y
xR Ez
R1)
, ,
, , ( ),
v u y
x zR |= , Ez
, ,
, , ( ),
v u y
xR |= , Ez; |= ,
, ,
, , ( ),
v u y
x zR Ez |= ,
, ,
, , ( ), ;v u z
xR Ez
R2)
, ,
, , ( ),v u z
xR |= , Ez
,
, ( ),v u
xR |= , Ez; |= ,
, ,
, , ( ),v u z
xR Ez |= ,
,
, ( ), ;v u
xR Ez
R2)
, ,
, , ( ),v u z
xR |= , Ez
,
, ( ),v u
xR |= , Ez; |= ,
, ,
, , ( ),v u z
xR Ez |= ,
,
, ( ), ;v u
xR Ez
Bластивості зняття в Ez і в
,
,R ( )v u
w Ez та властивості спрощення реномінації предикатів-індикаторів:
E) Ez, |= |= , Ez; |= , Ez Ez, |= ;
, ,
R E , ,¬ ) ( ), | | ( ),v u v u
w wR Ez R Ez ;
, ,
, ,| ( ), ( ), |v u v u
w wR Ez R Ez ;
,
E ,R ) ( ), | , | , де { , };v u
xR Ez Ez z v u
,
,| , ( ) | , , де { , }v u
xR Ez Ez z v u ;
, ,
Ev , ,R ) ( ), | , | ;v u z
x yR Ez Ey , ,
, ,| , ( ) | ,v u z
x yR Ez Ey .
187
Теоретичні і методологічні основи програмування
Властивості елімінації кванторів, E-розподілу та первісного означення:
L) х, |= ( ), ,x
zR Ez |= за умови zfu(, , х));
RL)
,
, ( ),v u
wR x |=
, ,
, , ( ), ,v u x
w zR Ez |= за умови
,
,( , , ( ))v u
wz fu R x ;
R) |= х, , Ez |= ( ),x
zR за умови zfu(, , х));
RR) |=
,
, ( ),v u
wR x , Ez |=
, ,
, , ( ),v u x
w zR за умови
,
,( , , ( ))v u
wz fu R x ;
vR) , Ey |= х, , Ey |= х, ( ),x
yR ;
RvR) , Ey |=
,
,, ( )v u
wR x , Ey |= ;
vL) х, Ey, |= , ( ), ,x
yx R Ey |= ;
RvL)
,
, ( ), ,v u
wR x Ey |= , , ,
, , ,( ), ( ), ,v u v u x
w w yR x R Ey |= ;
Ed) |= |= , Ey та Ey, |= ; Ev) |= Ez, |= , де zfu(, ).
Опишемо властивості, які гарантують наявність відношення логічного наслідку.
С) , |= , – вірна для всіх розглянутих відношень логічного наслідку.
Додатково гарантують наявність відповідного відношення такі властивості:
СL) , ,
P
|=T ; , ,
Pс
|=T ;
СR)
P
|=F , , ;
Pс
|=F , , ;
СLR) , ,
P
|=TF , , .
Низку властивостей, які гарантують наявність логічного наслідку, отримуємо на основі властивостей
константних і частково-константних предикатів. Це наведені вище C і C та властивість
CF)
, ,
*, , ( ), |v u z
xR Ez – вірна для всіх розглянутих відношень логічного наслідку.
На основі цих властивостей отримуємо умови гарантованої наявності того чи іншого відношення:
С) існує формула : та – гарантує |=* для кожного з розглянутих відношень;
СL) існує формула : та – гарантує
P
|=T та
Pс
|=T ;
СR) існує формула : та – гарантує
P
|=F та
Pс
|=F ;
СLR) існують формули , : , та , – – гарантує
P
|=TF ;
СF) існує формула
, ,
, , ( )v u z
xR Ez – гарантує |=* для кожного з розглянутих відношень;
C ) – гарантує
Pс
|=F та
Rс
|=F ;
C ) – гарантує
Pс
|=T та
Rс
|=T .
3. Першопорядкові секвенційні числення
Секвенційні числення формалізують відношення логічного наслідку для множин формул. Будуємо
числення в стилі семантичних таблиць, трактуючи секвенції як множини формул, специфікованих (відмічених)
спеціальними символами |– та –| . Позначаємо секвенції як |––|, скорочено . Формули із (відмічені |–) назвемо
T-формулами, а формули із (відмічені –|) – F-формулами. Це відповідає семантичному трактуванню формул із
як істинних, а формул із – як хибних. Секвенційні числення будуємо так: секвенція |––| вивідна |= .
Введемо для множини специфікованих формул = |––| множини означених імен та неозначених імен, або
val-змінних та unv-змінних: val(|––|) = {xV | Ex}; unv(|––|) = {xV | Ex}.
Множину нерозподілених для імен введемо так: ud() = nm() \ (val() unv()).
188
Теоретичні і методологічні основи програмування
Виведення в секвенційних численнях має вигляд дерева, вершинами якого є секвенції. Секвенція
вивідна, або має виведення, якщо існує замкнене секвенційне дерево з коренем – виведення секвенції .
Секвенційне дерево замкнене, якщо кожний його лист – замкнена секвенція.
Секвенційне числення задається базовими секвенційними формами і умовами замкненості секвенції.
Замкнені секвенції є аксіомами секвенційного числення. Замкненість |––| має гарантувати |= .
Правилами виведення секвенційних числень є секвенційні форми. Вони є синтаксичними аналогами
властивостей відношень логічного наслідку. Секвенційні форми записуємо у вигляді
або
.
Для відношень
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF в L
Q
ми маємо числення С
QIR
, С
QT
, С
QF
, С
QTF
, С
QTFR
.
Для відношень
Pс
|=T,
Pс
|=F,
Rс
|=T,
Rс
|=F в L
QС
маємо відповідно числення С
QСT
, С
QСF
, С
QCTR
, С
QСFR
.
Умови замкненості секвенції. Умови замкненості секвенції |––| в численнях відповідають умовам
гарантованої наявності відповідного відношення логічного наслідку. Звідси такі умови замкненості:
– числення С
QIR
: умова C CF (ця умова гарантує наявність
P
|=IR );
– числення С
QT
: умова C CF CL (ця умова гарантує наявність
P
|=T );
– числення С
QF
: умова C CF CR (ця умова гарантує наявність
P
|=F );
– числення С
QTF
: умова C CF CLR (ця умова гарантує наявність
P
|=TF );
– числення С
QTFR
: умова C CF (ця умова гарантує наявність
R
|=TF );
– числення С
QCT
: умова C CF CL C (ця умова гарантує наявність
Pc
|=T );
– числення С
QCF
: умова C CF CR C (ця умова гарантує наявність
Pc
|=F );
– числення С
QCTR
: умова C CF C (ця умова гарантує наявність
Rc
|=T );
– числення С
QCFR
: умова C CF C (ця умова гарантує наявність
Rc
|=F ).
Умови C, CF, CL, CR, CLR, C , C наведені вище.
Базові секвенційні форми числень С
QT
, С
QF
, С
QTF
, С
QTFR
. Властивості відношень логічного наслідку
індукують відповідні секвенційні форми. Спочатку опишемо базові форми числень С
QT
, С
QF
, С
QTF
, С
QTFR
. Ці
числення мають однакові базові секвенційні форми, а відрізняються різними умовами замкненості секвенції.
Форми спрощення (для форм типу RU умова: у()):
|–R
|
|
,
( ),R
; –|R
|
|
,
( ),R
; |–R
|
|
,
( ),R
; –|R
|
|
,
( ),R
;
|–RI
,
| ,
, ,
| , ,
( ),
( ),
v u
x
z v u
z x
R
R
; –|RI
,
| ,
, ,
| , ,
( ),
( ),
v u
x
z v u
z x
R
R
; |–RI
,
| ,
, ,
| , ,
( ),
( ),
v u
x
z v u
z x
R
R
–|RI
,
| ,
, ,
| , ,
( ),
( ),
v u
x
z v u
z x
R
R
;
|–RU
,
| ,
, ,
| , ,
( ),
( ),
v u
x
y v u
z x
R
R
; –|RU
,
| ,
, ,
| , ,
( ),
( ),
v u
x
y v u
z x
R
R
; |–RU
,
| ,
, ,
| , ,
( ),
( ),
v u
x
y v u
z x
R
R
; –|RU
,
| ,
, ,
| , ,
( ),
( ),
v u
x
y v u
z x
R
R
;
|–R1
, ,
| |, ,
, ,
| |, ,
( ), ,
,
( ), ,
v u y
x
v u y
x z
R p Ez
R p Ez
де pPs; –|R1
, ,
| |, ,
, ,
| |, ,
( ), ,
,
( ), ,
v u y
x
v u y
x z
R p Ez
R p Ez
де pPs;
|–R1
, ,
| |, ,
, ,
| |, ,
( ), ,
,
( ), ,
v u y
x
v u y
x z
R p Ez
R p Ez
де pPs; –|R1
, ,
| |, ,
, ,
| |, ,
( ), ,
,
( ), ,
v u y
x
v u y
x z
R p Ez
R p Ez
де pPs;
|–R2
,
| |,
, ,
| |, ,
( ), ,
,
( ), ,
v u
x
v u z
x
R p Ez
R p Ez
де pPs; –|R2
,
| |,
, ,
| |, ,
( ), ,
,
( ), ,
v u
x
v u z
x
R p Ez
R p Ez
де pPs;
189
Теоретичні і методологічні основи програмування
|–R2
,
| |,
, ,
| |, ,
( ), ,
,
( ), ,
v u
x
v u z
x
R p Ez
R p Ez
де pPs; –|R2
,
| |,
, ,
| |, ,
( ), ,
,
( ), ,
v u
x
v u z
x
R p Ez
R p Ez
де pP.
Форми еквівалентних перетворень:
|–RR
, ,
| , ,
, ,
| , ,
( ),
( ( )),
v z u t
y x
v z u t
y x
R
R R
; –|RR
, ,
| , ,
|
( ),
( ( )),
v z u t
y x
v w
x y
R
R R
; |–RR
, ,
| , ,
, ,
| , ,
( ),
( ( )),
v z u t
y x
v z u t
y x
R
R R
; –|RR
, ,
| , ,
, ,
| , ,
( ),
( ( )),
v z u t
y x
v z u t
y x
R
R R
;
|–R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
; –|R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
; |–R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
; –|R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
;
|–R
, ,
| , ,
,
| ,
( ) ( ),
( ),
v u v u
x x
v u
x
R R
R
; –|R
, ,
| , ,
,
| ,
( ) ( ),
( ),
v u v u
x x
v u
x
R R
R
;
|–R
, ,
| , ,
,
| ,
( ( ) ( )),
( ),
v u v u
x x
v u
x
R R
R
; –|R
, ,
| , ,
,
| ,
( ( ) ( )),
( ),
v u v u
x x
v u
x
R R
R
.
Форми зняття в формулах вигляду Ey та
,
, ( )v u
xR Ez :
|–E
|
|
,
,
Ez
Ez
; –|E
|
|
,
,
Ez
Ez
; |–RE
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R Ez
R Ez
; –|RE
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R Ez
R Ez
.
Форми cпрощення реномінації предикатів-індикаторів (для форм |–RE та –|RE умова: { , }z v u ):
|–RE
|
,
| ,
,
( ),v u
x
Ez
R Ez
; –|RE
|
,
| ,
,
( ),v u
x
Ez
R Ez
; |–REv
|
, ,
| , ,
,
( ),v u z
x y
Ey
R Ez
; –|REv
|
, ,
| , ,
,
( ),v u z
x y
Ey
R Ez
.
Форми декомпозиції формул:
|
|
|
,
,
; |
|
|
,
,
; |
| |
|
, ,
,
; |
| |
|
, ,
,
;
|
| |
|
, ,
( ),
; |
| |
|
, ,
( ),
;
Форми елімінації кванторів:
|
| |
|
( ), ,
,
x
zR Ez
x
; |
| |
|
( ), ,
,
x
zR Ez
x
; |–R
, ,
| |, ,
,
| ,
( ), ,
( ),
v u x
w z
v u
w
R Ez
R x
; –|R
, ,
| |, ,
,
| ,
( ), ,
( ),
v u x
w z
v u
w
R Ez
R x
;
|v
| | |
| |
, , ( ),
, ,
x
yx Ey R
x Ey
; |v
| | |
| |
, , ( ),
, ,
x
yx Ey R
x Ey
;
|–Rv
, , ,
| | |, , ,
,
| |,
( ), ( ), ,
( ), ,
v u v u x
w w y
v u
w
R x R Ey
R x Ey
; –|Rv
, , ,
| | |, , ,
,
| |,
( ), ( ), ,
( ), ,
v u v u x
w w y
v u
w
R x R Ey
R x Ey
.
Форми |–R, –|R, |–, –| назвемо T-формами; форми –|v, |–v, –|Rv, |–Rv назвемо F-формами.
Для |–, –| умова: zfu(, x); для |–R, –|R умова: zfu
,
,( , ( ))v u
wR x ; для F-форм Ey не входить до .
Допоміжні форми E-розподілу Ed та первісного означення Ev:
| |, ,
Ed
Ex Ex
; Ev
| ,
Ez
за умови: zfu().
190
Теоретичні і методологічні основи програмування
Базові секвенційні форми числення С
QIR
. Це |–R, –|R, |–RI, –|RI, |–RU, –|RU, |–R1, –|R1, |–R2, –|R2,
|–RR, –|RR, |–R, –|R, |–R,–|R, |–RE, –|RE, |–REv, –|REv, |, |, |, |–R, |v, –|Rv, Ed, Ev. До них додаємо
|
|
|
,
,
; |
|
|
,
,
.
Базові секвенційні форми числень С
QCT
та С
QCTR
. Ці числення мають однакові базові секвенційні
форми, вони відрізняються різними умовами замкненості секвенції. Базові секвенційні форми складаються з
наведених вище секвенційних форм, до яких додаємо форми типу R і форми декомпозиції | T, та | T :
|–R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
; –|R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
; |–R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
; –|R
,
| ,
,
| ,
( ),
( ),
v u
x
v u
x
R
R
;
| T
||
|
, ,
,
; | T
| |
|
, ,
,
.
Базові секвенційні форми числень С
QCF
та С
QCFR
. Ці числення мають однакові базові секвенційні
форми, проте відрізняються різними умовами замкненості секвенції. Базові секвенційні форми складаються з
секвенційних форм числень С
QCT
та С
QCTR
, проте замість форм | T та | T беремо форми | F та | F :
| F
| |
|
, ,
,
; | F
||
|
, ,
,
.
Форми типів R, RІ, RU, R допоміжні, вони виконуються кожен раз при появі відповідної ситуації.
Маємо також спеціальні форми Ed та Ev; всі інші базові секвенційні форми – основнi.
Основна властивість секвенційних форм. Властивості відношень логічного наслідку для множин
формул індукують основну властивість базових секвенційних форм (|= – одне з розглянутих відношень):
Теорема 9. 1. Нехай
| |
| |
– базова форма. Тоді: a) |= |= ; b) | | .
2. Нехай
| | | |
| |
– базова форма. Тоді: a) |= та |= |= ; b) | або | | .
Побудова виведення. При побудові виведення (секвенційного дерева) ми спрощуємо виділену формулу чи
розкладаємо її на компоненти. Секвенції трактуємо як множини специфікованих формул, тому якщо в результаті
виконання форми отримуємо формулу, яка вже є в секвенції, цю формулу-копію до секвенції не заносимо.
Опишемо поетапну побудову секвенційного дерева для заданої скінченної секвенції .
Побудова секвенційного дерева починається з кореня. На початку виведення виконуємо первісний
розподіл імен ud(): використовуючи Ed-форму, робимо всеможливі розподіли всіх імен із ud() на означені та
не-означені. Це веде до побудови дерева висоти h = |ud()| з коренем , що дає m = 2
h
наступників . Якщо
val() = , то для тієї секвенції-наступника 0, для якої val(0) = , за допомогою форми Ev виконуємо первісне
означення: збагачуємо секвенцію 0 формулою |–Ez такою, що zfu(), що дає секвенцію 0, |–Ez. Це дає
непорожність множини означених імен для кожної секвенції-наступника , що надалі гарантує застосовність
F-форм.
Опишемо етап виведення для певної незамкненої листа-секвенції . Це означає добудову скінченного
піддерева з вершиною . Активізуємо (окрім примітивних) формули секвенції . До кожної активної формули
далі застосовується відповідна форма. В процесі застосування основних форм кожен раз при появі відповідної
ситуації виконуємо спрощення, застосовуючи належні допоміжні форми типів R, RI, RU, R.
Форми типу R застосовуються до примітивних формул та їх заперечень. Після їх застосування усі
примітивні формули секвенції та їх заперечення стають Un-формулами, де Un – множина всіх unv-змінних
формул секвенцій на шляху від кореня до даної секвенції.
Після застосування основної форми та виконання спрощень утворені нею формули на даному етапі
пасивні, до таких формул на цьому етапі основні секвенційні форми не застосовуються.
Застосування на етапі основних секвенційних форм проводимо так.
191
Теоретичні і методологічні основи програмування
Спочатку виконуємо усі форми, окрім F-форм. При кожному застосуванні T беремо нове zVT, яке
відсутнє на шляху від кореня до секвенції, в якій виконуємо цю T-форму. F-форми виконуємо після
T-форм. Кожна F-форма виконується багатократно для кожного означеного у із формул на шляху від
до даної секвенції.
Після виконання усіх форм на етапі перевіряємо кожну секвенцію-лист на замкненість. Якщо всі листи
будованого дерева замкнені, то ми отримали замкнене секвенційне дерево, побудова завершена позитивно.
Якщо секвенція-лист незамкнена, то перевіряємо, чи буде фінальною секвенцією.
Незамкнена вершина-секвенція виведення секвенції – фінальна, якщо до неї незастосовна жодна
форма, або якщо кожне застосування секвенційної форми до не вводить нових формул, відмінних від формул
секвенцій на шляху від до . Поява фінальної секвенції означає ситуацію повторення незамкненої секвенції на
даному шляху. Це сигналізує про наявність в дереві шляху (від кореня до даної фінальної секвенції), всі
вершини якого незамкнені – незамкненого шляху. Його поява засвідчує: побудова виведення завершена
негативно.
Таким чином, при побудові секвенційного дерева можливі такі випадки:
1) Побудову завершено позитивно, маємо скінченне замкнене дерево.
2) Побудову завершено негативно, маємо скінченне незамкнене дерево. В такому дереві існує шлях, усі
вершини якого – незамкнені секвенції; такий шлях називають незамкненим.
3) Побудова не завершується, тоді маємо нескінченне дерево. За лемою Кеніга [2] таке дерево має хоча б
один нескінченний шлях. Усі вершини цього шляху – незамкнені секвенції, адже при появі замкненої секвенції
побудова дерева на цьому шляху обривається. Отже, в дереві маємо нескінченний незамкнений шлях.
Побудова секвенційного дерева для заданої зліченної секвенції має особливості. Побудова такого
дерева теж розбита на етапи та починається з його кореня . Кожне застосування секвенційної форми на етапі
проводимо до скінченної множини доступних на даний момент формул. На відміну від описаної вище
побудови, кожне застосування секвенційної форми проводимо до скінченної множини доступних на даний
момент формул (див., напр., [4, 6]). На початку побудови доступна лише пара перших формул списків T-формул
та F-формул секвенції (єдина T-формула чи F-формула, якщо один зі списків порожній).
На початку кожного етапу в усіх незамкнених секвенціях виконується крок доступу: до списку доступних
формул секвенції додаємо по одній формулі з її списків T-формул та F-формул. Нехай на початку етапу після
додавання до неї пари доступних формул отримана секвенція . Далі виконуємо етапний розподіл імен ud():
використовуючи Ed-форму, робимо всеможливі розподіли всіх імен із ud() на означені та неозначені. Це веде
до побудови дерева висоти |ud()| з коренем , що дає k = 2
|ud()|
наступників . Якщо val() = , то для тієї
секвенції-наступника 0, для якої val(0) = , виконуємо первісне означення, що дає секвенцію 0, |–Ez.
Порядок та особливості застосування на етапі секвенційних форм такі ж, як при виведенні скінченних
секвенцій. Кожна F-форма виконується багатократно для кожного означеного у із доступних формул на шляху
від до даної секвенції. Форми типу R застосовуються до примітивних формул та їх заперечень, при їх
застосуванні Un – множина всіх unv-змінних доступних формул на шляху від кореня до даної секвенції.
Після виконання усіх форм на етапі перевіряємо кожну секвенцію-лист на замкненість. Якщо всі листи
будованого дерева замкнені, то маємо замкнене секвенційне дерево, побудова завершена позитивно. Якщо ні,
то для кожного незамкненого листа робимо наступний крок доступу і продовжуємо виведення так, як описано.
При побудові дерева для зліченної секвенції втрачає сенс поняття фінальної секвенції, тому можливі 2 випадки:
1) побудова завершена позитивно із отриманням скінченного замкненого дерева;
2) побудова не завершується, тоді маємо нескінченне незамкнене дерево. В такому дереві існує нескін-
ченний незамкнений шлях. Кожна з формул секвенції зустрінеться на цьому шляху і стане доступною.
Теорема коректності. Теорема коректності формулюється однотипно для кожного з описаних числень.
В цьому формулюванні відношенням логічного наслідку
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF,
Pс
|=T,
Pс
|=F,
Rс
|=T,
Rс
|=F
відповідають числення С
QIR
, С
QT
, С
QF
, С
QTF
, С
QTFR
, С
QСT
, С
QСF
, С
QCTR
, С
QСFR
.
Теорема 10 (коректності). Нехай секвенція |––| вивідна в численні C
Q#
, тоді |= .
Якщо |––| вивідна у певному численні C
Q#
, то для неї побудоване замкнене секвенційне дерево. Для
кожної його вершини |––| маємо |= . Для листів дерева це випливає з визначення замкненої секвенції.
Збереження секвенційними формами відношення логічного наслідку (від засновків до висновку) випливає з
теореми 9. Тому для кореня дерева – секвенції |––| – теж маємо |= .
192
Теоретичні і методологічні основи програмування
4. Теореми про контрмоделі. Теорема повноти
Теореми повноти секвенційних числень традиційно доводяться на основі теорем про існування контр-
моделі для множини формул незамкненого шляху. Доведення теорем про контрмоделі використовує (див. [4])
метод модельних множин. Детально розглянемо теореми про контрмоделі для числень C
QCTR
та C
QCFR
.
Теорема 11. Нехай – незамкнений шлях у секвенційному дереві, збудованому в C
QCTR
для |––|, нехай
Н – множина всіх специфікованих формул секвенцій цього шляху. Тоді існують інтерпретація A = (S, I) та
V
S :
НT) |–Н T(A) та –|Н T(A).
Теорема 12. Нехай – незамкнений шлях у секвенційному дереві, збудованому в C
QCFR
для |––|, нехай
Н – множина всіх специфікованих формул секвенцій цього шляху. Тоді існують інтерпретація B = (S, I) та
V
A:
НF) |–Н F(B) та –|Н F(B).
Пари (A, ) та (B, ) назвемо T-контрмоделлю i F-контрмоделлю для секвенції |––|.
Множину Un = {ynm(Н) | –|EyН} та назвемо множиною неозначених імен множини Н. Задамо
W = nm(Н) \ Un. Наявність первісного означення (поетапних означень) дає умову W = {ynm(Н) | |–EyН}.
Доведення теорем 11 та 12 однотипне. Застосування форм до секвенцій шляху робимо до тих пір, поки
це можливо, тому кожна непримітивна формула чи її заперечення, що зустрічається на шляху , рано чи пізно
буде розкладена чи спрощена. Усі секвенції шляху незамкнені, тому не виконується умова замкненості:
C CF C для С
QCTR
та C CF C для С
QCFR
. Отже, для множини Н виконуються умови коректності:
НС) не існує формули такої, що |–Н та –|Н;
НCF) не існує формули вигляду
, ,
, , ( )v u z
xR Ez такої, що
, ,
| , , ( )v u z
xR Ez H ;
HC ) не існує формули такої, що | H – для множини Н теореми 2.3;
HC ) не існує формули такої, що | H – для множини Н теореми 2.4.
Переходи від нижчої вершини шляху до вищої відбуваються згідно з певною секвенційною формою,
тому для Н виконуються відповідні умови переходу. Наведемо для прикладу наступні умови переходу:
НR1) –|EzН та
, , , ,
| |, , , ,( ) ( )
v u y v u y
x z xR p H R p H ; –|EzН та
, , , ,
| |, , , ,( ) ( )
v u y v u y
x z xR p H R p H ;
НR1) –|EzН та
, , , ,
| |, , , ,( ) ( )
v u y v u y
x z xR p H R p H ; –|EzН та
, , , ,
| , , | , ,( ) ( )v u y v u y
x z xR p H R p H ;
НR2) –|EzН та
, , ,
| |, , ,( ) ( )v u z v u
x xR p H R p H ; –|EzН та
, , ,
| |, , ,( ) ( )v u z v u
x xR p H R p H ;
НR2) –|EzН та
, , ,
| |, , ,( ) ( )v u z v u
x xR p H R p H ; –|EzН та
, , ,
| |, , ,( ) ( )v u z v u
x xR p H R p H ;
НE ) |–EzН –|EzН; –|EzН |–EzН;
НRE )
, ,
| |, ,( ) ( ) ;v u v u
x xR Ez H R Ez H
, ,
| |, ,( ) ( ) ;v u v u
x xR Ez H R Ez H
НRE ) за умови { , }z v u маємо:
,
| |, ( ) ;v u
xR Ez H Ez H
,
| |, ( ) ;v u
xR Ez H Ez H
НREv )
, ,
| |, , ( ) ;v u z
x yR Ez H Ey H , ,
| |, , ( ) ;v u z
x yR Ez H Ey H
Mножинy специфікованих формул Н, для якої виконуються умови коректності НС, НCF, HC , вищена-
звані умови переходу та умова переходу Н T, назвемо RTС-модельною.
Mножинy специфікованих формул Н, для якої виконуються умови коректності НС, НCF, HC , вищена-
звані умови переходу та умова переходу Н F, назвемо RFС-модельною.
Умови Н T та Н F формулюються так:
193
Теоретичні і методологічні основи програмування
Н T) | H –|Н та –|Н; | H |–Н або |–Н;
Н F) | H –|Н або –|Н; | H |–Н та |–Н.
Побудуємо контрмодель за RTС-модельною множиною Н. Нехай S – множина, яка дублює множину W,
тобто |S| = |W|. Визначимо ін’єктивну
V
S з областю визначення W. Така є сбієкцією W S.
|–Ex Н дає xW, тому ExА () = T, звідки T(ExА); –|Ex Н дає xW, тому (x), звідки T(ExА).
Наведемо базові визначення значень предикатів. Для цього задамо на в інтерпретації A значення атомарних
формул і примітивних Un-формул та їх заперечень:
– |– рН T(рA); –| рН T(рA); |–рН T(pA); –|pН T(pA);
– , ,
| , ,( ) ( ( ) );v u v u
Ax xR p H T R p , ,
| , ,( ) ( ( ) );v u v u
Ax xR p H T R p
–
, ,
| , ,( ) ( ( ) );v u v u
Ax xR p H T R p
, ,
| , ,( ) ( ( ) ).v u v u
Ax xR p H T R p
Подібним чином будуємо контрмодель за RFС-модельною множиною Н, аналогічно задаючи S та .
|–Ex Н дає xW, тому ExА () = T, звідки F(Ex B); –|Ex Н дає xW, тому (x), звідки F(Ex B).
Задаємо на в B значення атомарних формул і примітивних Un-формул та їх заперечень:
– |– рН F(рB); –| рН F(рB); |–рН F(pB); –|pН F(pB);
–
, ,
| , ,( ) ( ( ) );v u v u
Bx xR p H F R p
, ,
| , ,( ) ( ( ) );v u v u
Bx xR p H F R p
–
, ,
| , ,( ) ( ( ) );v u v u
Bx xR p H F R p
, ,
| , ,( ) ( ( ) ).v u v u
Bx xR p H F R p
Для атомарних формул, примітивних Un-формул та їх заперечень твердження теореми 11 та теореми 12
випливає з наведеного вище задання значень відповідних предикатів.
Наведемо доведення для пункту НR1 паралельно для інтерпретацій A та B.
Нехай –|EzН та
, ,
| , , ( ) .
v u y
x zR p H Умова –|EzН дає zW, тому (z), звідки
, , , ,
, , , ,r ( ) r ( ).
v u y v u y
x x z Згідно
НR1 маємо
, ,
| , , ( ) .
v u y
xR p H Тоді
, ,
, ,( ( ) )
v u y
AxT R p ,
, ,
, ,( ( ) )
v u y
Ax zT R p та
, ,
, ,( ( ) ),
v u y
BxF R p
, ,
, ,( ( ) )
v u y
Bx zF R p .
Нехай –|EzН та
, ,
| , , ( ) .
v u y
x zR p H Умова –|EzН дає zW, тому (z), звідки
, , , ,
, , , ,r ( ) r ( ).
v u y v u y
x x z Згідно
НR маємо1
, ,
| , , ( ) .
v u y
xR p H Тоді
, ,
, ,( ( ) )
v u y
AxT R p ,
, ,
, ,( ( ) )
v u y
Ax zT R p та
, ,
, ,( ( ) ),
v u y
BxF R p
, ,
, ,( ( ) )
v u y
Bx zF R p .
Подібним чином доводимо для пунктів НR1, НR2, НR2 та для пунктів НE, НRE .
Для решти пунктів доводимо традиційно – індукцією за складністю формули згідно з визначенням Н.
Наведемо для прикладу доведення для пункту Н T (теорема 11) та пункту Н F (теорема 12).
Нехай | H . Згідно Н T маємо –|Н та –|Н. За припущенням індукції маємо T(A) та
T(A) = F(A), звідки (A). Проте (A) = ( )AT , звідки ( )AT .
Нехай | H . Згідно Н T маємо |–Н або |–Н. За припущенням індукції маємо T(A) або
T(A) = F(A), звідки (A). Проте (A) = ( )AT , звідки ( )AT .
Нехай | H . Згідно Н F маємо –|Н або –|Н. За припущенням індукції маємо F(B) або
F(B) = T(B), звідки (B). Проте (B) = ( ) ( ), B BT F звідки ( ) BF .
Нехай | H . Згідно Н F маємо |–Н та |–Н. За припущенням індукції маємо F(B) та
F(B) = T(B), звідки (B). Проте (B) = ( ) ( ) B BT F , звідки ( ) BF .
Теореми про контрмоделі для числень C
QСT
та C
QСF
формулюються і доводяться аналогічно. Числення
C
QСT
та C
QСF
формалізують відношення
Pс
|=T та
Pс
|=F, тому всі предикати A та B мають бути однозначними.
Для множини Н при цьому мають виконуватися додаткові умови коректності:
194
Теоретичні і методологічні основи програмування
НСL) не існують формули такі, що |–, |–Н (якщо Н отримана при виведенні в C
QСT
);
НСR) не існують формули такі, що –|, –|Н (якщо Н отримана при виведенні в C
QСF
).
Теореми про контрмоделі для C
QT
та C
QF
формулюються і доводяться аналогічно теоремам 11 та 12, але
опускаємо пункти HR , H R , Н T, Н F та умови HC , HC , додаємо умови НСL та НСR.
Наведемо теореми про контрмоделі для C
QTF R
, C
QTF
та C
QIR
.
Теорема 13. Нехай – незамкнений шлях у секвенційному дереві, збудованому в C
QTFR
для секвенції
|––|, нехай Н – множина всіх специфікованих формул секвенцій цього шляху. Тоді існують інтерпретації
A = (S, IA), B = (S, IB) та
V
S такі, що виконуються умови НT та НF .
Такі пари (A, ) та (B, ) назвемо T-контрмоделлю i F-контрмоделлю для |––|.
Теорема 14. Нехай – незамкнений шлях у секвенційному дереві, збудованому в C
QTF
для секвенції
|––|, нехай Н – множина всіх специфікованих формул секвенцій цього шляху. Тоді існують інтерпретації
A = (S, IA), B = (S, IB) та
V
S такі, що виконуються умови НT та НF .
Такі пари (A, ) та (B, ) назвемо T
P
-контрмоделлю i F
P
-контрмоделлю для |––|.
При доведенні теореми 13 та14 опускаємо пункти HR , H R , Н T, Н F і умови коректності
HC , HC , при цьому при доведенні теореми 14 додаємо умову коректності НСLR:
НСLR) не існують формули та такі, що |–, |–Н та –|, –|Н.
Зрозуміло, що НСLR НСL НСR. Зробимо зауваження щодо вибору контрмоделі. Для T
P
-
контрмоделі невиконання умови НСL, тобто наявність формули такої, що |–Н та |–Н, дає A() = T
та A() = T, звідки A() = F, що дає неоднозначність A . Для F
P
-контрмоделі невиконання умови НСR,
тобто наявність формули такої, що –|Н та –|Н, дає B() = F та B() = F, звідки B() T, що дає
неоднозначність B .
Отже, за умови НСLR при невиконанні НСL беремо F
P
-контрмодель, а при невиконанні умови НСR
беремо T
P
-контрмодель; при виконанні НСL та НСR можна брати як F
P
-контрмодель, так і T
P
-контрмодель.
Теорема 15. Нехай – незамкнений шлях у секвенційному дереві, збудованому в C
QIR
для |––|, нехай
Н – множина всіх специфікованих формул секвенцій цього шляху. Тоді існують інтерпретація A = (S, I) та
V
S:
НС) |–Н A() = T та –|Н A() = F.
Таку пару (A, ) назвемо IR-контрмоделлю для секвенції |––|.
На основі теорем про контрмоделі для кожного з описаних секвенційних числень, що формалізує
відповідне відношення логічного наслідку, отримуємо теорему повноти. Вона формулюється однотипно для
всіх цих числень. Як і в формулюванні теореми коректності, відношенням логічного наслідку
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF,
Pс
|=T,
Pс
|=F,
Rс
|=T,
Rс
|=F відповідають числення С
QIR
, С
QT
, С
QF
, С
QTF
, С
QTFR
, С
QСT
, С
QСF
, С
QCTR
,
С
QСFR
.
Теореми повноти формулюються однотипно для всіх цих числень:
Теорема 16 (повноти): Нехай секвенція |––| вивідна в численні C
Q#
, тоді |= .
Доведемо для прикладу для
Rc
|=T і числення C
QCTR
. Подібні доведення теорем повноти див. [4, 11].
Нехай маємо супротивне:
Rс
|=T та секвенція |––| невивідна, тоді секвенційне дерево для |––| не-
замкнене. Отже, в цьому дереві існує незамкнений шлях. Нехай Н – множина всіх специфікованих формул
секвенцій цього шляху. За теоремою 11 існує T-контрмодель (A, ): |–Н T(A) та –|Н T(A).
Згідно з |––| Н для всіх маємо T(A), для всіх Ψ маємо T(ΨA). Звідси T(A) та T(A),
тому невірно T(A) T(A). Це заперечує A|=T , тому й заперечує
Rс
|=T .
Висновки
Досліджено нові програмно-орієнтовані логічні формалізми – чисті першопорядкові логіки часткових
квазіарних предикатів з розширеними реномінаціями та спеціальною композицією предикатного доповнення.
Операції, подібні до предикатного доповнення, використовуються в різних варіантах програмних логік
Флойда-Хоара з частковими перед- та після-умовами. Розглянуто композиційні системи та мови таких логік, для
них описано низку відношень логічного наслідку, наведено властивості декомпозиції формул і елімінації
кванторів.
195
Теоретичні і методологічні основи програмування
Властивості відношень логічного наслідку є семантичною основою побудови відповідних числень
секвенційного типу. Наведено базові секвенційні форми цих числень та умови замкненості секвенцій. Описано
побудову виведення – секвенційного дерева. Для пропонованих секвенційних числень доведено теореми
коректності та повноти. Доведення теореми повноти опирається на теореми про побудову контрмоделей.
Література
1. Handbook of Logic in Computer Science / Edited by S. Abramsky, Dov M. Gabbay and T. S. E. Maibaum. Oxford University Press, Vol. 1–5,
1993–2000.
2. Kleene S.C. Mathematical Logic. New York, 1967.
3. Нікітченко М.С., Шкільняк С.С. Прикладна логіка. Київ: ВПЦ Київський університет, 2013. 278 с.
4. Шкільняк С.С. Спектр секвенційних числень першопорядкових композиційно-номінативних логік. Проблеми програмування. 2013.
№ 3. C. 22–37.
5. Нікітченко М.С., Шкільняк O.С., Шкільняк С.С. Першопорядкові композиційно-номінативні логіки із узагальненими реномінаціями.
Проблеми програмування. 2014. № 2–3. C. 17–28.
6. Нікітченко М.С., Шкільняк O.С., Шкільняк С.С. Чисті першопорядкові логіки квазіарних предикатів. Проблеми програмування. 2016.
№ 2–3. C. 73–86
7. Hoare C. An axiomatic basis for computer programming, Comm. ACM. 1969. 12(10). P. 576–580.
8. Apt K. Ten years of Hoare’s logic: a survey – part I. ACM Trans. Program. Lang. Syst., 1981. 3(4), 431–483.
9. Нікітченко М.С., Шкільняк O.С., Шкільняк С.С., Мамедов Т.А. Пропозиційні логіки часткових предикатів з композицією предикат-
ного доповнення. Проблеми програмування. 2019. № 1. C. 3–13.
10. Nikitchenko M., O. Shkilniak O., Shkilniak S. Program Logics of Renominative Level with the Composition of Predicate Complement.
Proceedings of the 15th International Conference on ICT. CEUR Workshop, Kherson, Ukraine. 2019. Vol. 2393. P. 603–616.
11. Nikitchenko M., O. Shkilniak O., Shkilniak S., Mamedov T. Completeness of the First-Order Logic of Partial Quasiary Predicates with the
Complement Composition. Computer Science Journal of Moldova. 2019. Vol. 27. N 2 (80). P. 162–187.
12. Шкільняк О.С. Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення. Проблеми
програмування. 2019. № 3. C. 11–27.
References
1. Abramsky S., Gabbay D. and MAIBAUM, T. (editors). (1993–2000). Handbook of Logic in Computer Science Oxford
University Press.
2. Kleene S. (1967) Mathematical Logic. New York.
3. Nikitchenko M. and Shkilniak S. (2013). Applied logic. Кyiv: VPC Кyivskyi Universytet (in ukr).
4. Shkilniak S. (2013). Spectrum of sequent calculi of first-order composition-nominative logics. Problems in Progamming. N 3.
P. 22–37 (in ukr).
5. Nikitchenko M., Shkilniak O. and Shkilniak S. (2014). First-order composition-nominative logics with generalized renominations.
Problems in Progamming. N 2–3. P. 17–28 (in ukr).
6. Nikitchenko M., Shkilniak O. and Shkilniak S. (2016). Pure first-order logics of quasiary predicates. Problems in Progamming. N 2–3.
P. 73–86 (in ukr).
7. Hoare C. (1969). An axiomatic basis for computer programming, Comm. ACM 12(10). P. 576–580.
8. Apt K. (1981). Ten years of Hoare’s logic: a survey – part I, ACM Trans. Program. Lang. Syst. 3(4). P. 431–483
9. Nikitchenko M., Shkilniak O., Shkilniak S. and Mamedov T. (2019). Propositional logics of partial predicates with composition of predicate
complement. Problems in Progamming. N 1. P. 3–13 (in ukr).
10. Nikitchenko M., Shkilniak O. and Shkilniak S. (2019). Program Logics of Renominative Level with the Composition of Predicate Complement.
Proceedings of the 15th International Conference on ICT. CEUR Workshop, Kherson, Ukraine. Vol. 2393. P. 603–616.
11. Nikitchenko M., Shkilniak O., Shkilniak S. and Mamedov T. (2019). Completeness of the First-Order Logic of Partial Quasiary Predicates with
the Complement Composition. Computer Science Journal of Moldova, Vol. 27, N 2 (80). P.162–187.
12. Shkilniak O. (2019). Relations of logical consequence of logics of partial predicates with composition of predicate complement. Problems in
Progamming. N 3. P. 11–27 (in ukr).
Одержано 02.03.2020
Про авторів:
Нікітченко Микола Степанович,
доктор фізико-математичних наук, професор,
завідувач кафедри теорії та технології програмування.
Кількість наукових публікацій в українських виданнях – понад 220, в т.ч.
кількість наукових публікацій у фахових виданнях – понад 120.
Кількість наукових публікацій в зарубіжних виданнях – понад 50.
196
Теоретичні і методологічні основи програмування
Scopus Author ID: 6602842336;
h-індекс (Google Scholar): 15 (13 з 2015).
http://orcid.org/0000-0002-4078-1062,
Шкільняк Оксана Степанівна,
кандидат фізико-математичних наук, доцент,
доцент кафедри інтелектуальних програмних систем.
Кількість наукових публікацій в українських виданнях – понад 80, в т.ч.
кількість наукових публікацій у фахових виданнях – понад 40.
Кількість наукових публікацій в зарубіжних виданнях – 17.
Scopus Author ID: 57190873266;
h-індекс (Google Scholar): 5 (3 з 2015).
http://orcid.org/0000-0003-4139-2525,
Шкільняк Степан Степанович,
доктор фізико-математичних наук, професор,
професор кафедри теорії та технології програмування.
Кількість наукових публікацій в українських виданнях – понад 200, в т.ч.
кількість наукових публікацій у фахових виданнях –понад 110.
Кількість наукових публікацій в зарубіжних виданнях – 35.
Scopus Author ID: 36646762300;
h-індекс (Google Scholar): 8 (6 з 2015).
http://orcid.org/0000-0001-8624-5778.
Місце роботи авторів:
Київський національний університет імені Тараса Шевченка ,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 5213345.
E-mail: me.oksana@gmail.com,
nikitchenko@unicyb.kiev.ua,
sssh@unicyb.kiev.ua.
197
|