Pure first-order logics of quasiary predicates
Pure first-order logics of partial and total, single-valued and multi-valued quasiary predicates are investigated. For these logics we describe semantic models and languages, giving special attention in our research to composition algebras of predicates and interpretation classes (sematics), and log...
Збережено в:
| Дата: | 2018 |
|---|---|
| Автори: | , , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2018
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/182 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-182 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/81/06962b4f6fe07fd313fc3827c0a81581.pdf |
| spelling |
pp_isofts_kiev_ua-article-1822024-04-28T13:09:56Z Pure first-order logics of quasiary predicates Чистые логики первопорядковые порядка квазиарных предикатов Чисті першопорядкові логіки квазіарних предикатів Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. logic; predicate; semantics; logical consequence; sequent calculus UDC 004.42:510.69 логика; предикат; семантика; логическое следствие; секвенциальное исчисление УДК 004.42:510.69 логіка; предикат; семантика; логічний наслідок; секвенційне числення УДК 004.42:510.69 Pure first-order logics of partial and total, single-valued and multi-valued quasiary predicates are investigated. For these logics we describe semantic models and languages, giving special attention in our research to composition algebras of predicates and interpretation classes (sematics), and logical consequence relations for sets of formulas. For the defined relations a number of sequent type calculi is constructed; their characteristic features are extended conditions for sequent closure and original forms for quantifier elimination.Problems in programming 2016; 2-3: 73-86 Исследованы чистые первопорядковые логики частичных и тотальных, однозначных и неоднозначных квазиарных предикатов. Описаны семантические модели и языки таких логик, особое внимание уделено изучению композиционных предикатных алгебр и классов интерпретаций (семантик), отношений логического следствия для множеств формул. Для таких отношений построен ряд исчислений секвенциального типа, характерными особенностями этих исчислений являются расширенные условия замкнутости секвенции и оригинальные формы элиминации кванторов.Problems in programming 2016; 2-3: 73-86 Досліджено чисті першопорядкові логіки часткових і тотальних, однозначних і неоднозначних квазіарних предикатів. Описано семантичні моделі та мови таких логік, особливу увагу приділено вивченню композиційних предикатних алгебр та класів інтерпретацій (семантик), відношень логічного наслідку для множин формул. Для таких відношень побудовано низку числень секвенцій ного типу, характерною особливістю цих числень є розширені умови замкненості секвенції та оригінальні форми елімінації кванторів.Problems in programming 2016; 2-3: 73-86 Інститут програмних систем НАН України 2018-07-06 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/182 10.15407/pp2016.02-03.073 PROBLEMS IN PROGRAMMING; No 2-3 (2016); 73-86 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2016); 73-86 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2016); 73-86 1727-4907 10.15407/pp2016.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/182/177 Copyright (c) 2017 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2024-04-28T13:09:56Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
logic predicate semantics logical consequence sequent calculus UDC 004.42:510.69 |
| spellingShingle |
logic predicate semantics logical consequence sequent calculus UDC 004.42:510.69 Nikitchenko, M.S. Shkilniak, О.S. Shkilniak, S.S. Pure first-order logics of quasiary predicates |
| topic_facet |
logic predicate semantics logical consequence sequent calculus 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 |
Pure first-order logics of quasiary predicates |
| title_short |
Pure first-order logics of quasiary predicates |
| title_full |
Pure first-order logics of quasiary predicates |
| title_fullStr |
Pure first-order logics of quasiary predicates |
| title_full_unstemmed |
Pure first-order logics of quasiary predicates |
| title_sort |
pure first-order logics of quasiary predicates |
| title_alt |
Чистые логики первопорядковые порядка квазиарных предикатов Чисті першопорядкові логіки квазіарних предикатів |
| description |
Pure first-order logics of partial and total, single-valued and multi-valued quasiary predicates are investigated. For these logics we describe semantic models and languages, giving special attention in our research to composition algebras of predicates and interpretation classes (sematics), and logical consequence relations for sets of formulas. For the defined relations a number of sequent type calculi is constructed; their characteristic features are extended conditions for sequent closure and original forms for quantifier elimination.Problems in programming 2016; 2-3: 73-86 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2018 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/182 |
| work_keys_str_mv |
AT nikitchenkoms purefirstorderlogicsofquasiarypredicates AT shkilniakos purefirstorderlogicsofquasiarypredicates AT shkilniakss purefirstorderlogicsofquasiarypredicates AT nikitchenkoms čistyelogikipervoporâdkovyeporâdkakvaziarnyhpredikatov AT shkilniakos čistyelogikipervoporâdkovyeporâdkakvaziarnyhpredikatov AT shkilniakss čistyelogikipervoporâdkovyeporâdkakvaziarnyhpredikatov AT nikitchenkoms čistíperšoporâdkovílogíkikvazíarnihpredikatív AT shkilniakos čistíperšoporâdkovílogíkikvazíarnihpredikatív AT shkilniakss čistíperšoporâdkovílogíkikvazíarnihpredikatív |
| first_indexed |
2024-09-16T04:08:13Z |
| last_indexed |
2024-09-16T04:08:13Z |
| _version_ |
1818568385365016576 |
| fulltext |
Теоретичні та методологічні основи програмування
© М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк, 2016
ISSN 1727-4907. Проблеми програмування. 2016. № 2–3. Спеціальний випуск 73
УДК 004.42:510.69
ЧИСТІ ПЕРШОПОРЯДКОВІ ЛОГІКИ КВАЗІАРНИХ ПРЕДИКАТІВ
М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк
Досліджено чисті першопорядкові логіки часткових і тотальних, однозначних і неоднозначних квазіарних предикатів. Описано
семантичні моделі та мови таких логік, особливу увагу приділено вивченню композиційних предикатних алгебр та класів інтер-
претацій (семантик), відношень логічного наслідку для множин формул. Для таких відношень побудовано низку числень секве-
нцій ного типу, характерною особливістю цих числень є розширені умови замкненості секвенції та оригінальні форми еліміна-
ції кванторів.
Ключові слова: логіка, предикат, семантика, логічний наслідок, секвенційне числення.
Исследованы чистые первопорядковые логики частичных и тотальных, однозначных и неоднозначных квазиарных предикатов.
Описаны семантические модели и языки таких логик, особое внимание уделено изучению композиционных предикатных алгебр и
классов интерпретаций (семантик), отношений логического следствия для множеств формул. Для таких отношений построен ряд
исчислений секвенциального типа, характерными особенностями этих исчислений являются расширенные условия замкнутости сек-
венции и оригинальные формы элиминации кванторов.
Ключевые слова: логика, предикат, семантика, логическое следствие, секвенциальное исчисление.
Pure first-order logics of partial and total, single-valued and multi-valued quasiary predicates are investigated. For these logics we describe
semantic models and languages, giving special attention in our research to composition algebras of predicates and interpretation classes
(sematics), and logical consequence relations for sets of formulas. For the defined relations a number of sequent type calculi is constructed;
their characteristic features are extended conditions for sequent closure and original forms for quantifier elimination.
Key words: logic, predicate, semantics, logical consequence, sequent calculus.
Вступ
Розширення сфери застосування інформаційних технологій виводить на перший план задачу створення
надійних і ефективних програмних систем. Успішне вирішення цієї задачі неможливе без широкого викорис-
тання понять і методів математичної логіки.
Логіка тісно пов’язана з програмуванням із самого початку його виникнення. В межах математичної ло-
гіки запропоновано перші формалізації понять алгоритму й алгоритмічно обчислюваної функції, мови програ-
мування базуються на тих чи інших уточненнях цих понять. Апарат математичної логіки (алгебра логіки) ле-
жить в основі схемотехніки комп’ютерів. Подальший розвиток інформатики й програмування та пов’язана з
цим поява нових задач і проблем характеризується залученням до їх розв’язку все нових понять і засобів мате-
матичної логіки. На даний момент розроблено багато різноманітних логічних систем, які успішно використо-
вуються в програмуванні (див., напр., [1]). Такі системи зазвичай базуються на класичній логіці предикатів. Ця
логіка добре досліджена, вона має багатий досвід застосування. На основі класичної будуються спеціальні логі-
ки, орієнтовані на вирішення тих чи інших конкретних задач. Водночас поява нових застосувань логіки в інфо-
рматиці та програмуванні висвітила принципові обмеження класичної логіки предикатів, які ускладнюють її
використання. Така логіка базується на традиційних математичних структурах однозначних тотальних скінчен-
но-арних відображень, а для програмування характерне використання часткових відображень над складними
даними, які можуть бути неоднозначними. Тому особливої актуальності набуває проблема побудови нових,
програмно-орієнтованих логік. Таку побудову доцільно проводити на базі спільного для логіки і програмування
композиційно-номінативного підходу. На основі цього підходу розроблено низку логічних формалізмів, що
знаходяться на різних рівнях абстрактності й загальності (див., напр., [2–6]). Композиційно-номінативні логіки
базуються на класах квазіарних відображень – часткових відображень, заданих на довільних наборах іменова-
них значень.
Метою даної роботи є дослідження семантичних і синтаксичних аспектів чистих першопорядкових ком-
позиційно-номінативних логік (ЧКНЛ). Розглянуто класи ЧКНЛ часткових і тотальних, однозначних і неодноз-
начних квазіарних предикатів. Описано семантичні властивості ЧКНЛ, особливу увагу приділено вивченню
композиційних предикатних алгебр та класів інтерпретацій (семантик), відношень логічного наслідку для мно-
жин формул. Для таких відношень побудовано низку числень секвенційного типу. Характерна особливість цих
числень – розширені умови замкненості секвенції та оригінальні форми елімінації кванторів.
Поняття, які тут не визначаються, тлумачимо в сенсі [2, 3]. Нагадаємо основні визначення та позначення.
Нехай V і A – довільні множини, трактуємо їх як множину предметних імен (змінних) і множину предме-
тних значень. V-A-іменна множина (V-A-ІМ) – це часткова однозначна функція d : V A. V-A-ІМ зазвичай пода-
ємо у вигляді [ 1v a1,..., nv an, ...], де vіV, aіA, vі vj при і j. Клас всіх V-A-ІМ позначаємо VA.
Вводимо функцію asn : VA 2V таким чином: asn(d) = {vV | v ad для деякого aA}.
Для V-A-ІМ вводимо операцію ║–х видалення компоненти з іменем х та операцію накладки:
d║–х = [v ad | v х]; = [v a | vasn()].
Теоретичні та методологічні основи програмування
74
Параметричну операцію реномінації :r
,...,
,...,
1
1
n
n
vv
xx
VА
VA задаємо так: )(r
,...,
,...,
1
1
dn
n
vv
xx
d [ 1v d(x1),...,
nv (xn)]. Якщо параметри реномінації відсутні, маємо тотожну реномінацію r, вона діє як тотожне відобра-
ження: r(d) = d.
В подальшому викладі використаємо скорочення y для y1,..., yn . Замість n
n
vv
xx
,...,
,...,
1
1
r тоді можна писати v
x r .
Послідовне застосування двох операцій v
x r (зовнішня) та
u
y r (внутрішня) можна подати [3, 7] у вигляді
однієї, яку назвемо згорткою операцій v
x r та
u
y r і будемо позначати v
x r u
y . Тоді маємо )(r)(r(r dd u
y
v
x
u
y
v
x .
1. Квазіарні предикати
Під V-A-квазіарним предикатом будемо розуміти часткову неоднозначну, взагалі кажучи, функцію ви-
гляду P : VA {T, F}. Тут {T, F} – множина істиннісних значень.
Ми трактуємо часткові неоднозначні квазіарні предикати як відношення між VA та {T, F}, такі предикати
названо [3] предикатами реляційного типу, назвемо їх R-предикатами. Множину значень, які предикат P може
прийняти на dVА, позначаємо P(d). Маємо P(d) {T, F}, тому P(d) може бути одним із {}, {T}, {F}, {T, F}.
Кожний предикат P : VA {T, F} задається областю істинності та областю хибності, це множини
T(P) = {dVA | TP(d)} та F(P) = {dVA | FP(d)}.
Ім’я zV неістотне для V-A-квазіарного предиката P, якщо з умови d1║–х = d2║–х випливає P(d1) = P(d2).
V-A-квазіарний предикат P:
– однозначний, якщо T(P)F(P) = ;
– тотальний, якщо T(P)F(P) =
VA;
– неспростовний (частково істинний), якщо F(P) = ;
– виконуваний, якщо T(P) ;
– тотально істинний, якщо T(P) = VА, тотально хибний, якщо F(P) = VА;
– тотожно істинний, якщо T(P) = VА та F(P) = , тотожно хибний, якщо T(P) = та F(P) = VА;
– всюди невизначений, якщо T(P) = та F(P) = ;
– тотально насичений (повне бінарне відношення), якщо T(P) = VА та F(P) = VА.
Кожний неспростовний та кожний невиконуваний предикат є однозначними.
Часткові однозначні V-A-квазіарні предикати назвемо P-предикатами, тотальні – T-предикатами, тотальні
однозначні – TS-предикатами. Класи таких предикатів відповідно позначаємо V
APrR , V
APrP , V
APrT , V
APrTS .
Всюди невизначений V-A-квазіарний предикат позначаємо як V
A , тотожно істинний – як V
AT , тотожно
хибний – як V
AF , тотально насичений – як V
A . Якщо V і А маються на увазі, ці предикати позначаємо , T, F, .
Предикат P : VА{T, F} монотонний, якщо з d d' випливає P(d) P(d').
Предикат P : VА {T, F} антитонний, якщо з d d' випливає P(d) P(d').
Константні предикати , T, F, є монотонними й антитонними.
Для однозначних предикатів монотонність стає еквітонністю.
Однозначний предикат P : VА {T, F} еквітонний, якщо з умови P(d) та d d' випливає P(d') = P(d).
Монотонні R-предикати, антитонні R-предикати, еквітонні P-предикати, антитоннi T-предикати будемо
називати RM-предикатами, RА-предикатами, PE-предикатами, TА-предикатами. Класи V-A-квазіарних
RM-предикатів, RА-предикатів, PE-предикатів, TА-предикатів позначимо відповідно V
A
V
A
V
A PrPEPrRAPrRM
V
APrTA .
Предикат P
~
назвемо дуальним до предиката P, якщо ( ) ( ) та ( ) ( )T P F P F P T P .
Для V-A-квазіарного предиката P, трактованого як реляція P
VА Bool, можна розглядати предикат P –
доповнення до P як до реляції. Тоді )()( PTPT та )()( PFPF . Звідси )()
~
( );()
~
( PTPFPFPT .
Прикладом пари взаємно дуальних та взаємно доповнених предикатів є та .
Твердження 1. Q монотонний Q та Q
~
антитонні; Q антитонний Q та Q
~
монотонні.
Теоретичні та методологічні основи програмування
75
Твердження 2. ;
~
V
A
V
A
V
A PrTQPrTQPrPQ ;
~
V
A
V
A
V
A PrPQPrPQPrTQ
V
A
V
A PrTSQPrTSQ ; QQPrTSQ V
A
~
.
Задамо відображення дуалізації V
A
V
A PrRPrR : наступним чином: PP
~
)( для кожного V
APrRP .
Відображення дуалізації інволютивне: PP ))(( для кожного V
APrRP .
Твердження 3. (T) = T, (F) = F, () = , () = , )( V
APrP = ,V
APrT )( V
APrT = ,V
APrP )( V
APrTS =
= ,V
APrTS )( V
APrPE = ,V
APrTA )( V
APrTA = ,V
APrTA )( V
APrRM = ,V
APrRA )( V
APrRM = V
APrRA .
2. Композиційні алгебри квазіарних предикатів
Опишемо композиції квазіарних предикатів.
На пропозиційному рівні композиції працюють лише з виробленими предикатами істиннісними значен-
нями, їх називають логiчними зв’язками. Основними є 1-арна композиція заперечення та 2-арні композиції
диз’юнкція , кон’юнк ція &, імплікація , еквіваленція . Предикати (P), (P, Q), (P, Q), &(P, Q), (P, Q)
далі традиційно позначаємо P, PQ, PQ, P&Q, PQ. Як базові пропозиційні композиції візьмемо та .
Предикати P та PQ задамо через області істинності й хибності відповідних предикатів:
T(P) = F(P); F(P) = T(P);
T(PQ) = T(P)T(Q); F(PQ) = (P)F(Q).
Композиції , &, є похідними, вони виражаються через та :
PQ = PQ; P&Q = (P Q); PQ = (PQ)&(QP).
Твердження 4. Маємо та P P P P .
Твердження 5. Для предикатів ,, T, F маємо:
1) = , = ; = , = ;
2) T = F, F = T, T T = T, T F = F T = T, F F = F;
3) T = T = T, F = F = ; T = T = , F = F = ; = = T.
На рівні ЧКНЛ до логiчних зв’язок додаємо композиції реномінації та квантифікації.
Параметричну композицію реномінації v
xR : PrА PrА задамо так: ))(r())((R dPdP v
x
v
x для кожного
dVА.
Композиція R з відсутніми параметрами – тотожна реномінація, – діє як тотожне відображення: R(P) = P.
Параметричну композицію квантифікації x: PrА PrА візьмемо як базову; задамо її через області іс-
тинності та хибності відповідного предиката xP:
T(xP) = {dVA | d x a T(Р) для деякого aA};
F(xP) = {dVA | d x a F(Р) для всіх aA}.
Композиція х є похідною, вона задається такою умовою: хР = хР.
Композиції , , ,R v
x x назвемо базовими композиціями ЧКНЛ.
Твердження 6. 1) Для предикатів та маємо: ;)( ,)(R xv
x )( ,)(R xv
x ;
2) для предикатів T та F маємо: R (T) T, (T) T; R (F) F, (F) Fv v
x xx x .
Теорема 1. Композиції , , ,R v
x
x зберігають:
1) однозначність та тотальність квазіарних предикатів;
2) монотонність та антитонність квазіарних предикатів.
Теоретичні та методологічні основи програмування
76
Наслідок 1. 1) Mножини {}, {}, {T, F}, {, , T, F} замкнені відносно , , , &, , ,R v
x x, x;
2) класи P-предикатів, T-предикатів, TS-предикатів замкнені відносно , , , &, , ,R v
x x, x;
3) класи монотонних, антитонних, еквітонних предикатів замкнені відносно , , , &, , ,R v
x x, x.
Композиційну алгебру ),( CQPrRQR V
A
V
A , де CQ = {, , ,R v
x x}, назвемо чистою першопорядковою
алгеброю квазіарних предикатів.
Необхідна умова, щоб певний клас квазіарних предикатів утворив алгебру – його замкненість щодо опе-
рацій алгебри, у нашому випадку – щодо , , ,R v
x x. Те, що є підалгеброю алгебри , позначатимемо .
Таким чином, можна виділити низку підалгебр алгебри V
AQR :
),( CQPrPQP V
A
V
A – алгебра P-предикатів;
),( CQPrTQT V
A
V
A – алгебра T-предикатів;
),( CQPrTSQTS V
A
V
A – алгебра TS-предикатів; маємо V
A
V
A QPQTS та V
A
V
A QTQTS ;
),( CQPrRMQRM V
A
V
A – алгебра монотонних R-предикатів;
),( CQPrRAQRA V
A
V
A – алгебра антитонних R-предикатів;
),( CQPrPEQPE V
A
V
A – алгебра еквітонних P-предикатів; маємо V
A
V
A QPQPE та V
A
V
A QRMQPE ;
),( CQPrTAQTA V
A
V
A – алгебра антитонних T-предикатів; маємо V
A
V
A QTQTA та V
A
V
A QRAQTA ;
сингулярні алгебри V-A = )},({ CQV
A та V-A = );},({ CQV
A для них маємо V-A
V
AQPE та V-A ;V
AQTA
алгебра BV-A = );},F,T({ CQV
A
V
A маємо BV-A ,V
AQTS BV-A ,V
AQPE BV-A ;V
AQTA
алгебра BLV-A = );},F,T,,({ CQV
A
V
A
V
A
V
A тоді BLV-A ,V
AQRM BLV-A ,V
AQRA а також V-A,V-A, BV-A BLV-A .
Нехай – відображення дуалізації. Алгебри ),Pr( 1 CQ і ),Pr( 2 CQ дуальні, якщо (Pr1) = Pr2 та (Pr2) = Pr1.
Отже, маємо пари дуальних алгебр V
AQP та ,V
AQT V
AQPE та ,V
AQTA V
AQRM та ,V
AQRA V-A та V-A .
Алгебри ,V
AQR ,V
AQTS BV-A , BLV-A автодуальні.
Властивості квазіарних предикатів та їх композицій описано в [2–6]. Властивості пропозиційних компо-
зицій в цілому аналогічні властивостям відповідних класичних логічних зв’язок, те саме стосується більшості вла-
стивостей кванторів. Водночас [3, 4] для квазіарних предикатів вже невірні деякі пов’язані з кванторами закони
класичної логіки. В цій роботі обмежимось розглядом властивостей, пов’язаних з реномінаціями та кванторами.
Розглянемо основні властивості композицій реномінації (див. також [3, 6]).
R) PP )(R – тотожна реномінація.
RI) )(R)(R ,
, PP v
x
vz
xz – згортка пари тотожних імен.
RU) Нехай zV неістотне для предиката P. Тоді )(R)(R ,
, PP v
x
vz
xy .
Згортку
w
y
v
x R композицій v
xR і
w
yR задаємо так: ))(r())((R)))((R(R dPdPdP v
x
w
y
w
y
v
x
w
y
v
x . Звідси:
RR) )(R))(R(R PP w
y
v
x
w
y
v
x .
Опишемо взаємодію реномінацій та логічних зв’язок і кванторів.
Ren) )(R PzyP y
z за умови z неістотне для P – перейменування кванторного імені.
R) )(R)(R PP v
x
v
x – R-дистрибутивність.
Теоретичні та методологічні основи програмування
77
R) )(R)(R)(R QPQP v
x
v
x
v
x – R-дистрибутивність.
Rs) ),(R)(R PyyP v
x
v
x якщо },{ xvy – проста (обмежена) R-дистрибутивність.
R) ),(R)(R PzyP y
z
v
x
v
x якщо z неістотне для P та },{ xvz – R-дистрибутивність.
Для опису властивостей елімінації кванторів використaємо спеціальні 0-арні композиції – параметризова-
ні за предметними іменами предикати-індикатори Ez, які визначають наявність в даних компоненти з відповід-
ним zV. Подібні предикати-індикатори z, пов’язані з Ez (маємо Ez = z), використані в низці робіт [4–9].
Предикати Ez задаємо так: T(Ez) = {d | d(z)} = {dVA | zasn(d)}; F(Ez) = {d | d(z)} = {dVA | zasn(d)}.
Предикати Ez не є монотонними і не є антитонними. Кожне xV таке, що x z, неістотне для Ez.
Теорема 2. Для R-предикатів справджуються наступні співвідношення:
))(R( ,
, PT xu
yv T(Ey) ))(R( xPT u
v ; зокрема, ))(R( PT x
y T(Ey) T(xР);
))(R( xPF u
v T(Ey) ))(R( ,
, PF xu
yv ; зокрема, F(xР) T(Ey) ));(R( PF x
y
))(R( ,
, PT xu
yv F(Ey) ))(R( xPT u
v ; зокрема, ))(R( PT x
y F(Ey) T(xР);
))(R( xPF u
v F(Ey) ))(R( ,
, PF xu
yv ; зокрема, F(xР) F(Ey) ))(R( PF x
y .
3. Мови та семантичні моделі ЧКНЛ
Семантичними моделями ЧКНЛ є [2, 3] чисті першопорядкові композиційні системи квазіарних предика-
тів. Вони мають вигляд (VA, Pr, CQ). Композиційна система (VA, Pr, CQ) задає алгебру даних (A, Pr) та компози
ційну алгебру предикатів (Pr, CQ). Терми композиційної алгебри трактуємо як формули мови ЧКНЛ.
Алфавiт мови ЧКНЛ: множина V предметних імен (змінних), в якій виділена множина U V тотально не-
істотних [3] імен; множина Ps предикатних символів; множина },,,{ xRCs v
x символів базових композицій.
Множину Ps називають сигнатурою мови; четвірку = (V, U, Cs, Ps) назвемо розширеною сигнатурою мови.
Дамо індуктивне визначення множини Fr формул:
FA) Ps Fr; формули pPs назвемо атомарними;
FС) , Fr , , ,v
xR xFr.
Для зручності далі використовуємо скоро чення формул (див. [2, 3]), користуючись символами похід-
них композицій, дужками "(", ")" та інфіксною формою запису. Наприклад, – скорочення формули
.
Позначимо nm() множину тих xV, які фігурують у символах реномінації та квантифікації формули .
Інтерпретуємо мову на композицій них системах (VA, Pr, CQ). Iмена xV позначають елементи множи-
ни базових даних A, символи композицій – композиції із CQ. Символи Рs позначають базові предикати в
множині Pr, для опису цього позначення задамо тотальне однозначне відображення I : Ps Pr. Із базових
предикатів за допомогою композицій будуємо складніші, які позначаються формулами. Відображення інтер-
претації формул I : Fr Pr задамо як розширення I : Ps Pr згідно побудови формул із простіших за допо-
могою символів Cs:
IF) I() = (I()), I() = (I(), I()), ));((R))(( IRI v
x
v
x I(x) = x(I()).
Трійку J = (CS, , I) назвемо інтерпретацією мови ЧКНЛ сигнатури . Iнтерпретації будемо скорочено
позначати (A, I). Предикат J() – значення формули при інтерпретації J – позначимо J.
Ім’я xV неістотне для формули , якщо для кожної інтерпретації J ім’я x неістотне для предиката J.
Визначимо для формул множини гарантовано неістотних імен за допомогою відображення : Fr2V так.
Для рPs візьмемо (р) = U, а далі [2] для кожної Fr задаємо: () = (); () = ()();
)(
,...,
,...,
1
1
n
n
vv
xx
R ((){v1,...,vn}) \ {xi | vi(), 1,i n }, (x) = (){x}. Кожне u() неістотне [2] для .
Для Fr задаємо
)()( . Задамо множину “нових” для неістотних імен: fu() = U \ nm().
Теоретичні та методологічні основи програмування
78
Виділення підалгебр квазіарних предикатів виділяє відповідні класи інтерпретацій. Можна говорити
про загальний клас R-інтерпретацій та підкласи P-інтерпретацій, T-інтерпретацій, TS-інтерпретацій, а також
PE-інтерпретацій, TA-інтерпретацій, RM-інтерпретацій, RA-інтерпретацій. Такі класи інтерпретацій назива-
ють семан тиками, будемо їх відповідно позначати R, P, T, TS, PE, TA, RM, RA.
Логіки -предикатів будемо називати логіками з -семантикою; тут – одне з R, P, T, TS, PE, TA, RM, RA.
Семантики P, T, R в [3] названо неокласичною, пересиченою, загальною.
Для зазначених семантик маємо такі співвідношення:
Теорема 3. TS P R, TS T R, PE RM R, TA RA R, PE P, TA T .
Відображення дуалізації продовжимо на класи інтерпретацій.
Інтерпретацію (J) = (A, I) назвемо дуальною до інтерпретації J = (A, I), якщо для кожного pPs маємо
)()( )( JJ pFpT та )()( )( JJ pTpF . Тоді J дуальна до (J): )()( )(JJ pFpT та )()( )(JJ pTpF .
Теорема 4. Інтерпретації J та дуальні для всіх Fr маємо )()( FT J та ( ) ( )JF T .
Якщо J та G дуальні, то: J монотонний G антитонний; G антитонний J монотонний.
Виділення дуальних пар предикатних алгебр індукує виділення дуальних семантик.
Твердження 7. Маємо такі дуальні пари: P та T, PE та TA, RM та RA. Семантики R та TS автодуальні.
Для кожної JP можна збудувати HTS: для кожного pPs маємо T(pJ) T(pH) =
VA та F(pJ) F(pH) =
VA.
Таку H називають системою тотальних розширень для J. Згідно теореми про розширення [2] для кожної Fr
тоді маємо T(J) T(H) = VA та F(J) F(H) = VA.
Формула виконувана при інтерпретації J, або J-виконувана, якщо J – виконуваний предикат.
Формула виконувана в класі інтерпретацій K, якщо J-виконувана при деякій JK.
Кожна формула виконувана в T та виконувана в R (беремо інтерпретацію, задану алгеброю V-A).
Отже, поняття виконуваної формули змістовне лише для P-інтерпретацій.
Формула неспростовна при інтерпретації J, або J-неспростовна (позн. J |= ), якщо предикат J – не-
спростовний. Формула неспростовна в класі інтерпретацій K (позн. K|= ), якщо J |= для кожної JK.
Формула тотально істинна при інтерпретації J (позн. J | ), якщо J – тотально істинний предикат.
Формула тотально iстинна в класі інтерпретацій K (позн. K| ), якщо J | для кожної JK.
Формула тотожно істинна при інтерпретації J (позн. K|=id
), якщо J = T.
Формула тотожно iстинна в класі інтерпретацій K, якщо K|=id
для кожної JK.
Подібним чином даємо визначення тотально хибної при інтерпретації J та тотально хибної в K формули;
тотожно хибної при інтерпретації J та тотожно хибної в K формули.
Теорема 5. 1) { | R|= } = { | R| } = { | R|=id
} = ;
2) { | P| } = { | P|=id
} = { | T|= } = { | T|=id
} = ;
3) { | P|= } = { | T| } = { | TS|=id
} = { | TS|= } = { | TS| }.
Твердження 8. P|= невиконувана в P.
Теорема 6. P|= T| та P|= TS|=id
.
Mаємо J |= при JP |= при дуальній T. Звідси отримуємо перше твердження.
Доводимо друге твердження. Якщо TS|id , то F(J) для деякої JTS, тому P| в силу TS P.
Якщо P| , то F(J) для деякої JP. Візьмемо для J систему тотальних розширень HTS. Тоді
F(J) F(), звідки F() , тому TS|id
.
Поняття тавтології для ЧКНЛ вводимо традиційним чином. Формула пропозиційно нерозкладна, якщо
вона атомарна чи має вигляд x чи R v
x . Нехай Fr0 – множина пропозиційно нерозкладних формул. Істиннiс-
на оцiнка мови – це тотальне відображення : Fr0 {T, F}. Продовжимо до відображення : Fr {T, F} згідно
дії та на предикати (див. [2]). Формула тавтологiя, якщо () = T для кожної істиннісної оцінки .
Твердження 9. тавтологія TS|=id .
Теоретичні та методологічні основи програмування
79
Нехай утворена із пропозиційно нерозкладних формул 1, …, n. Нехай TS|id , тоді (d) = F для
деяких J = (A, I) TS та dVA. Візьмемо істиннiсну оцiнку : (i) = iJ(d). Тоді () = F, тому не тавтологія.
Наслідок 2. Пропозиційна формула є тавтологія TS|=id
P|= T| .
4. Відношення логічного наслідку та логічної еквівалентності
На множині формул можна ввести низку відношень, які формалізують фундаментальне поняття логічно-
го наслідку. Спочатку вводимо відношення наслідку для двох формул при фіксованій інтерпретації J.
1) Істиннісний, або T-наслідок J|=T : J|=T T(J) T(J).
2) Хибнісний, або F-наслідок J|=F : J|=F F(J) F(J).
3) Cильний, або TF-наслідок J|=TF : J|=TF T(J) T(J) та F(J) F(J).
4) Неспростовнісний, або IR-наслідок J|=IR : J|=IR T(J)F(J) = .
5) Дуальний до IR, або DI-наслідок J|=DI : J|=DI F(J)T(J) = VA.
Відповідні відношення логічного наслідку в семантиці визначаємо за схемою:
|= , якщо J|= для кожної J.
Зазначені відношення описано в [3–6]. Окрім цих відношень, в [10] досліджено ще такі.
6) С-наслідок J|=С : J|=С T(J)F(J) F(J)T(J).
7) TF-наслідок J|=TF : J|=TF T(J) T(J) або F(J) F(J).
Вони продукують відповідні відношення логічного наслідку, нетривіальними та відмінними від інших є
P|=TF та R|=С . Проте P|=TF та R|=С нетранзитивні, для них невірні деякі властивості декомпозиції формул (про це
нижче). С-наслідок для пропозиційної логіки розглядався в [11], проте із певними неточностями (див. [10]).
Безпосередньо із визначень отримуємо, що усі визначені вище відношення рефлексивні.
Також маємо: J|=IR J|=С, J|=DI J|=С; J|=TF J|=T J|=TF, J|=TF J|=F J|=TF .
Теорема 7. Нехай інтерпретації A та B дуальні. Тоді маємо:
1) A|=T B|=F та A|=F B|=T ;
2) A|=IR B|=DI та A|=DI B |=IR ;
3) A|=TF B|=TF ;
4) A|=С B|=С ; A|=TF B|=TF .
Зауважимо, що пп. 1–3 теореми доведено в [3], п.4 доведено в [10].
Відношення С-наслідку та TF-наслідку пов’язані таким чином (див. [10]):
Теорема 8. Маємо J|=C , J|=TF , .
Звідси як наслідок отримуємо:
R|=C ,
R|=TF , .
У випадках класичної логіки та логіки TS-предикатів усі наведені відношення логічного наслідку втрача-
ють відмінності, вони збігаються і стають єдиним відношенням, яке позначимо TS|= . Отже:
Твердження 10. TS|=TF = TS|=T = TS|=F = TS|=IR = TS|=DI = TS|=C = TS|=TF = TS|=.
Для запропонованих відношень маємо такі властивості (доведення див. [3, 10]):
Теорема 9. 1) P|=DI = T|=IR = R|=IR = R|=DI = ;
2) P|=T = T|=F ; P|=F = T|=T ; P|=IR = T|=DI; P|=TF = T|=TF; P|=TF = T|=TF; R|=T = R|=F = R|=TF;
3) P|=IR = T|=DI = P|=С = T|=С = TS|= .
Таким чином, із перелічених вище відношень не більше 7 різних. Виділимо ці відношення:
P|=IR, P|=TF, P|=T, P|=F, P|=TF, R|=С, R|=TF.
Розглянемо питання, пов’язані з транзитивністю розглянутих відношень.
Твердження 11. Відношення J|=T, J|=F, J|=TF та відношення P|=T, P|=F, P|=TF, R|=TF є транзитивними.
Відношення наслідку A|=IR нетранзитивне. Справді, маємо
Теоретичні та методологічні основи програмування
80
Приклад 1. Нехай AP, p, q, sPs. Задамо pA як T, qA як , sA як F. Тоді p A|=IR q, q A|=IR s, проте p A|IR s.
Водночас для відношення логічного наслідку P|=IR ситуація нормалізується (див. [3, 10]):
Теорема 10. Відношення P|=IR транзитивне.
Приклад 2. Нехай p, qPs, – це формула p (qq), – це p (qq). Тоді
P|=TF p та p
P|=TF .
Водночас p
P|=TF та
P|=TF p, тому p
P|=TF та
P|=TF p. Проте [10]
P|T та
P|F , тому
P|TF .
Приклад 3. Нехай p, qPs, – це формула p (qq), – це формула p (qq). Тоді маємо
R|=C p та
p
R|=C . Водночас p
R|=TF та
R|=TF p, тому p
R|=С та
R|=С p. Проте [10]
R|C .
Таким чином, відношення P|=TF нетранзитивне та відношення R|=C нетранзитивне. Отже, ці відношення
не задовольняють постулату Тарського про транзитивність логічного наслідку.
Із пропозиційного рівня успадковується [2, 3] відношення |=t тавтологічного наслідку.
|=t , якщо – тавтологія. Таке |=t рефлексивне і транзитивне.
Теорема 11. 1) Для класичної семантики пропозиційної логіки усі розглянуті відношення збігаються;
2) Для пропозиційних формул маємо:
P|=IR
T|=DI
P|=C
T|=C
TS|= |=t ;
Між розглянутими відношеннями логічного наслідку отримано такі співвідношення (див. [3, 4, 10]):
Теорема 12. 1) P|=TF
P|=T
P|=TF, P|=TF
P|=F
P|=TF, P|=TF
P|=IR ; R|=TF
P|=TF, R|=TF
R|=С
P|=IR ;
2) P|=T
P|=F, P|=F
P|=T, P|=TF
R|=С, R|=С
P|=TF ;
3) |=t
P|=IR ; P|=TF |=t , R|=C |=t .
Відношення логічного наслідку індукують відповідні відношення логічної еквівалентності.
Відношення еквівалентності при інтерпретації J задаємо [3] за схемою: J , якщо J|= та J|= .
Для відношення JTF маємо: JTF T(J) = T(J) та F(J) = F(J). Отже, JTF J = J.
Відношення JT, JF, JTF, JTF транзитивні, проте JIR нетранзитивне (див. приклад 1).
Відношення логічної еквівалентності PIR, PT, PF, PTF, RTF, а також PTF, RС, визначаємо за схемою:
, якщо
|= та |= .
Подібним чином визначаємо відношення тавтологічної еквівалентності t : t , якщо |=t та |=t .
Твердження 12.
J для кожної J.
Відношення PIR, PT, PF, PTF, RTF, t рефлексивні, транзитивні та симетричні.
Теорема 13 (див. [10]). Відношення JTF, JС та PTF, RС нетранзитивні.
Таким чином, PTF та RС насправді не є відношеннями еквiвалентності.
Властивості відношень логічного наслідку та логічної еквівалентності досліджено, зокрема, в [3–6, 10].
Основою еквівалентних перетворень формул є [2, 3] теорема еквівалентності. Вона формулюється для ві-
дношень RTF, PTF, PIR . Для PT та PF теорема невірна, а PTF та RС не є відношеннями еквiвалентності.
Теорема 14. Нехай ' отримано з формули заміною деяких входжень 1, ..., n на 1, ..., n. Якщо
1
1, ..., n
n, то
'.
Властивості квазіарних предикатів індукують відповідні семантичні властивості формул (див. [3–6]).
Наведемо основні властивості, пов’язані з реномінаціями та кванторами (тут – це RTF чи PTF).
R) ( )R ;
RI) )()(,
, v
x
vz
xz RR .
RU) )()(,
, v
x
vz
xy RR за умови z().
RR) )())(( w
y
v
x
w
y
v
x RRR .
R) )()( v
x
v
x RR .
R) )()()( v
x
v
x
v
x RRR .
Теоретичні та методологічні основи програмування
81
Rs) )()( v
u
v
u xRxR за умови { , }x v u – проста (обмежена) R-дистрибутивність.
R) )()( y
z
v
x
v
x zRyR за умови ))(( xRfuz v
x .
5. Відношення логічного наслідку для множин формул
Відношення логічного наслідку поширимо на пари множин формул. Спочатку задамо відношення нас-
лідку між двома множинами формул при фіксованій інтерпретації J. Нехай Fr, Fr. Введемо позначення
)( JT як T(J),
)( JF як FJ),
)( JT як T(J),
)( JF як F(J).
є T-наслідком при J (позн. J|=T ), якщо T(J) T
(J).
є F-наслідком при J (позн. J|=F ), якщо F(J) F
(J).
є TF-наслідком при J (позн. J|=TF ), якщо T(J) T
(J) та F(J) F
(J).
є IR-наслідком при J (позн. J|=ID ), якщо T(J) F
(J) = .
є DI-наслідком при J (позн. J|=DI ), якщо F(J) T
(J) =
VA.
є С-наслідком при J (позн. J|=С ), якщо T(J) F
(J) F
(J) T
(J).
є TF-наслідком при J (позн. J|=TF ), якщо T(J) T
(J) або F(J) F
(J).
Відповідні відношення логічного наслідку для множин формул в семантиці визначаємо за схемою:
|= , якщо J|= для кожної J.
Наведемо характерні властивості відношень логічного наслідку для множин формул.
Теорема 15 Нехай інтерпретації J та дуальні. Тоді:
1) J|=IR |=DI та J|=DI |=IR ;
2) J|=T |=F та J|=F |=T ;
3) J|=TF |=TF ;
4) J|=С |=С ; J|=TF |=TF ;
Із наведених відношень логічного наслідку для множин формул лише 7 різних. Виділимо ці відношення:
P|=IR, P|=TF, P|=T, P|=F, P|=TF, R|=С, R|=TF .
Відношення наслідку та логічного наслідку для множин формул рефлексивні й нетранзитивні [2, 3].
Розглянемо відношення логічного наслідку, коли одна з множин формул порожня. Такі властивості вивча-
лись в [10]. Зауважимо, що J|= означає T J|= , J|= означає J|= F.
Теорема 16.
P|=C
P|=IR
P|=F
T|=C
T|=DI
T|=T P|= T| ;
P|=C
P|=IR
P|=F
T|=C
T|=DI
T|=T P|= T| .
Розглянемо можливість перенесення формули з лівої частини логічного наслідку в праву і навпаки.
Теорема 17. 1)
P|=IR , ,
P|=IR та
P|=IR , ,
P|=IR ;
2)
R|=С , ,
R|=С та
R|=С , ,
R|=С ;
Теорема 18. Можливі такі ситуації: 1) ,
P|=T та
P|T , ; ,
P|=T та
P|T , ;
2)
P|=F , та ,
P|F ;
P|=F , та ,
P|F ;
3) ,
P|=TF та
P|TF , ;
P|=TF , та ,
P|TF ;
4) ,
R|=TF та
R|TF , ;
R|=TF , та ,
R|TF ;
5) ,
P|=TF та
P|TF , ;
P|=TF , та ,
P|TF .
Отже, для P|=IR та R|=С можна робити перенесення формули з лівої частини логічного наслідку в праву і
навпаки; для P|=T, P|=F, P|=TF, P|=TF, R|=TF – не можна.
Теоретичні та методологічні основи програмування
82
Теорема 19. 1) , ,
P|=T ,
P|=F , , , , ,
P|=TF , , ;
2) , ,
P|F ;
P|T , , ; , ,
R|TF , , .
У випадку відношень для множин формул R|=С зводиться до R|=TF (тут позначення для { | }).
Теорема 20. Маємо
R|=С ,
R|=TF , .
Аналогом теореми еквівалентності для множин формул є теорема заміни еквівалентних.
Теорема 21. Нехай
, тоді маємо: ,
|= ,
|= ;
|= ,
|=|= , .
Тут та |= – це відповідно RTF, PTF, PIR та R|=TF, P|=TF, P|=IR .
Розглянемо властивості відношень логічного наслідку для множин формул на пропозиційному рівні.
Маємо [3–6] такі властивості декомпозиції формул (тут |= – одне з відношень P|=IR, P|=T, P|=F, P|=TF, R|=TF):
L) , |= , |= .
R) |= , |= , .
L) , |= , |= та , |= .
R) |= , |= , , .
L) (), |= , , |= .
R) |= , () |= , та |= , .
Згідно теореми 17, для P|=IR та R|=С додатково справджуються:
L) ,
P|=IR
P|=IR , .
R)
P|=IR , ,
P|=IR .
Згідно теореми 18, для P|=T, P|=F, P|=TF R|=TF та P|=TF ці властивості невірні.
Не всі властивості декомпозиції формул вірні для P|=TF та R|=С (відповідні приклади див. у [10]):
Теорема 22. Для відношень P|=TF та R|=С властивості L та R є невірними
Таким чином, для відношень P|=TF та R|=С, на додаток до їх нетранзитивності, вже невірні деякі властиво-
сті декомпозиції формул. Це не дає змоги безпосередньо будувати cеквенційні числення для цих відношень.
Водночас для відношення R|=С ситуація не настільки погана, адже за теоремою 20 R|=С зводиться до R|=TF . Тому
перевірка наявності
R|=С зводиться до перевірки наявності ,
R|=TF , .
Для всіх зазначених відношень маємо монотонність: якщо та , то |= |= .
Розглянемо властивості, які гарантують наявність логічного наслідку. Для кожного з відношень маємо:
С) , |= , .
Додатково гарантують наявність відповідного відношення логічного наслідку такі властивості
СL) , ,
P|=T ;
СR)
P|=F , , ;
СLR) , ,
P|=TF , , .
B силу L та R явне виділення таких властивостей зайве для відношень P|=IR та R|=С .
Наведемо властивості, пов'язані з реномінацією та кванторами. Вони отримуються на основі наведених ви-
ще властивостей R, RI, RU, RR, R, R, Rs, R. Кожна така властивість R продукує 4 відповідні властивості
RL, RR, RL, RR для відношення логічного наслідку, коли виділена формула чи її заперечення знаходиться
у лівій чи правій частині цього відношення. Наведемо для прикладу властивості, індуковані Rs та R.
RsL) ( ),v
xR y |= ( ),v
xyR |= за умови у{ ,v x }.
RsR) |= , ( )v
xR y |= , ( )v
xyR за умови у{ ,v x }.
RsL) ( ),v
xR y |= ( ),v
xyR |= за умови у{ ,v x }.
RsR) |= , ( )v
xR y |= , ( )v
xyR за умови у{ ,v x }.
Теоретичні та методологічні основи програмування
83
RL) ( ),v
xR y |= ( ),v y
x zzR |= за умови ( ( ))v
xz fu R x .
RR) |= , ( )v
xR y |= , ( )v y
x zzR за умови ( ( ))v
xz fu R x .
RL) ( ),v
xR y |= ( ),v y
x zzR |= за умови ( ( ))v
xz fu R x .
RR) |= , ( )v
xR y |= , ( )v y
x zzR за умови ( ( ))v
xz fu R x .
Наведемо властивості елімінації кванторів. Такі властивості базуються на теоремі 2.
L) х, |= ( ), ,x
zR Ez |= за умови zfu(, , х)).
R) |= х, , Ez |= ( ),x
zR за умови zfu(, , х)).
vR) , Ey |= х, , Ey |= , ( ),x
yx R .
vL) х, Ey, |= , ( ), ,x
yx R Ey |= .
Для |=IR в силу L та R властивості вигляду із запереченням виділеної формули є похідними.
Bластивості E-розподілу та первісного означення:
Ed) |= Ey, |= та |= , Ey.
Ev) |= Ez, |= за умови zfu(, ).
6. Секвенційні числення ЧКНЛ
Секвенційні числення формалізують відношення логічного наслідку для множин формул. Як і в роботах
[2, 8, 9], секвенційні числення будуємо в стилі семантичних таблиць. Ми трактуємо секвенції як множини фор-
мул, специфікованих (відмічених) символами |– та –| . Позначаємо секвенції як |––|, скорочено як . Формули із
називаємо T-формулами, а формули із – F-формулами. Це відповідає семантичному трактуванню формул із
як істинних, а формул із – як хибних. Секвенційні числення будуємо так: секвенція |––| вивідна |= .
В цій роботі не розглядаємо секвенційні числення логік еквітонних і антитонних предикатів, такі чис-
лення описано в [2, 8]. Ми пропонуємо секвенційні числення ЧКНЛ для відношень P|=IR, P|=T, P|=F, P|=TF, R|=TF .
Характерна їх особливість – розширені умови замкненості секвенції та оригінальні форми елімінації кванторів.
Для відношення R|=С секвенційне числення будується опосередковано, враховуючи теорему 20. Тоді:
R|=С секвенція |–
, |–, –|, –|
вивідна в численні для R|=TF .
Виведення в секвенційних численнях має вигляд дерева, вершинами якого є секвенції.
Секвенція вивідна (має виведення), якщо існує замкнене секвенційне дерево з коренем . Таке дерево
називають виведенням секвенції . Секвенційне дерево замкнене, якщо кожний його лист – замкнена секвенція.
Замкнені секвенції є аксіомами секвенційного числення. Правилами виведення секвенційних числень є
секвенційні форми, вони є синтаксичними аналогами властивостей відношень логічного наслідку.
Замкненість секвенції |––| означає, що |= . Тому умови, які гарантують наявність логічного наслідку,
індукують відповідні умови замкненості секвенції. Для опису таких умов введемо наступні визначення.
Для множини специфікованих формул (секвенції) |––| задамо множини означених та неозначених пред-
метних імен, або множини val-змінних та unv-змінних: val(|––|) = {xV | Ex}; unv(|––|) = {xV | Ex}.
Множину нерозподілених для |––| імен введемо так: ud(|––|) = nm() \ (val(|––|) unv(|––|)).
Формули вигляду ( )x
yR назвемо R-формулами. Rs-формою R-формули ),(,,
,, vux
zyxR де { } ( )u , на-
звемо R-формулу ( )v
zR , утворену із )(,,
,, vux
zyxR всеможливими спрощенням зовнішньої реномінації на основі
вла стивостей R, RI, RU (застосування R дає Rs-форму , яка може не бути R-формулою). Властивості R, RI, RU
гарантують: якщо та мають однакові Rs-форми, то T(J) = T(J) та F(J) = F(J) для всіх інтерпретацій J.
Нехай Un V – множина імен, трактованих як неозначені, а символ V позначає відсутність значення.
Нехай R-формула uxr
vysR ,,
,, така: { , , } , { , }r s y Un x v Un . Un-форма формули uxr
vysR ,,
,, – це вираз ux
vR ,
, .
Для формули , яка не є R-формулою, її Un-форма збігається із .
R-формули та назвемо Rs-Un-еквівалентними, якщо та мають однакові Rs-форми або ці Rs-
форми мають однакові Un-форми. Кожна R-формула Rs-Un-еквівалентна сама собій (рефлексивність).
Якщо R-формули та Rs-Un-еквівалентні, то та теж назвемо Rs-Un-еквівалентними.
Теоретичні та методологічні основи програмування
84
Твердження 13. Якщо формули та Rs-Un-еквівалентні, то для кожнoї інтерпретації J маємо:
T(J) V\UnA = T(J) V\UnA та F(J) V\UnA = F(J) V\UnA.
Це означає: J (d) = J (d) для кожних J та dVA, для яких asn(d)Un = , тобто Eu(d) = F для всіх uUn.
Тепер опишемо умови, які гарантують наявність того чи іншого логічного наслідку. Ці умови індуковані
властивостями С, СL, СR, СLR, вони опираються на твердження 13. Нехай Fr, Fr, Un = {x | Ex}.
Теорема 23. 1) Нехай формули та – Rs-Un-еквівалентні, тоді , |= , ; зокрема, , |= ,
(тут |= – одне з P|=IR, P|=T, P|=F, P|=TF, R|=TF );
2) нехай формули та – Rs-Un-еквівалентні, тоді , ,
P|=T ; зокрема, , ,
P|=T ;
3) нехай формули та – Rs-Un-еквівалентні, тоді
P|=F , , ; зокрема,
P|=F , , ;
4) нехай формули , – Rs-Un-еквівалентні та , – Rs-Un-еквівалентні, тоді , ,
P|=TF , , ;
зокрема, , ,
P|=TF , , для довільних формул , .
Теорема 23 обґрунтовує наведені нижче умови замкненості секвенції |––| із множиною unv-змінних Un.
Базова умова замкненості індукована властивістю С:
С) існують Rs-Un-еквівалентні формули та такі: та ; зокрема, якщо існує : та .
Властивості СL, СR, СLR, які істотні для відношень P|=T, P|=F, P|=TF, індукують додаткові умови СL, СR,
СLR замкненості секвенції |––|:
СL) існують Rs-Un-еквівалентні R-формули та такі: та ;
зокрема, якщо існує формула : та ;
СR) існують Rs-Un-еквівалентні R-формули та такі: та ;
зокрема, якщо існує формула : та ;
СLR) існують Rs-Un-еквівалентні R-формули , та Rs-Un-еквівалентні R-формули , такі:
, , , ; зокрема, якщо існують формули та такі: , , , .
Зрозуміло, що СLR СL та СR.
У випадку числень для відношення P|=IR умови СL, СR, СLR зводяться до С.
Секвенційне числення задається базовими секвенційними формами і умовами замкненості секвенції.
Опишемо числення, які будемо називати базовими секвенційними численнями ЧКНЛ.
Числення QBG формалізує відношення R|=TF. Умова замкненості секвенції: C.
Числення QBLR формалізує відношення |=TF. Умова замкненості секвенції: C CLR.
Числення QBL формалізує відношення |=T. Умова замкненості секвенції: C CL.
Числення QBR формалізує відношення |=F. Умова замкненості секвенції: C CR.
Числення QBC формалізує відношення |=IR. Умова замкненості секвенції: C.
Числення QBG, QBLR, QBL, QBR мають однакові базові секвенційні форми. Опишемо ці форми.
Форми еквівалентних перетворень |–RR, –|RR, |–RR, –|RR, |–R, –|R, |–R, –|R, |–R, –|R, |–R,
–|R, |–Rs, –|Rs, |–Rs, –|Rs, |–R, –|R, |–R, –|R індукуються відповідними властивостями відношення
логічного наслідку RRL, RRR, RRL, RRR, RL, RR, RL, RR, RL, RR, RL, RR, RsL, RsR, RsL,
RsR, RL, RR, RL, RR, які в свою чергу продукуються властивостями RR, R, R, Rs, R.
Наведемо для прикладу форми |–RR, –|R, |–Rs, –|R:
|–RR
)),((
),(
|
|
w
y
v
x
w
y
v
x
RR
R
; –|R
),(
)),()((
|
|
v
x
v
x
v
x
R
RR
.
|–Rs
),(
),(
|
|
yR
yR
v
x
v
x
, де у{ ,v x }; –|R
),(
),(
|
|
yR
zR
v
x
y
z
v
x
, де ))(( xRfuz v
x ;
Форми декомпозиції індукуються відповідними властивостями L, R, L, R, L, R :
|
,
,
|
|
; |
,
,
|
|
;
Теоретичні та методологічні основи програмування
85
|
,
, ,
|
||
; |
,
, ,
|
||
;
|
),(
, ,
|
||
; |
),(
, ,
|
||
.
Форми елімінації кванторів та E-розподілу:
|
,
,),(
|
| |
x
EzR x
z
; |
,
,),(
|
| |
x
EzR x
z
;
|v
,,
),(,,
| |
| | |
Eyx
REyx x
y
; |v
,,
),(,,
| |
| ||
Eyx
REyx x
y
.
Для форм |, |R умова: zfu(, , x). Для форм |v, |v вважаємо, що Ey не входить до , .
, ,
Ed
|| ExEx
за умови: Ex не входить до , .
Окрім базових форм, при побудові секвенційного дерева можна використовувати допоміжні форми
спрощення. Такі форми |–R, –|R, |–R, –|R, |–RI, –|RI, |–RI, –|RI, |–RU, –|RU, |–RU, –|RU індукуються відпо-
відними властивостями відношення логічного наслідку RL, RR, RL, RR, RIL, RI R, RI L, RIR, RUL, RUR,
RUL, RUR, які в свою чергу продукуються властивостями RI, RU, R. Перетворення на основі форм спро-
щення фактично закладені в умови замкненості секвенції: для встановлення Rs-Un-еквівалентності формул
необхідна побудова Rs-форм для цих формул, що робиться на основі RI, RU, R. Наведемо тут для прикладу
форми |–RI та –|RU:
|–RI
),(
),(
,
,|
|
vz
xz
v
x
R
R
; –|RU
),(
),(
,
,|
|
vy
uz
v
u
R
R
, де у();
Базовими формами числення QBС є |–RR, –|RR, |–R, –|R, |–R, –|R, |–Rs, –|Rs, |–R, –|R, |, |, |, |v,
Ed, до яких додаємо | та | . Допоміжнi форми спрощення: |–R, –|R, |–RI, –|RI, |–RU, –|RU. Форми | та | такі:
|
,
,
|
|
; |
,
,
|
|
.
Властивості відношень логічного наслідку індукують основну властивість базових секвенційних форм:
Теорема 24. 1. Нехай
||
||
– базова форма; тоді: a) |= |= ; b) | | .
2. Нехай
||
||||
– базова форма; тоді: a) |= та |= |= ; b) | | або | .
Для кожного з пропонованих числень, що формалізує відповідне відношення логічного наслідку, вірні тео-
реми коректності та повноти. Для доведення повноти пропонованих секвенційних числень використовуємо ме-
тод модельних множин (подібні доведення див., напр., [8]).
Теорема 25 (коректності та повноти). |= секвенція |– –| вивідна.
Висновки
Досліджено семантичні та синтаксичні аспекти композиційно-номінативних логік. Розглянуто класи
чистих першопорядкових логік часткових і тотальних, однозначних і неоднозначних квазіарних предикатів.
Описа но семантичні моделі та мови таких логік, особливу увагу приділено вивченню композиційних преди-
катних алгебр та класів інтерпретацій (семантик). Виділено низку підалгебр першопорядкової алгебри кваз і-
арних предикатів, описано відповідні семантики. Розглянуто відношення логічного наслідку для множин фо-
рмул, досліджено їх властивості. Для таких відношень запропоновано низку числень секвенційного типу.
Характерна осо бливість цих числень – розширені умови замкненості секвенції та оригінальні форми елімі-
нації кванторів. По дібні дослідження планується продовжити для першопорядкових композиційно-
номінативних логік з рівністю.
Теоретичні та методологічні основи програмування
86
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. Нікітченко М.С. , Шкільняк С.С. Композиційно-номінативні логіки квазіарних предикатів: семантичні аспекти // Вісник Київського націо-
нального університету імені Тараса Шевченка. – Серія: фіз.-мат. науки. – 2012. – Вип. 4. – C. 165–172.
5. Нікітченко М.С. , Шкільняк О.С. , Шкільняк С.С. Першопорядкові композиційно-номінативні логіки із узагальненими реномінаціями //
Проблеми програмування. – 2014. – № 2–3. – C. 17–28.
6. Nikitchenko М., Shkilniak S. Semantic Properties of Logics of Quasiary Predicates // Workshop on Foundations of Informatics: Proceedings FOI-
2015. – Chisinau, Moldova. – P. 180–197.
7. Нікітченко М.С., Шкільняк С.С. Алгебри квазіарних та бі-квазіарних реляцій // Проблеми програмування. – 2016. – № 1. – C. 17–28.
8. Шкільняк С.С. Спектр секвенційних числень першопорядкових композиційно-номінативних логік // Проблеми програмування. – 2013,
№ 3. – C. 22–37.
9. Шкільняк С.С. Секвенційні системи логічного виведення першопорядкових логік часткових предикатів // Компьютерная математика. –
2013, Вып. 2. – C. 88–96.
10. Нікітченко М.С. , Шкільняк О.С. , Шкільняк С.С. Відношення логічного наслідку в логіках квазіарних предикатів // Проблеми програ-
мування. – 2016. – № 1. – C. 13–25.
11. Смирнова Е.Д. Логика и философия. – М.: РОССПЕН, 1996. – 304 с.
References
1. ABRAMSKY, S., GABBAY, D. and MAIBAUM, T. (editors). (1993–2000). Handbook of Logic in Computer Science Modal logic. 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. (2012). Composition-nominative logics of quasiary predicates: semantic aspects. In Bulletin of Taras
Shevchenko National University of Kyiv. Series: Physics & Mathematics. No 4. P. 165–172 (in ukr).
5. NIKITCHENKO, M., SHKILNIAK, O. and SHKILNIAK, S. (2014). First-order composi tion-nominative logics with generalized renominations. In
Problems in Progamming. № 2–3, p. 17–28 (in ukr).
6. 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.
7. NIKITCHENKO, M. and SHKILNIAK, S. (2016). Algebras of quasiary and of bi-quasiary relations. In Problems in Progamming. № 1, p. 3–12 (in ukr).
8. SHKILNIAK, S. (2013). Spectrum of sequent calculi of first-order composition-nominative logics. In Problems in Progamming. № 3, p. 22–37 (in ukr).
9. SHKILNIAK, S. (2013). Sequent systems of logical deduction for pure first-order logics of partial predicates. In Computer mathematics. 2,
p. 88–96 (in ukr).
10. SHKILNIAK, O. (2016). Logical consequence relations in logics of quasiary predicates. In Problems in Progamming. № 1, p. 13–25 (in ukr).
11. SMIRNOVA, E. (1996). Logic and Philosophie. Moskow: ROSSPEN (in rus).
Про авторів:
Нікітченко Микола Степанович,
доктор фізико-математичних наук, професор,
завідувач кафедри Теорії та технології програмування.
Кількість наукових публікацій в українських виданнях – понад 200, у тому числі у фахових виданнях – 100.
Кількість наукових публікацій в іноземних виданнях – 30.
Індекс Гірша – 8 (6 з 2010).
http://orcid.org/0000-0002-4078-1062.
Шкільняк Оксана Степанівна,
кандидат фізико-математичних наук, доцент,
доцент кафедри Інформаційних систем.
Кількість наукових публікацій в українських виданнях – 78, у тому числі у фахових виданнях – 30.
Кількість наукових публікацій в іноземних виданнях – 8.
http://orcid.org/0000-0003-4139-2525
Шкільняк Степан Степанович,
доктор фізико-математичних наук, професор,
професор кафедри Теорії та технології програмування.
Кількість наукових публікацій в українських виданнях – понад 200, у тому числі у фахових виданнях – 92.
Кількість наукових публікацій в іноземних виданнях – 14.
Індекс Гірша – 4 (3 з 2010).
http://orcid.org/0000-0001-8624-5778.
Місце роботи авторів:
Київський національний університет імені Тараса Шевченка ,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 2590519.
E-mail: me.oksana@gmail.com, nikitchenko@unicyb.kiev.ua, sssh@unicyb.kiev.ua.
|