Logics of general non-deterministic predicates: semantic aspects
Semantic aspects of a new class of program-oriented logical formalisms – logics of general non-deterministic quasiary predicates (GND-predicates) – are considered. Сlasses of GND-predicates are singled out, their compositions and algebras are investigated. The language of pure first-order logics of...
Збережено в:
| Дата: | 2018 |
|---|---|
| Автори: | , , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2018
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/263 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-263 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/49/cf3d8a675fa8a5df8dfea0e4f124ac49.pdf |
| spelling |
pp_isofts_kiev_ua-article-2632024-04-28T11:37:22Z Logics of general non-deterministic predicates: semantic aspects Логики общих недетерминированных предикатов: cемантични аспекты Логіки загальних недетермінованих предикатів: cемантичні аспекти Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. logic; algebra; composition; non-deterministic predicate; logical consequence UDC 004.42:510.69 логика; алгебра; композиция; недетерминированный предикат; логическое следствие УДК 004.42:510.69 логіка; алгебра;композиція; недетермінований предикат; логічний наслідок УДК 004.42:510.69 Semantic aspects of a new class of program-oriented logical formalisms – logics of general non-deterministic quasiary predicates (GND-predicates) – are considered. Сlasses of GND-predicates are singled out, their compositions and algebras are investigated. The language of pure first-order logics of GND-predicates is described. The relation of the logical consequence for the sets of formulas is proposed and investigated. The properties of the decomposition of formulas and of quantifier elimination are described.Problems in programming 2018; 2-3: 031-045 Исследованы семантические аспекты нового класса программно-ориентированных логических формализмов – логик общих недетерминированных квазиарных предикатов, или GND-предикатов. Выделены разновидности таких предикатов, исследованы свойства их композиций, рассмотрены композиционные алгебры GND-предикатов. Описаны языки чистых первопорядковых логик GND-предикатов. Предложены и исследованы отношения логического следствия для множеств формул. Описаны свойства декомпозиции формул и элиминации кванторов.Problems in programming 2018; 2-3: 031-045 Досліджено семантичні аспекти нового класу програмно-орієнтованих логічних формалізмів – логік загальних недетермінованих квазіарних предикатів, або GND-предикатів. Виділено різновиди таких предикатів, досліджено властивості їх композицій, розглянуто композиційні алгебри GND-предикатів. Описано мови чистих першопорядкових логік GND-предикатів. Запропоновано та досліджено відношення логічного наслідку для множин формул. Описано властивості декомпозиції формул та елімінації кванторів. Problems in programming 2018; 2-3: 031-045 Інститут програмних систем НАН України 2018-11-05 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/263 10.15407/pp2018.02.031 PROBLEMS IN PROGRAMMING; No 2-3 (2018); 31-45 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2018); 31-45 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2018); 31-45 1727-4907 10.15407/pp2018.02 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/263/257 Copyright (c) 2018 PROBLEMS OF PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2024-04-28T11:37:22Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
logic algebra composition non-deterministic predicate logical consequence UDC 004.42:510.69 |
| spellingShingle |
logic algebra composition non-deterministic predicate logical consequence UDC 004.42:510.69 Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. Logics of general non-deterministic predicates: semantic aspects |
| topic_facet |
logic algebra composition non-deterministic predicate logical consequence 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 |
Logics of general non-deterministic predicates: semantic aspects |
| title_short |
Logics of general non-deterministic predicates: semantic aspects |
| title_full |
Logics of general non-deterministic predicates: semantic aspects |
| title_fullStr |
Logics of general non-deterministic predicates: semantic aspects |
| title_full_unstemmed |
Logics of general non-deterministic predicates: semantic aspects |
| title_sort |
logics of general non-deterministic predicates: semantic aspects |
| title_alt |
Логики общих недетерминированных предикатов: cемантични аспекты Логіки загальних недетермінованих предикатів: cемантичні аспекти |
| description |
Semantic aspects of a new class of program-oriented logical formalisms – logics of general non-deterministic quasiary predicates (GND-predicates) – are considered. Сlasses of GND-predicates are singled out, their compositions and algebras are investigated. The language of pure first-order logics of GND-predicates is described. The relation of the logical consequence for the sets of formulas is proposed and investigated. The properties of the decomposition of formulas and of quantifier elimination are described.Problems in programming 2018; 2-3: 031-045 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2018 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/263 |
| work_keys_str_mv |
AT nikitchenkoms logicsofgeneralnondeterministicpredicatessemanticaspects AT shkilniakos logicsofgeneralnondeterministicpredicatessemanticaspects AT shkilniakss logicsofgeneralnondeterministicpredicatessemanticaspects AT nikitchenkoms logikiobŝihnedeterminirovannyhpredikatovcemantičniaspekty AT shkilniakos logikiobŝihnedeterminirovannyhpredikatovcemantičniaspekty AT shkilniakss logikiobŝihnedeterminirovannyhpredikatovcemantičniaspekty AT nikitchenkoms logíkizagalʹnihnedetermínovanihpredikatívcemantičníaspekti AT shkilniakos logíkizagalʹnihnedetermínovanihpredikatívcemantičníaspekti AT shkilniakss logíkizagalʹnihnedetermínovanihpredikatívcemantičníaspekti |
| first_indexed |
2024-09-16T04:08:23Z |
| last_indexed |
2024-09-16T04:08:23Z |
| _version_ |
1818528069892177920 |
| fulltext |
Теоретичні та методологічні основи програмування
© М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк, 2018
ISSN 1727-4907. Проблеми програмування. 2018. № 2–3. Спеціальний випуск 31
УДК 004.42:510.69
ЛОГІКИ ЗАГАЛЬНИХ НЕДЕТЕРМІНОВАНИХ ПРЕДИКАТІВ:
CЕМАНТИЧНІ АСПЕКТИ
М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк
Досліджено семантичні аспекти нового класу програмно-орієнтованих логічних формалізмів – логік загальних
недетермінованих квазіарних предикатів, або GND-предикатів. Виділено різновиди таких предикатів, досліджено властивості їх
композицій, розглянуто композиційні алгебри GND-предикатів. Описано мови чистих першопорядкових логік GND-предикатів.
Запропоновано та досліджено відношення логічного наслідку для множин формул. Описано властивості декомпозиції формул
та елімінації кванторів.
Ключові слова: логіка, алгебра, композиція, недетермінований предикат, логічний наслідок.
Исследованы семантические аспекты нового класса программно-ориентированных логических формализмов – логик общих
недетерминированных квазиарных предикатов, или GND-предикатов. Выделены разновидности таких предикатов, исследованы
свойства их композиций, рассмотрены композиционные алгебры GND-предикатов. Описаны языки чистых первопорядковых
логик GND-предикатов. Предложены и исследованы отношения логического следствия для множеств формул. Описаны
свойства декомпозиции формул и элиминации кванторов.
Ключевые слова: логика, алгебра, композиция, недетерминированный предикат, логическое следствие.
Semantic aspects of a new class of program-oriented logical formalisms – logics of general non-deterministic quasiary predicates (GND-
predicates) – are considered. Сlasses of GND-predicates are singled out, their compositions and algebras are investigated. The language
of pure first-order logics of GND-predicates is described. The relation of the logical consequence for the sets of formulas is proposed and
investigated. The properties of the decomposition of formulas and of quantifier elimination are described.
Key words: logic, algebra, composition, non-deterministic predicate, logical consequence.
Вступ
Розвиток інформаційних технологій та їх проникнення в усі сфери діяльності людини роблять
першорядною задачу створення ефективних і надійних програмних систем. Основою, ядром таких систем є
апарат математичної логіки. Водночас поява все нових задач і проблем, які виникають в процесі розвитку
інформатики й програмування, індукує їх зворотний вплив на логіку, вимагає зробити її ближчою й
адекватнішою до потреб програмування. На даний час розроблено (див., напр., [1]) низку різноманітних
логічних систем, які успішно застосовуються в інформатиці й програмуванні. В їх основі зазвичай лежить
класична логіка предикатів та базовані на ній спеціальні логіки (модальні, темпоральні, епістемічні, програмні
тощо). Проте класична логіка має принципові обмеження, які істотно ускладнюють її використання.
Характерним для програмування є широке використання часткових неоднозначних відображень над неповними
даними, а класична логіка предикатів базується на традиційних математичних структурах однозначних
тотальних скінченно-арних відображень.
Обмеження класичної логіки предикатів виводять на перший план проблему побудови нових, програмно-
орієнтованих логічних формалізмів. Природною основою такої побудови є спільний для логіки й
програмування композиційно-номінативний підхід. Логіки, збудовані на його основі, названо композиційно-
номінативними (КНЛ). Передумовою їх виникнення стала необхідність посилення можливостей класичної
логіки для розв’язання нових задач інформатики й програмування. КНЛ базуються на загальних класах
часткових відображень, заданих на довільних наборах іменованих значень. Такі набори названо номінативними
даними. Однорівневі однозначні номінативні дані названо іменними множинами (ІМ). Відображення, задані
на ІМ, названо квазіарними. Низку різноманітних класів КНЛ квазіарних предикатів описано та досліджено
в [2–7].
Метою даної роботи є дослідження нових класів програмно-орієнтованих логічних формалізмів – КНЛ
загальних недетермінованих квазіарних предикатів. Ці логіки відображають такі властивості програм, як
частковість, недетермінізм, нефіксовану арність. Огляд недетермінованих пропозиційних логік та логік
недетермінованих n-арних предикатів наведено в [8]. Загальні недетерміновані квазіарні предикати, названі
GND-предикатами, запропоновано в [9]. Вони є узагальненням часткових неоднозначних предикатів реляційного
типу [3]. Композиційні алгебри GND-предикатів досліджено в [10]. Показано зв'язок GND-предикатів із
7-значними тотальними детермінованими предикатами, описано мови чистих першопорядкових логік GND-
предикатів.
Вивчення семантичних аспектів GND-предикатів триває в даній роботи. Виділено різновиди
GND-предикатів, розглянуто властивості їх композицій, описано композиційні алгебри та мови логіки
GND-предикатів. Досліджено відношення логічного наслідку для множин формул. Визначено відношення
G-наслідку, логічного G-наслідку та логічного SG-наслідку, описано властивості цих відношень. Досліджено
властивості декомпозиції формул та елімінації кванторів. Ці властивості є семантичною основою подальшої
побудови числень секвенційного типу для логік GND-предикатів.
Теоретичні та методологічні основи програмування
32
Поняття, які тут не визначаються, тлумачимо в сенсі [2, 3, 6]. Нагадаємо лише базові визначення.
V-A-іменна множина (V-A-ІМ) – це часткова однозначна функція вигляду d : V A. Трактуємо V і A як
множину предметних імен (змінних) і множину предметних значень. Клас всіх V-A-ІМ позначаємо
V
A.
Під V-A-квазіарним предикатом розумітимемо часткову неоднозначну, взагалі кажучи, функцію вигляду
P :
V
A {T, F}. Тут {T, F} – множина істиннісних значень.
1. Загальні недетерміновані предикати та їх різновиди
Поняття недетермінованого (неоднозначного) предиката в загальному випадку описано в [10]. Такий
предикат на деяких даних через нечіткість та невизначеність інформації може функціонувати
недетермінованим чином: на одному і тому ж даному може приймати значення T, приймати значення F, а
може і не приймати жодного значення. Наприклад (див. [10]), це можуть бути різні екземпляри одного і того
ж предиката, що є компонентами складнішого: на одному і тому ж даному одні екземпляри прийняли
значення T, інші екземпляри – значення F, а деякі екземпляри зациклились і не приймають жодного
значення.
Таким чином, недетермінований предикат P :
V
A {T, F} при застосуванні до певного d
V
А може
приймати значення T, приймати значення F, а також може не приймати жодного значення, тобто може бути
невизначеним. Для кожного d
V
А має бути принаймні одна з цих ситуацій, що загалом дає 7 можливостей
для прийняття значення при застосуванні до певного даного. Так описані недетерміновані квазіарні
предикати загального вигляду названо GND-предикатами. Клaс V-А-квазіарних GND-предикатів позначимо
PrGV–A.
Нехай P[d] – множина значень, які недетермінований предикат P може прийняти на d
V
А, тоді P[d]
може бути однією з множин {}, {T}, {F}, {T, F}, {T, }, {F, }, {T, F, }. Скорочено позначимо їх , T, F,
TF, T, F, TF. Таким чином, GND-предикати можна моделювати як 7-значні тотальні детерміновані
предикати, які названо [10] TD7-предикатами. Множиною істиннісних значень цих предикатів є TV7 = {, T,
F, TF, T, F, TF}. Зв’язок GND-предикатів та TD7-предикатів досліджено в [10], основні результати
наведено нижче.
B роботах [3–7] часткові неоднозначні квазіарні предикати ми трактували дещо огрублено, як
відповідності (відношення) між множинами
V
A та {T, F}, їх було названо R-предикатами – предикатами
реляційного типу. Кожний R-предикат P :
V
A {T, F} при застосуванні до певного даного d
V
А може
приймати лише значення T, лише значення F, обидва значення T та F, а також може бути невизначеним –
всього маємо 4 можливості.
Таким чином, для R-предиката P множиною значень P[d], які P може прийняти на d
V
А, може бути одна
з множин {}, {T}, {F}, {T, F}. Клaс V-А-квазіарних R-предикатів тут будемо позначати PrRV–A.
Зауважимо, що для класичних предикатів є лише 2 можливості – T чи F – для прийняття значення при
застосуванні до певного даного, адже вони є тотальними однозначним відображеннями P : A
X
{T, F}, X V.
Кожний V-A-квазіарний GND-предикат P можна однозначно описати за допомогою 3-х множин: областi
істинності T(P), області хибності F(P) та областi невизначеності (P). Ці множини задаються так:
– T(P) = {d
V
A | P може приймати на d значення T} = {d
V
A | TP[d]},
– F(P) = {d
V
A | P може приймати на d значення F} = {d
V
A | FP[d]},
– (P) = {d
V
A | P може бути невизначеним на d} = {d
V
A | P[d]}.
Кожне d
V
А має належати принаймні одній з цих множин, тому їх пов’язує така загальна умова:
T(P) F(P) (P) =
V
A (G)
Області істинності, хибності, невизначеності будемо також називати T-областю, F-областю, -областю.
Множину T(P) F(P) назвемо областю амбівалентності GND-предиката P.
Для однозначного задання V-A-квазіарного R-предиката P достатньо 2-х множин: T(P) та F(P). При цьому
( ) ( ) ( )P T P F P (R)
Кожний R-предикат P можна трактувати як GND-предикат, для якого маємо умову (R).
Можна виділити низку різноманітних класів GND-предикатів. При цьому має виконуватись умова (G).
Теоретичні та методологічні основи програмування
33
V-A-квазіарний GND-предикат P:
– однозначний, або SG-предикат, якщо T(P)F(P) = ;
– тотальний, або TG-предикат, якщо T(P)F(P) =
V
A;
– виконуваний, якщо T(P) ;
– неспростовний, якщо F(P) = ;
– тотально істинний, якщо T(P) =
V
А;
– тотально хибний, якщо F(P) =
V
А;
– тотально невизначений, або TIG-предикат (with total class of indefinite values), якщо (P) =
V
А;
– тотально амбівалентний, або TAmG-предикат, якщо T(P) = F(P) =
V
А.
TIG-предикати (в [10] названі OIG) дуже подібні до R-предикатів: кожний TIG-предикат, як і кожний
R-предикат, цілком визначається тільки T-областю та F-областю. Для R-предиката P (P) детермінується T(P)
та F(P) умовою (R), а для TIG-предиката P маємо (P) =
V
А, тому для нього істотні теж лише T(P) та F(P).
Клас TAmG-предикатів вироджений, такі предикати відрізняються лише -областями.
Зрозуміло, що існують SG-предикати, які не є R-предикатами, та навпаки. Те ж саме для TG-предикатів.
Поєднуючи (де це можливо) наведені вище умови з умовою (R), отримуємо низку класів R-предикатів.
V-A-квазіарний GND-предикат P:
– однозначний R-предикат, або P-предикат, якщо T(P)F(P) = та ( ) ( ) ( ) P T P F P ;
– тотальний R-предикат, або T-предикат, якщо (P) = (умова (G) тоді дає T(P)F(P) =
V
A);
– неспростовний (частково істинний) R-предикат, якщо F(P) = та ( ) ( ) P T P ;
– тотально хибний R-предикат, якщо F(P) =
V
А та (P) = ;
– тотально істинний R-предикат, якщо T(P) =
V
А та (P) = .
Поєднання відповідних умов дає, зокрема, такі важливі класи GND-предикатів:
– TSG-предикати (умови T(P)F(P) = та T(P)F(P) =
V
A);
– TS-предикати (умови T(P)F(P) = , T(P)F(P) =
V
A та (P) = );
– STIG-предикати (умови (P) =
V
A та T(P)F(P) = );
– TTIG-предикати (умови (P) =
V
A та T(P)F(P) =
V
A);
– TSTIG-предикати (умови (P) =
V
A, T(P)F(P) = та T(P)F(P) ) =
V
A);
В класі V-A-квазіарних GND-предикатів можна виділити 7 константних. Предикат P:
– тотожно істинний (позн. T), якщо F(P) = (P) = та T(P) =
V
А;
– тотожно хибний (позн. F), якщо T(P) = (P) = та F(P) =
V
А;
– тотально істинно-невизначений (позн. T
), якщо T(P) = (P) =
V
А та F(P) = ;
– тотально хибно-невизначений (позн. F
), якщо F(P) = (P) =
V
А та T(P) = ;
– тотожно невизначений (позн. ), якщо T(P) = F(P) = та (P) =
V
А;
– тотально амбівалентний R-предикат (позн. ), якщо T(P) = F(P) =
V
А та (P) = ;
– тотально недетермінований (позн.
), якщо T(P) = F(P) = (P) =
V
А.
При цьому T, F, , є константними R-предикатами.
Беручи до уваги області невизначеності та амбівалентності, можна виділити також низку спеціальних
класів GND-предикатів, які не є R-предикатами, окрім вироджених випадків. V-A-квазіарний GND-предикат P:
Теоретичні та методологічні основи програмування
34
– AU-предикат, якщо T(P)F(P) (P);
– UA-предикат, якщо (P) T(P)F(P);
– U=A-предикат, якщо (P) = T(P)F(P);
– nU=A-предикат, якщо ( )P T(P)F(P);
– AnU-предикат, якщо T(P)F(P) ( );P
– ImG-предикат (with imprecise values), якщо ( )P T(P)F(P).
Для кожного ImG-предиката P не існує даних на яких P приймає значення лише T або лише F.
Твердження 1. Для введених спеціальних класів GND-предикатів маємо такі властивості.
1. Неоднозначні AU-предикати не є R-предикатами; SG-предикати гарантовано є AU-предикатами.
2. За умови (P) = кожний AU-предикат та кожний U=A-предикат стає TS-предикатом.
3. Кожний UA-предикат тотальний: dT(P)F(P) dT(P)F(P) (UA) d(P) суперечність
з (G).
4. Кожний U=A-предикат є UA-предикатом, тому кожний U=A-предикат – тотальний.
5. Тотальні R-предикати (T-предикати) є UA-предикатами.
6. Кожний UA-предикат та кожний U=A-предикат з умовою (P) ≠ не є R-предикатом.
7. Кожний R-предикат є AnU-предикатом: для R-предикатів T(P) F(P) (P) = , що дає AnU-умову.
8. Кожний SG-предикат є AnU-предикатом.
9. Для R-предикатів ImG-умова дає вироджений клас із умовою T(P) = F(P).
10. Кожний TIG-предикат є ImG-предикатом; кожний TAmG-предикат є ImG-предикатом.
Нехай – це назва одного із визначених вище класів GND-предикатів (напр., SG, TIG).
Відповідний клас V-A-квазіарних -предикатів позначаємо V–A (напр., PrSGV–A, PrTIGV–A).
Твердження 2. Поєднуючи умови UA та U=A із умовою T(P)F(P) =
V
A, отримуємо (див пп. 3 та 4
твердження 1) ті ж самі класи тотальних предикатів: PrUAV–A = PrTUAV–A; PrU=AV–A = PrTU=AV–A .
Твердження 3. Поєднуючи умови AU, AnU, ImG, nU=A, UA, U=A із T(P)F(P) = , маємо відомі класи:
PrSAUV–A = PrSAnUV–A = PrSGV–A; PrSImGV–A = PrSnU=AV–A = PrSTIGV–A; PrSUAV–A = PrSU=AV–A = PrTSV–A.
Твердження 4. Поєднуючи умови AU, ImG, AnU, nU=A із умовою T(P)F(P) =
V
A, отримуємо нові класи
тотальних предикатів: PrTAUV–A, PrTImGV–A, PrTAnUV–A, PrTnU=AV–A .
2. Композиції GND-предикатів
Композиції квазіарних GND-предикатів як засоби побудови складніших предикатів із простіших мають
враховувати особливості недетермінованих предикатів. Пропозиційні композиції (логічні зв’язки) задаємо через
області істинності, хибності та невизначеності відповідних предикатів.
Для композиції заперечення маємо:
T(P) = F(P), F(P) = T(P), (P) = (P).
При визначенні диз’юнкції беремо до уваги таке: PQ невизначений на d P та Q невизначені на d
або P невизначений на d та Q хибний на d або Q невизначений на d та P хибний на d. Тому задаємо:
T(PQ) = T(P) T(Q), F(PQ) = F(P) F(Q),
(PQ) = ((P) (Q)) ((P) F(Q)) (F(P) (Q)).
Композиції та – це базові пропозиційні композиції GND-предикатів.
Композиції та & є похідними, вони задаються через та : PQ = P Q; P&Q = (P Q).
Теоретичні та методологічні основи програмування
35
Звідси, зокрема, для кон’юнкції отримуємо: (P&Q) = ((P) (Q)) ((P) T(Q)) (T(P) (Q)).
Це узгоджується із такою природною умовою для кон’юнкції: P&Q невизначений на d P та Q
невизначені на d або P невизначений на d та Q істинний на d або Q невизначений на d та P істинний на d.
Твердження 5. Безпосередньо із визначень отримуємо [10] такі співвідношення:
– T(PQ) (PQ) = T(P) (P) T(Q) (Q); F(PQ) (PQ) = (F(P) (P)) (F(Q) (Q));
– F(P&Q) (P&Q) = F(P) (P) F(Q) (Q); T(P&Q) (P&Q) = (T(P) (P)) (T(Q) (Q)).
Покажемо тепер коректність так визначених композицій та для GND-предикатів. Це означає, що
та мають зберігати умову (G).
Теорема 1. Якщо для GND-предикатів P та Q виконується умова (G) то вона виконується для P та PQ.
Для маємо: F(P) T(P) (P) = T(P) F(P) (P) =
V
A. Покажемо, що зберігає умову (G).
Маємо T(P) F(P) (P) =
V
A та T(Q) F(Q) (Q) =
V
A. Треба довести: T(PQ) F(PQ) (PQ) =
V
A.
Нехай супротивне: маємо умови (G) для P та Q, проте (G) невірна для PQ. Останнє означає: для
деякого d
V
A маємо dT(PQ) F(PQ) (PQ), звідки dF(PQ) (PQ) та dT(PQ). Згідно
твердження 5 звідси маємо (d(F(P) (P)) (F(Q) (Q)) та dT(P) T(Q)) (dF(P) (P) та
dT(P) T(Q)) або (dF(Q) (Q) та dT(P) T(Q)) (dF(P), d(P), dT(P), dT(Q)) або (dF(Q),
d(Q), dT(P), dT(Q) (dF(P) (P) T(P) та dT(Q)) або (dF(Q) (Q) T(Q) та dT(P)). Перша
умова суперечить умові (G) для P, друга – умові (G) для Q. Отримали суперечність, що й доводить
збереження композицією умови (G).
Твердження 6. (P(QS)) = ((PQ)S) = (F(P)F(Q)(S)) (F(P)(Q)F(S))
((P)F(Q)F(S)) (F(P)(Q)(S)) ((P)F(Q)(S)) ((P)(Q)F(S)) ((P)(Q)(S));
(P&(Q&S)) = ((P&Q)&S) = (T(P)T(Q)(S)) (T(P)(Q)T(S)) ((P)T(Q)T(S))
(T(P)(Q)(S)) ((P)T(Q)(S)) ((P)(Q)T(S)) ((P)(Q)(S)).
Подібним чином можна задати -oбласті для диз’юнкції та кон’юнкції 4-х і більше предикатів.
Теорема 2. Для GND-предикатів виконуються такі закони традиційної логіки.
1) Комутативність та &: PQ = QP; P&Q = Q&P.
2) Асоціативність та & (випливає з твердження 6): (PQ)R = P(QR); (P&Q)&R = P&(Q&R).
3) Зняття подвійного заперечення: P = Р.
4) Ідемпотентність та &: Р = РР; Р = Р&Р.
5) Закони де Моргана: (PQ) = P & Q; (P&Q) = P Q.
Приклад 1 (див. [10]). Маємо T(P&Q P) = T((PQ) & P) = T(P), F(P&Q P) = F((PQ) & P) = F(P);
водночас (P&Q P) = ((PQ) & P) = (P) (F(P) T(P) (Q)).
Це можна трактувати так: при ускладненні опису предиката зростає невизначеність його функціонування
(наростає “ентропія” опису). При переході від простого опису предиката P до складнішого із залученням Q до
цього опису, до -області (P) додається компонента F(P) T(P) (Q), яка може бути ≠ .
Таким чином, предикати P, (PQ) & P, P&Q P збігаються в класі R-предикатів, водночас предикати
(PQ) & P та P&Q P збігаються в класі GND-предикатів, проте вони не збігаються із P.
Приклад 2. Маємо ((P&R)(Q&R)) = ((PQ)&R) (((P)(Q)) F(R) T(R)).
Тут маємо ((PQ)&R) = (T(P)(R))((P)(R))(T(Q)(R))((Q)(R))(F(P)(Q)T(R))
((P)F(Q)T(R))((P)(Q)T(R)). Ці подання отримуємо на основі визначення та твердження 5.
Теоретичні та методологічні основи програмування
36
Приклад 3. Візьмемо d
V
А таке: d(P), d(Q), dF(Q), d(R), dF(R), dT(R).
Маємо d(P) F(R) T(R), звідки d((P)(Q)) F(R) T(R), тому d((P&R)(Q&R)).
Водночас із умов d(R), d(Q) та dF(Q) згідно прикладу 2 отримуємо d((PQ)&R).
Ми отримали, що предикати (PQ)&R та (P&R)(Q&R) не збігаються в класі GND-предикатів, проте
вони збігаються в класі R-предикатів. Таким чином, приклади 1 – 3 засвідчують наступне.
Теорема 3. Для GND-предикатів не виконуються такі важливі закони традиційної логіки:
– закони поглинання для та &;
– закони дистрибутивності для та &.
Теорема 4. Пропозиційні композиції GND-предикатів виводять за межі R-предикатів.
Нехай R-предикат P є дуальним [6] до R-предиката P. Це означає: ( ) ( ), ( ) ( ).T P F P F P T P
Для R-предикатів P та P маємо: ( ) ( ) ( ) ( ) ( ),P T P F P T P F P ( ) ( ) ( ) ( ) ( );P F P T P F P T P
( ) ( ) ( ) ( ) ( ( ) ( ))T P P F P P T P F P F P T P
V
А, ( ) ( ) ( ( ) ( )) ( ) ( ) ;T P P F P P T P F P F P T P
( & ) ( & ) ( ( ) ( )) ( ) ( )T P P F P P T P F P F P T P
V
А, ( & ) ( & ) ( ) ( ) ( ( ) ( )) .T P P F P P T P F P F P T P
Отже, як R-предикати P P та &P P є TS-предикатами [6], для них -області – це .
Тепер потрактуємо P P та &P P як GND-предикати. -області таких GND-предикатів:
( ) ( ( ) ( )) ( ( ) ( )) ( ( ) ( ))P P P P P F P F P P ( ( ) ( )) ( ( ) ( )) ( ) ( );T P F P F P T P P P
( & ) ( ( ) ( )) ( ( ) ( )) ( ( ) ( ))P P P P P T P T P P ( ( ) ( )) ( ( ) ( )) ( ) ( ).T P F P F P T P P P
Нехай R-предикат P такий: F(P) T(P) або ( ) ( )T P F P . Тоді ( )P P та ( & )P P .
Отже, P P та &P P вже не є R-предикатами.
Наведемо ще один приклад на підтвердження теореми 4.
Приклад 4. Нехай R-предикат P такий, що F(P) T(P) ; тоді &P P P не є R-предикатом.
Kомпозицію реномінації R :v
x V A V APrG PrG для GND-предикатів задаємо так, як і для R-предикатів:
R ( )[ ] [r ( )]v v
x xP d P d для кожного d
V
А; тут r :v
x
V
А
V
A – операція реномінації ІМ (див. [6]).
Композицію R v
x можна визначити через T-область, F-область, -область відповідного предиката R ( )v
x P :
(R ( ))v
xT P = {d
V
A | r ( ) ( )};v
x d T P (R ( ))v
xF P = {d
V
A | r ( ) ( )};v
x d F P (R ( ))v
x P = {d
V
A | r ( ) ( )}v
x d P .
Основні властивості композицій реномінації для GND-предикатів такі ж як (див. [3, 6]) для R-предикатів.
R) R( ) P P – тотожна реномінація; композиція R без параметрів діє як тотожне відображення.
RI)
,
,R ( ) R ( )z v v
z x xP P – згортка тотожної пари імен у реномінації;
RU) ,
,R ( ) R ( )z v v
y x xP P , якщо z неістотне [3, 6] для P, – згортка пари імен з неістотним верхнім іменем;
RR) R (R ( )) R ( )v w v w
x y x yP P ; тут Rv w
x y – згортка [3, 6] композицій реномінації R v
x та Rw
y ;
R) R ( ) R ( ) v v
x xP P – R-дистрибутивність;
R) R ( ) R ( ) R ( ) v v v
x x xP Q P Q – R-дистрибутивність.
Теоретичні та методологічні основи програмування
37
Опишемо композиції квантифікації x : V A V APrG PrG та x : V A V APrG PrG .
Задаємо предикат xP через його області істинності, хибності та невизначеності.
T(xP) = {d
V
A | d x a T(Р) для деякого aA}; F(xP) = {d
V
A | d x a F(Р) для всіх aA};
(xP) = {d
V
A | d x a (Р) F(Р) для всіх aA та d x b (Р) для деякого bA}.
Композицію x віднесемо її до базових. Композиція х є похідною, її задаємо традиційно: хР = хР.
Твердження 7 (див. [10]). d (xP)
T(xP) d x b T(Р)
(P) для деякого bA;
d (xP)
F(xP) d x a F(Р)
(P) для всіх aA.
Основні властивості композицій квантифікації GND-предикатів такі ж, як (див. [3, 6]) для R-предикатів.
1. Комутативність однотипних кванторів: xуР = ухР; xуР = ухР.
2. Закони де Моргана для кванторів: хР = хР; хР = хР.
3. Неістотність квантифікованих імен: xхР = хР; xхР = хР; xхР = хР; xхР = хР.
4. Дистрибутивність кванторів щодо та &: хР хQ = х (РQ); хР &xQ = х (Р&Q).
Наведемо властивості x, пов’язані з реномінацією; відповідні властивості x записуються аналогічно.
RR) ,
,R (u x
v y хP) = R (u
v хP).
Ren) R ( )y
zyP z P за умови z неістотне для P – перейменування кванторного імені.
Rs) R ( ) R ( )v v
x xyP y P за умови { , }y v x – проста (обмежена) R-дистрибутивність.
R) R ( ) R ( )v v y
x x zyP z P за умови неістотне для P та { , }z v x – R-дистрибутивність.
Для опису властивостей елімінації кванторів використовують [6] спеціальні предикати-індикатори Ez
наявності в даних компоненти з відповідним zV. На рівні GND-предикатів такі Ez задаємо наступним чином:
T(Ez) = {d | d(z)}, F(Ez) = {d | d(z)}, (Ez) = .
Таким чином, предикати-індикатори Ez тотальні та однозначні, вони є TS-предикатами.
Твердження 8. Для кожного PrGV–A : (Ez) = ()F(Ez) (); (Ez) = ()T(Ez) ()};
(Ez)T(Ez) = ()T()T(Ez) ()T(); (Ez)F(Ez) = ()F()F(Ez) ()F().
Композиції , , R ,v
x x – це базові композиції чистих першопорядкових логік GND-предикатів.
3. Композиційні алгебри GND-предикатів
Композиційну алгебру AQGV–A = (PrGV–A, CQ), де CQ = {, , R ,v
x x} – множина базових композицій,
назвемо чистою першопорядковою алгеброю GND-предикатів.
Композиційну алгебру ARGV–A = (PrGV–A, CR), де CR = {, , R v
x } – множина базових композицій,
назвемо реномінативною алгеброю GND-предикатів, або алгеброю GND-предикатів реномінативного рівня.
Композиційну алгебру APGV–A = (PrGV–A, CP), де CP = {, } – множина базових композицій, назвемо
пропозиційною алгеброю GND-предикатів, або алгеброю GND-предикатів пропозиційного рівня.
Зв’язок GND-предикатів та 7-значних тотальних детермінованих предикатів, або TD7-предикатів,
досліджено в [10]. Описано низку підалгебр алгебри APGV–A, індукованих підалгебрами алгебри TD7-предикатів
AТD7V–A = (PrTD7V–A, {, }). Ці підалгебри в свою чергу індукуються відповідними підалгебрами алгебри
істиннісних значень ATV7 = (TV7, {, }), де TV7 = {, T, F, TF, T, F, TF}.
Теоретичні та методологічні основи програмування
38
Подібним чином підалгебри алгебри ATV7 індукують відповідні підалгебри реномінативної алгебри
ARGV–A та підалгебри першопорядкової алгебри AQGV–A . Назви таких підалгебр формуємо із вказівки рівня
розгляду та назви класу GND-предикатів. Наприклад, AQSGV–A – алгебра SG-предикатів кванторного рівня.
Композиції та для 7-значних предикатів задаються [10] за допомогою таблиць істинності (табл. 1, 2).
Таблиця 1. Композиція
P T F TF T F TF
P F T TF F T TF
Таблиця 2. Композиція
T F TF T F TF
T T T T T T T T
F T F TF T F TF
TF T TF TF T T TF TF
T T T T
T T T T T T T T
F T F TF T F TF
TF T TF TF T T TF TF
Похідні композиції та & виражаються через та : P Q = P Q; P & Q = (P Q).
Зв’язок алгебр ATV7 та APGV–A встановлюється [10] так. Наявність певного істиннісного значення в TV7
означає, що існують предикат PPrGV–A та d
V
A такі, що P[d].
Для опису підалгебр ATV7 виділено [10] усі підмножини множини TV7, замкнені щодо {, }:
6-елементні TV6_1 = {, T, F, T, F, TF} та TV6_2 ={ T, F, TF, T, F, TF};
5-елементні TV5_1 = {, T, F, T, F}, TV5_2 = {T, F, T, F, TF}, TV5_3 = {, T, F, TF, TF};
4-елементні TV4_1 = {T, F, T, F}, TV4_2 = {T, F, TF, TF}, TV4_3 = {TF, T, F, TF}; TV4_4 = {, T, F, TF};
3-елементні TV3_1 = {T, F, }, TV3_2 = {T, F, TF}, TV3_3 = {T, F, TF}, TV3_4 = {T, F, TF}, TV3_5 = {, T, F};
2-елементні TV2_1 = {T, F}, TV2_2 = {T, F}, TV2_3 = {TF, TF};
1-елементні TV1_1 = {}, TV1_2 = {TF}, TV1_3 = {TF}.
Ці підмножини TVm_n задають відповідні підалгебри ATVm_n алгебри ATV7. Далі ці підалгебри індукують
відповідні підалгебри алгебри AТD7V–A , які в свою чергу індукують наступні підалгебри алгебри AQGV–A :
AQAUV–A, AQTGV–A;
AQSGV–A, AQTAUV–A, AQImGV–A;
AQТSGV–A, AQТUAV–A, AQТІmGV–A, AQTIGV–A;
AQРV–A, AQTV–A, AQTU=A V–A, AQTTIGV–A, AQSTIGV–A;
AQTSV–A, AQTSTIGV–A, AQTAmGV–A;
AQV–A, AQV–A, AQV–A .
Підалгебри ATVm_n подібним чином індукують відповідні підалгебри алгебри APGV–A та алгебри ARGV–A:
Не всі описані класи GND-предикатів замкнені щодо введеної вище композиції . Це, зокрема, клас
R-предикатів та специфічні класи nU=A-предикатів, AnU-предикатів, TnU=A-предикатів, TAnU-предикатів. Цим
класам зіставлено класи TD7-предикатів, для яких множинами іститннісних значень є відповідно {T, F, , TF},
Теоретичні та методологічні основи програмування
39
{, T, F, TF}, {T, F, , T, F, TF}, {T, F, TF}, {T, F, T, F, TF}; ці множини незамкнені щодо .
Опишемо відношення між виділеними підалгебрами алгебри AQGV–A.
Пишемо A B, якщо A є підалгеброю B. Те, що алгебри A та B ізоморфні, позначаємо A iz B.
Теорема 5. Маємо наступні співвідношення:
, ;V A V A V AAQAU AQTG AQG
, ;V A V A V AAQSG AQTAU AQAU ;V A V AAQTAU AQTG ;V A V AAQImG AQG – ;V A iz V AAQSG AQTAU
, ;V A V A V AAQTSG AQSG AQTAU , ;V A V A V AAQTUA AQTImG AQTG ;V A V AAQTIG AQAU
, ;V A V A V AAQTIG AQTImG AQImG
;V A V AAQP AQSG , ;V A V A V AAQT AQTU A AQTUA , ;V A V A V AAQTTIG AQTU A AQTAU
, ;V A V A V AAQTTIG AQTImG AQTIG , ;V A V A V AAQSTIG AQSG AQTIG
– – – ;V A iz V A iz V A iz V A iz V AAQP AQT AQTU A AQTTIG AQSTIG
, , , ;V A V A V A V A V AAQTS AQP AQT AQTSG AQTU A , , ;V A V A V A V AAQTSTIG AQTTIG AQSTIG AQTSG
, ;V A V A V AAQTAmG AQTUA AQTImG – ;V A iz V AAQTS AQTSTIG
, ;V A V A V AAQ AQP AQSTIG , ;V A V A V AAQ AQTAmG AQT
, , ;V A V A V A V AAQ AQTAmG AQTU AG AQTTIG – – V A iz V A iz V AAQ AQ AQ .
Чиста першопорядкова алгебра R-предикатів AQRV–A не індукована жодною підалгеброю алгебри TV7, але
вона є вкладенням в алгебри AQImGV–A та AQAUV–A; при цьому AQRV–A iz AQTIGV–A.
Аналогічні відношення є між відповідними підалгебрами алгебри APGV–A та алгебри ARGV–A .
Виділеним підалгебрам алгебри АТV7 відповідають сингулярні алгебри GND-предикатів, носії яких
складені з константних предикатів T, F, , T
, F
, ,
. Зокрема, це 1-елементні алгебри
Q
V–A,
Q
V–A,
Q
V–A .
4. Мови чистих першопорядкових логік GND-предикатів
Мови чистих першопорядкових логік GND-предикатів із синтаксичного погляду ідентичні відомим [2, 3]
мовам ЧКНЛ. Алфавiт мови: множини { , , , } v
xCs R x символів базових композицій; множина V предметних
імен (змінних), в якій виділена множина U V тотально неістотних імен; множина Ps предикатних символів.
Визначення множини Fr формул: Ps Fr; , Fr , Ф, ,v
xR xFr.
Для запису формул використовуємо префіксну форму запису. Для зручності вживаємо [2] скорочення
формул, користуючись символами похідних композицій та інфіксною формою запису для бінарних
композицій.
В логіці GND-предикатів клас інтерпретацій істотно ширший порівнянно з логікою R-предикатів.
Інтерпретуємо мову на композиційних системах вигляду CS = (A, PrGV–A, CQ). Символи Cs позначають
відповідні композиції, імена xV – елементи множини A. Символи Рs позначають базові предикати в PrGV–A,
для його опису задамо тотальне однозначне відображення :I Ps PrGV–A, яке розширимо до відображення
інтерпретації формул :I Fr PrGV–A так:
I() = (I()), I() = (I(), I()), ( ) R ( ( )); v v
x xI R I I(x) = x(I()).
Трійки J = (CS, , I) – це інтерпретації мови сигнатури = (V, U, Cs, Ps). Cкорочено їх позначаємо (A, I).
Предикат J() – значення формули при інтерпретації J – позначимо J.
Виділення класів GND-предикатів та відповідних підалгебр алгебри AQGV–A виділяє класи
інтерпретацій GND-предикатів. Тому маємо загальний клас G-інтерпретацій та низку підкласів цього класу.
Такі класи інтерпретацій називають семантиками. Таким чином, можна говорити про загальну G-семантику
Теоретичні та методологічні основи програмування
40
та, зокрема, про семантики AU, TG, SG, TAU, ImG, ТSG, ТAU, ТІmG, TIG, Р, T, TU=A, TTIG, STIG, TS,
TSTIG, TAmG.
Відому R-семантику можна трактувати як “вкладення” в G-семантику. Якщо “абстрагуватись” від
областей невизначеності предикатів, явно їх не виділяючи, то властивості R-предикатів аналогічні
властивостям TIG-предикатів, що засвідчує ізоморфізм алгебр AQRV–A та AQTIGV–A . При цьому для
TIG-предикатів (P) =
V
A, а для R-предикатів ( ) ( ) ( ) P T P F P . В обох випадках область невизначеності
окремої ролі не грає.
Логіки -предикатів назвемо логіками з -семантикою ( – один з визначених вище класів предикатів).
Далі зосередимося на вивченні загального класу логік із G-семантикою та логік із SG-семантикою.
Відношення логічного наслідку в логіці GND-предикатів описане в [10]. Нагадаємо відповідні визначення.
Відношення G-наслідку J|=G для двох формул при фіксованій інтерпретації J задаємо так:
J|=G T(J) T(J) та F(J) F(J) та (J) (J) T(J) та (J) (J) F(J).
Неформально те, що J є наслідком J означає: при переході від J до J істинність може лише
збільшитися, а хибність лише зменшитися, невизначеність переходить у невизначеність або істинність, у
невизначеність переходить невизначеність або хибність.
Відношення логічного G-наслідку |=G визначаємо так: |=G , якщо J|=G для кожної інтерпретації J.
Відношення логічного SG-наслідку
SG
|=G задаємо так:
SG
|=G , якщо J|=G для кожної JSG.
Відношення J|=G рефлексивне й транзитивне [10]. Тому |=G та
SG
|=G теж рефлексивні й транзитивні.
Для відношення J|=G справджується [10] закон контрапозиції: J|=G J|=G . Звідси:
Твердження 9. |=G |=G ;
SG
|=G
SG
|=G .
Відношення G-еквівалентності при інтерпретації J визначаємо так: JG , якщо J|=G та J|=G .
Відношення логічної G-еквівалентності визначаємо так: G , якщо |=G та |=G .
Відношення логічної SG-еквівалентності визначаємо так:
SG
G , якщо
SG
|=G та
SG
|=G .
Твердження 10. G JG для кожної інтерпретації J;
SG
G JG для кожної JSG.
Для логіки GND-предикатів умова G не означає повну збіжність предикатів J та J. Справді, якщо
JG , то T(J) = T(J) та F(J) = F(J), позначимо ці множини як Т та F. При цьому (J) та (J) можуть
відрізнятися, проте [10] лише в T F. Приклад такої відмінності – (J) та (J & J J). При цьому
|=G & та G () & (див. [10]). Водночас ситуація нормалізується для логіки SG-предикатів.
Для SG-предикатів завжди T(J) F(J) = , тому
SG
G означає повну збіжність предикатів J та J .
В [10] показано монотонність відношення J|=G : J|=G &A J|=G B.
Звідси монотонність відношень |=G та
SG
|=G : |=G &A |=G B;
SG
|=G &A
SG
|=G B.
Теорема 6 (еквівалентності). Нехай ' отримана з замiною деяких входжень 1,..., n на 1,..., n.
1) Якщо 1 G 1, ..., n G n, то G '; 2) Якщо 1
SG
G 1, ..., n
SG
G n, то
SG
G '.
Для відношення J|=G виконуються властивості декомпозиції формул (див. [10]):
AB J|=G A J|=G та B J|=G ; D J|=G (PQ) D J|=G P та D J|=G Q.
Звідси випливають аналогічні властивості для відношень логічного наслідку |=G та
SG
|=G .
Опишемо умови гарантованої наявності логічного наслідку для відношень |=G та
SG
|=G .
Теорема 7. Для довільних формул , A, B маємо &A |=G B та &A
SG
|=G B.
Теорема 8. Для довільних формул , маємо &
SG
|=G .
Для кожного SG-предиката P маємо T(P)F(P) = . Тому для довільних формул , та JSG маємо
T(&J) T(J) та F(J) F(&J). -умова для & J|=G виконується гарантовано:
Теоретичні та методологічні основи програмування
41
(&J) (J) T(J) = (J) T(J) F( J) =
V
A
(J) (&J) F(&J) = (J) F(PJ) T(J) =
V
A .
5. Відношення логічного наслідку для множин формул
Нехай Fr, Fr. Введемо позначення ( )JT
як ( ) JT , ( )JF
як ( ) JF , ( )JT
як
( ) JT , ( )JF
як ( ) JF ,
це чи ,
хоч одне це
(( ) )
і i
і
i i J
T
як ( ) J ,
це чи ,
хоч одне це
(( ) )
і i
і
i i J
F
як ( ) J .
Замість {, }J будемо також скорочено писати , J.
Умова (G) та твердження 5 і 6 стосовно множин формул узагальнюється так.
Твердження 11 (умова GS). Нехай формули множини трактуємо як поєднані кон’юнкцією, а формули
множини – як поєднані диз’юнкцією. Тоді T
(J) F
(J)
(J) =
V
A та T
(J) F
(J)
(J) =
V
A.
Твердження 12. Нехай формули множини {, } трактуємо як поєднані кон’юнкцією, а формули
множини {, } – як поєднані диз’юнкцією. Тоді:
– T
(, J) = TT; F
( J) = FF; T
(, J) = TT; F
(, J) = FF;
–
(, J) = ()(T)(T);
(, J) = ()(F)(F);
–
(, J) T
(, J) = TT;
(, J) F
(, J) = (F)(F);
–
(, J) T
(, J) = (T)(T);
(, J) F
(, J) = FF.
Тут і далі будемо позначати T
(J) як T, T
(J) як T, F
(J) як F, F
(J) як F,
(J) як ,
(J) як ;
для формул вводимо позначення T(J) як T, F(J) як F, (J) як (інтерпретацію J вважаємо зафіксованою).
Теорема 9. 1)
(J) T
(J) = ( ) ( )J JT
; 2)
(J) F
(J) = ( ) ( )J JF
.
Теорема доводиться індукцією за кількістю формул множини .
є G-наслідком при J (позн. J|=G ), якщо:
T
(J) T
(J), F
(J) F
(J),
(J)
(J) T
(J),
(J)
(J) F
(J).
Відношення логічного наслідку |=G та
SG
|=G для множин формул визначаємо так:
|=G , якщо J|=G для кожної інтерпретації J;
SG
|=G , якщо J|=G для кожної JSG.
Теорема 10. Відношення J|=G, |=G,
SG
|=G для множин формул рефлексивні: J|=G , |=G ,
SG
|=G .
Теорема 11. Відношення J|=G для множин формул монотонне: J|=G , J|=G , .
Для перевірки умов для -областей використовуємо твердження 12.
Наслідок 1. Відношення |=G та
SG
|=G монотонні: |=G , |=G , ;
SG
|=G ,
SG
|=G , .
Теорема 12. J|=G та JG J|=G ; & J|=G та JG & J|=G .
Наслідок 2 (теорема заміни еквівалентних для відношень |=G та
SG
|=G ).
1) |=G , та G |=G , ; , |=G та G , |=G .
2)
SG
|=G , та
SG
G
SG
|=G , ; ,
SG
|=G та
SG
G ,
SG
|=G .
Теорема 13 (гарантована наявність J|=G). , J|=G , .
Теоретичні та методологічні основи програмування
42
Наслідок 3. Для довільних , Fr та Fr маємо: , |=G , ; ,
SG
|=G , .
Таким чином, наявність відношення |= гарантує наступна властивість (тут |= – |=G або
SG
|=TF):
С) , |= , .
Наявність відношення логічного наслідку |=TF логіки R-предикатів теж гарантує [3, 6] властивість С.
Теорема 14. Для довільних , Fr та , Fr маємо: , ,
SG
|=G , , .
Таким чином, наявність відношення
SG
|=G додатково гарантує така властивість:
СLR) , ,
SG
|=TF , , .
Властивість СLR також гарантує [3, 6] наявність відношення
P
|=TF логіки P-предикатів.
Для відношень |=G та
SG
|=G для множин формул, маємо властивості еквівалентних перетворень. Це
властивості спрощення зовнішньої реномінації та властивості згортки реномінацій і пронесення реномінації
через логічні зв’язки та квантори. Ці властивості базуються на відповідних властивостях композицій
GND-предикатів: R, RI, RU (властивості спрощення); RR, R, R, Rs, R. Кожна з них продукує (при цьому
використовується теорема заміни еквівалентних) 4 відповідні властивості для відношення логічного наслідку
для множин формул, коли виділена формула чи її заперечення знаходиться у лівій чи правій частині цього
відношення.
Властивості еквівалентних перетворень для відношень |=G та
SG
|=G аналогічні відповідним властивостям
для відношення |=TF (див. [6]). Наведемо для прикладу властивості, індуковані R (|= – це |=G чи
SG
|=TF).
RL) ( ),v
xR |= ( ) ( ),v v
x xR R |= ;
RR) |= ( ),v
xR |= ( ) ( ),v v
x xR R ;
RL) ( ),v
xR |= ( ( ) ( )),v v
x xR R |= ;
RR) |= ( ),v
xR |= ( ( ) ( )),v v
x xR R .
Опишемо властивості декомпозиції формул для відношень логічного наслідку для множин формул.
Твердження 13. , J|=G , J|=G ; J|=G , J|=G , .
Наслідок 4. , |= , |= ; |= , |= , (тут |= – це |=G чи
SG
|=TF).
Твердження 14. J|=G , J|=G , , ; &, J|=G , , J|=G .
Для кожної інтерпретації J маємо ()J = (&)J. Звідси:
Твердження 15. (), J|=G &, J|=G , , J|=G .
Наслідок 5. |= , |= , , ; (), |= , , |= (|= – це |=G чи
SG
|=TF).
Теорема 15. , J|=G , J|=G та , J|=G ;
J|=G (), J|=G , та J|=G .
При доведенні теореми 15 використовуємо твердження 5 та 12.
Наслідок 6. , |= , |=G та , |=G ;
|= (), |= , та |= (тут |= – |=G або
SG
|=TF).
Для отримання наслідку 6 із теореми 15 використовуємо такий закон традиційної логіки:
J ((J) (J)) ( J (J) J (J)) (*)
Теоретичні та методологічні основи програмування
43
Підсумовуючи, маємо такі властивості декомпозиції формул (|= – це |=G чи
SG
|=G):
L) , |= , |= .
R) |= , |= , .
L) , |= , |= та , |= .
R) |= , |= , , .
L) (), |= , , |= .
R) |= , () |= , та |= , .
Таким чином, для відношень |=G та
SG
|=G отримано традиційні властивості декомпозиції формул. Ці
властивості ідентичні властивостям декомпозиції для відношень
R
|=TF та
P
|=TF логіки R-предикатів (див. [6]).
Розглянемо тепер властивості елімінації кванторів.
За монотонністю відношення J|=G (теорема 11) маємо:
Твердження 16. Ey, J|=G х, Ey, J|=G х, , x
yR ; х, , , xyR Ey J|=G х, Ey, J|=G .
Зворотні імплікації гарантує
Теорема 16. Ey, J|=G х, , x
yR Ey, J|=G х, ; х, , , xyR Ey J|=G х, Ey, J|=G .
Доведення полягає в перевірці виконання відповідних умов для T-областей, F-областей та -областей,
які мають виконуватися для цих відношень J|=G . Перевірка умов для T-областей та F-областей така ж, як для
відношення J|=TF логіки R-предикатів. При перевірці умов для -областей використовуються твердження 5, 7 та
12, а також твердження 8 стосовно предикатів-індикаторів Ey.
Теорема 17. х, J|=G , ,x
zR Ez J|=G , де zfu(, , );
J|=G х, Ez, | , ,x
J G zR де zfu(, , ).
Перевірка відповідних умов для T-областей та F-областей така ж, як для відношення J|=TF логіки
R-предикатів. При перевірці умов для -областей використовуються твердження 5, 7, 8 та 12.
Згідно (*) із твердження 15 та теорем 16 і 17 маємо властивості елімінації кванторів (|= – це |=G чи
SG
|=G):
L) х, |= , , |x
zR Ez , zfu(, , );
R) |= х, , | ,x
zEz R , zfu(, , );
vR) Ey, |= х, Ey, |= х, , x
yR ;
vL) х, Ey, |= х, , , xyR Ey |= .
Вони ідентичні властивостям елімінації кванторів для відношень |=TF та
P
|=TF логіки R-предикатів [6].
Розглянемо властивості E-розподілу та первісного означення. При заданій J = (A, I) вони мають вигляд:
IEd) J|=G Ey, J|=G та J|=G , Ey;
IEv) J|=G Ez, J|=G за умови zfu(, ).
Позначаємо: T
(J), T
(J), F
(J), F
(J),
(J),
(J) як T, T, F, F, , ; T(Ey) як y, F(Ey) як y.
Твердження 17 (випливає з тверджень 8 та 12).
(Ey, J) = y ;
(Ey, J) = y ;
(Ey, J)T
(Ey, J) = T y T;
(Ey, J)F
(Ey, J) = F y F .
Теоретичні та методологічні основи програмування
44
Використовуючи твердження 17, показуємо для -областей в IEd: T та F
(Ey, J) T та
(Ey, J)F
(Ey, J) = F y
та
(Ey, J)T
(Ey, J) = T y та
(Ey, J) F.
Твердження 18. zfu(, ) та dS для всіх aA маємо d||–z + z a S; тут S – це T, T, F, F, , .
Використовуючи твердження 17 та 18, показуємо, що за умови zfu(, ) для -областей в IEv маємо:
T та F
(Ez, J) T та
(Ez, J)F
(Ez, J) = F z.
Згідно (*) із IEd та IEv отримуємо властивості E-розподілу та первісного означення (|= – це |=G чи
SG
|=G):
Ed) |= Ey, |= та |= , Ey.
Ev) |= Ez, |= за умови zfu(, ).
Вони ідентичні відповідним властивостям для відношень |=TF та
P
|=TF логіки R-предикатів (див. [6]).
Висновки
Досліджено семантичні аспекти нового класу програмно-орієнтованих логічних формалізмів – логік
загальних недетермінованих квазіарних предикатів, або GND-предикатів. Ці логіки відображають такі
властивості програм, як частковість, недетермінізм, нефіксовану арність. GND-предикати є узагальненням
відомих часткових неоднозначних предикатів реляційного типу. Виділено низку різновидів GND-предикатів,
розглянуто властивості їх композицій, описано композиційні алгебри. Показано зв'язок GND-предикатів із
7-значними тотальними детермінованими предикатами. Описано мови чистих першопорядкових логік
GND-предикатів. Досліджено відношення логічного наслідку для множин формул. Визначено відношення
G-наслідку, логічних G-наслідку та SG-наслідку, описано їх властивості. Досліджено властивості
декомпозиції формул та елімінації кванторів. На цій семантичній основі для логік GND-предикатів
планується побудова числень секвенційного типу.
Література
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. Нікітченко М.С., Шкільняк С.С. Математична логіка та теорія алгоритмів. Київ: ВПЦ Київський університет, 2008. 528 с.
3. Нікітченко М.С., Шкільняк С.С. Прикладна логіка. Київ: ВПЦ Київський університет, 2013. 278 с.
4. Nikitchenko М., Shkilniak S. Semantic Properties of Logics of Quasiary Predicates. Workshop on Foundations of Informatics: Proceedings
FOI-2015. Chisinau, Moldova. P. 180–197.
5. Шкільняк О.С. Відношення логічного наслідку в логіках квазіарних предикатів. Проблеми програмування. 2016. № 1. C. 29–43.
6. Нікітченко М.С., Шкільняк О.С., Шкільняк С.С. Чисті першопорядкові логіки квазіарних предикатів. Проблеми програмування. 2016.
№ 2–3. C. 73–86.
7. Мykola S. Nikitchenko and Stepan S. Shkilniak. Algebras and logics of partial quasiary predicates. Algebra and Discrete Mathematics.
Vol. 23 (2017). N 2, P. 263–278.
8. Avron A., Zamansky A. Non-deterministic semantics for logical systems, in Handbook of Philosophical Logic, D.M. Gabbay, F. Guenthner
(eds.), 2nd ed., Vol. 16, (2011), Springer Netherlands, P. 227–304.
9. Nikitchenko М.S., Shkilniak O.S. and Shkilniak S.S. Logics of partial non-deterministic predicates. PDMU-2017: international conference:
abstracts. – Vilnius, Lithuania. P. 94–95.
10. Нікітченко М.С., Шкільняк О.С., Шкільняк С.С. Алгебри загальних недетермінованих предикатів. Проблеми програмування. 2018.
№ 1. C. 5–21.
References
1. Abramsky S., Gabbay D. and Maibaum T. (editors). (1993–2000). Handbook of Logic in Computer Science. Oxford University Press.
2. Nikitchenko M. and Shkilniak S. (2008). Mathematical logic and theory of algorithms. Кyiv: VPC Кyivskyi Universytet (in ukr).
3. Nikitchenko M. and Shkilniak S. (2013). Applied logic. Кyiv: VPC Кyivskyi Universytet (in ukr).
4. Nikitchenko M. and Shkilniak S. (2015). Semantic Properties of Logics of Quasiary Predicates. In Workshop on Foundations of Informatics:
Proceedings FOI-2015. Chisinau, Moldova. P. 180–197.
5. Shkilniak O. (2016). Logical consequence relations in logics of quasiary predicates. In Problems in Progamming. № 1. P. 29–43 (in ukr).
6. Nikitchenko M., Shkilniak O. and Shkilniak S. (2016). Pure first-order logics of quasiary predicates. In Problems in Progamming. N 2–3.
P. 73–86 (in ukr).
7. Nikitchenko M. and Shkilniak S. (2017). Algebras and logics of partial quasiary predicates. In Algebra and Discrete Mathematics. Vol. 23.
N 2. P. 263–278.
Теоретичні та методологічні основи програмування
45
8. Avron A. and Zamansky A. (2011). Non-deterministic semantics for logical systems. In Handbook of Philosophical Logic, D.M. Gabbay,
F. Guenthner (eds.), 2nd ed., vol. 16, Springer Netherlands. P. 227–304.
9. Nikitchenko M., Shkilniak O. and Shkilniak S. (2017). Logics of partial non-deterministic predicates. In International conference PDMU-2017:
abstracts. Vilnius, Lithuania. P. 94–95.
10. Nikitchenko M., Shkilniak O. and Shkilniak S. (2018). Algebras of general non-deterministic predicates. In Problems in Progamming. N 1.
P. 5–21 (in ukr).
Про авторів:
Нікітченко Микола Степанович,
доктор фізико-математичних наук, професор,
завідувач кафедри Теорії та технології програмування.
Кількість наукових публікацій в українських виданнях – понад 250,
у тому числі у фахових виданнях – понад 110.
Кількість наукових публікацій в зарубіжних виданнях – понад 50.
Scopus Author ID: 6602842336.
H-індекс (Google Scholar): 12 (9 з 2013).
http://orcid.org/0000-0002-4078-1062,
Шкільняк Оксана Степанівна,
кандидат фізико-математичних наук,
доцент, доцент кафедри інформаційних систем.
Кількість наукових публікацій в українських виданнях – 90,
у тому числі у фахових виданнях – 34.
Кількість наукових публікацій в зарубіжних виданнях – 10.
Scopus Author ID: 57190873266.
H-індекс (Google Scholar): 3 (3 з 2013).
http://orcid.org/0000-0003-4139-2525,
Шкільняк Степан Степанович,
доктор фізико-математичних наук, професор,
професор кафедри Теорії та технології програмування.
Кількість наукових публікацій в українських виданнях – понад 230,
у тому числі у фахових виданнях – понад 100.
Кількість наукових публікацій в зарубіжних виданнях – 17.
Scopus Author ID: 36646762300
H-індекс (Google Scholar): 6 (5 з 2013).
http://orcid.org/0000-0001-8624-5778.
Місце роботи авторів:
Київський національний університет імені Тараса Шевченка,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 259 05 19.
E-mail: me.oksana@gmail.com,
nikitchenko@unicyb.kiev.ua,
sssh@unicyb.kiev.ua.
http://orcid.org/0000-0001%20-8624-5778
mailto:me.oksana@gmail.com
|