Pure first-order quasiary logics with equality predicates
Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are stud...
Збережено в:
| Дата: | 2018 |
|---|---|
| Автори: | , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2018
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/316 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-316 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/42/2c523fe1b6024bd0ed05cd5b5fb1f842.pdf |
| spelling |
pp_isofts_kiev_ua-article-3162024-04-28T11:52:03Z Pure first-order quasiary logics with equality predicates Чистые первопорядковые квазиарные логики с предикатами равенств Чисті першопорядкові квазіaрні логіки з предикатами рівності Nikitchenko, M.S. Shkilniak, S.S. logic; predicate; equality; logical consequence; sequent calculus UDC 004.42:510.69 логика; предикат; равенство; логическое следствие; секвенциальное исчисление УДК 004.42:510.69 логіка; предикат; рівність; логічний наслідок; секвенційне числення УДК 004.42:510.69 Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are studied. The main attention is paid to logics with special equality relations. Logics with weak equality and strong equality are defined, their properties are investigated. Languages of such logics and their interpetations are described. The following classes of interpretations (semantics) are identified: partial deterministic, non-deterministic, total deterministic, and total non-deterministic interpetations. Semantic properties of the proposed logics are investigated. Special attention is paid to consequence relations for sets of formulas. Based on the properties of these relations a number of calculi of sequent type is proposed. Basic rules of these calculi and corresponding closedness conditions are formulated; the procedure of sequent tree construction is described. For the proposed calculi correctness and completeness theorems are proved. The proof of completeness is based on the construction of countermodel for an unclosed path in the sequent tree.Problems in programming 2017; 2: 03-23 Изучаются чистые первопорядковые логики однозначных и неоднозначных квазиарных предикатов. Эти логики являются программно-ориентированными логическими формализмами, отображающими такие свойства программ как частичность, недетерминизм, нефиксированную арность. Основное внимание уделено логикам со специальными предикатами равенства. Выделены чистые первопорядковые логики с предикатами слабого равенства и с предикатами строгого равенства. Описаны языки и семантические модели этих логик, исследованы их семантические свойства, в частности, свойства, связанные с предикатами равенства. Указаны свойства отношений логического следствия для множеств формул. На основе этих свойств для чистых первопорядковых логик с предикатами равенства построен ряд исчислений секвенциального типа, для них доказаны теоремы корректности и полноты.Problems in programming 2017; 2: 03-23 Вивчаються чистi першопорядковi квазіарні логіки однозначних та неоднозначних часткових предикатів. Основна увага приділена таким логікам із спеціальними предикатами рівності. Виділено чистi першопорядковi логіки з предикатами слабкої рівності та з предикатами строгої рівності. Описано мови та семантичні моделі цих логік, досліджено їх семантичні властивості, зокрема, властивості, пов’язані з предикатами рівності. Наведено властивості відношень логічного наслідку для множин формул. На базі цих властивостей для чистих першопорядкових логік з предикатами рівності побудовано низку числень секвенційного типу, для них доведено теореми коректності та повноти.Problems in programming 2017; 2: 3-23 Інститут програмних систем НАН України 2018-11-19 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/316 10.15407/pp2017.02.003 PROBLEMS IN PROGRAMMING; No 2 (2017); 3-23 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2017); 3-23 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2017); 3-23 1727-4907 10.15407/pp2017.02 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/316/311 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:52:03Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
logic predicate equality logical consequence sequent calculus UDC 004.42:510.69 |
| spellingShingle |
logic predicate equality logical consequence sequent calculus UDC 004.42:510.69 Nikitchenko, M.S. Shkilniak, S.S. Pure first-order quasiary logics with equality predicates |
| topic_facet |
logic predicate equality 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.S. |
| author_facet |
Nikitchenko, M.S. Shkilniak, S.S. |
| author_sort |
Nikitchenko, M.S. |
| title |
Pure first-order quasiary logics with equality predicates |
| title_short |
Pure first-order quasiary logics with equality predicates |
| title_full |
Pure first-order quasiary logics with equality predicates |
| title_fullStr |
Pure first-order quasiary logics with equality predicates |
| title_full_unstemmed |
Pure first-order quasiary logics with equality predicates |
| title_sort |
pure first-order quasiary logics with equality predicates |
| title_alt |
Чистые первопорядковые квазиарные логики с предикатами равенств Чисті першопорядкові квазіaрні логіки з предикатами рівності |
| description |
Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are studied. The main attention is paid to logics with special equality relations. Logics with weak equality and strong equality are defined, their properties are investigated. Languages of such logics and their interpetations are described. The following classes of interpretations (semantics) are identified: partial deterministic, non-deterministic, total deterministic, and total non-deterministic interpetations. Semantic properties of the proposed logics are investigated. Special attention is paid to consequence relations for sets of formulas. Based on the properties of these relations a number of calculi of sequent type is proposed. Basic rules of these calculi and corresponding closedness conditions are formulated; the procedure of sequent tree construction is described. For the proposed calculi correctness and completeness theorems are proved. The proof of completeness is based on the construction of countermodel for an unclosed path in the sequent tree.Problems in programming 2017; 2: 03-23 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2018 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/316 |
| work_keys_str_mv |
AT nikitchenkoms purefirstorderquasiarylogicswithequalitypredicates AT shkilniakss purefirstorderquasiarylogicswithequalitypredicates AT nikitchenkoms čistyepervoporâdkovyekvaziarnyelogikispredikatamiravenstv AT shkilniakss čistyepervoporâdkovyekvaziarnyelogikispredikatamiravenstv AT nikitchenkoms čistíperšoporâdkovíkvazíarnílogíkizpredikatamirívností AT shkilniakss čistíperšoporâdkovíkvazíarnílogíkizpredikatamirívností |
| first_indexed |
2024-09-16T04:07:49Z |
| last_indexed |
2024-09-16T04:07:49Z |
| _version_ |
1818568256736198656 |
| fulltext |
Теоретичні та методологічні основи програмування
© М.С. Нікітченко, С.С. Шкільняк, 2017
ISSN 1727-4907. Проблеми програмування. 2017. № 2 3
УДК 004.42:510.69
М.С. Нікітченко, C.С. Шкільняк
ЧИСТІ ПЕРШОПОРЯДКОВІ КВАЗІAРНІ ЛОГІКИ З
ПРЕДИКАТАМИ РІВНОСТІ
Вивчаються чистi першопорядковi квазіарні логіки однозначних та неоднозначних часткових предика-
тів. Основна увага приділена таким логікам із спеціальними предикатами рівності. Виділено чистi пер-
шопорядковi логіки з предикатами слабкої рівності та з предикатами строгої рівності. Описано мови та
семантичні моделі цих логік, досліджено їх семантичні властивості, зокрема, властивості, пов’язані з
предикатами рівності. Наведено властивості відношень логічного наслідку для множин формул. На базі
цих властивостей для чистих першопорядкових логік з предикатами рівності побудовано низку числень
секвенційного типу, для них доведено теореми коректності та повноти.
Ключові слова: логіка, предикат, рівність, логічний наслідок, секвенційне числення.
Вступ
Поняття і методи математичної ло-
гіки засвідчують високу ефективність при
розв'язанні задач інформатики й програму-
вання. Для цього розроблено багато різно-
манітних логічних систем (див., напр., [1]).
Такі системи зазвичай базуються на класи-
чній логіці предикатів. Ця логіка добре до-
сліджена, вона є основою низки спеціаль-
них логік (модальних, темпоральних, про-
грамних тощо). Водночас класична логіка
має [2, 3] низку обмежень, що ускладнює її
використання. Тому на перший план вису-
вається проблема побудови нових логічних
формалізмів, більше адаптованих до по-
треб програмування. Такими є компози-
ційно-номінативні логіки (КНЛ) часткових
предикатів. Вони базуються на загальних
класах часткових відображень, заданих на
наборах іменованих значень. Такі відо-
браження названо квазіарними.
Мета даної роботи – це дослідження
чистих першопорядкових КНЛ однознач-
них та неоднозначних квазіарних предика-
тів. Описано семантичні моделі та мови
чистих першопорядкових КНЛ, дослідже-
но семантичні властивості. Основна увага
приділена таким логікам із спеціальними
предикатами рівності. Виділено предикати
слабкої рівності та строгої рівності, описа-
но властивості, пов’язані з цими предика-
тами. Наведено властивості відношень ло-
гічного наслідку для множин формул. На
базі цих властивостей для чистих першо-
порядкових КНЛ з предикатами рівності
побудовано низку числень секвенційного
типу. Наведено умови замкненості секвен-
ції та базові секвенційні форми цих чис-
лень, для них доведено теореми коректно-
сті та повноти.
Можна виділити такі рівні чистих
першопорядкових КНЛ:
– базовий рівень чистих першопо-
рядкових КНЛ (ЧКНЛ);
– чисті першопорядкові КНЛ з пре-
дикатами слабкої рівності (ЧКНЛР);
– чисті першопорядкові КНЛ з пре-
дикатами строгої рівності (ЧКНЛРС).
ЧКНЛ добре досліджені (див.,
напр., [2–5]). Реномінативні КНЛ з рівніс-
тю описано в [6, 7]. У даній роботі увагу
зосередимо на вивченні ЧКНЛ з рівністю –
ЧКНЛР та ЧКНЛРС.
Поняття, які в цій статті не визна-
чаються, будемо тлумачити в сенсі [3, 5].
1. Різновиди квазіарних предикатів
Нехай V і A – множини, які будемо
трактувати як множину предметних імен
(змінних) і множину предметних значень.
V-A-іменна множина (V-A-ІМ) – це
однозначна функція вигляду d : VA.
Множину всіх V-A-ІМ позначаємо VA.
Введемо функцію asn :
VA2V так:
asn(d) = {vV | v ad для деякого aA}.
Для V-A-ІМ вводимо операцію ||–х
видалення компоненти з іменем х та опе-
рацію накладання:
d ||–х = [v ad | v х];
= [v a | vasn()].
Теоретичні та методологічні основи програмування
4
Задамо операцію реномінації
n
n
vv
xx
,...,
,...,
1
1
r :
)(r
,...,
,...,
1
1
dn
n
vv
xx
1,..., 1 1|| [ ( ),..., ( )].
nv v n nd v d x v d x
Введемо для y1,..., yn позначення y .
Тоді замість n
n
vv
xx
,...,
,...,
1
1
r також пишемо v
x r .
Послідовне застосування двох опе-
рацій реномінації v
x r та u
y r можна подати
[3] у вигляді однієї операції реномінації,
яку називають згорткою операцій v
x r та u
y r
і позначають u
y
v
x r . Тоді
)(r)(r(r dd u
y
v
x
u
y
v
x .
Маємо )(r)(r
,
, dd v
x
vz
xz .
Тотожна реномінація r (без параме-
трів) діє як тотожне відображення: r(d) = d.
V-A-квазіарний предикат – це дові-
льна (часткова неоднозначна, взагалі ка-
жучи) функція вигляду
P : VA {T, F},
де {T, F} – множина істиннісних значень.
Часткові неоднозначні V-A-квазіар-
ні предикати трактуємо як відповідності
(відношення) між VA та множиною {T, F}.
Такі предикати названо [3–5] предикатами
реляційного типу, або R-предикатами.
Кожний R-предикат P : VA {T, F}
однозначно задається областю істинності
T(P) = {dVA | TP[d]} та областю хибнос-
ті F(P) = {dVA | FP[d] }.
Предикат P : VА {T, F} назвемо:
– однозначним, якщо T(P)F(P) = ;
– тотальним, якщо T(P)F(P) = VA;
– неспростовним (частково істин-
ним), якщо F(P) = ;
– виконуваним, якщо T(P) ;
– тотожно істинним (позн. T), якщо
T(P) = VА та F(P) = ;
– тотожно хибним (позн. F), якщо
F(P) = VА та T(P) = ;
– тотально істинним, якщо T(P) = VА;
– тотально хибним, якщо F(P) = VА;
– всюди невизначеним (позн. ), як-
що T(P) = F(P) = ;
– тотально насиченим (позн. ), як-
що T(P) = VА та F(P) = VА.
Кожний неспростовний і кожний
невиконуваний предикат є однозначними.
Часткові однозначні предикати на-
звемо P-предикатами, тотальні – T-преди-
катами, тотальні однозначні – TS-предика-
тами. Класи V-A-квазіарних R-предикатів,
P-предикатів, T-предикатів, TS-предикатів
позначаємо V
APrR , V
APrP , V
APrT , V
APrTS .
Предметне ім’я хV (строго) неіс-
тотне для V-A-квазіарнoго предиката P,
якщо для довільних d1, d2
VA маємо:
d1||–х = d2 ||–х P[d1] = P[d2].
V-A-квазіарний предикат P моно-
тонний, якщо: d d' P[d] P[d'].
V-A-квазіарний предикат P анти-
тонний, якщо: d d' P[d] P[d'].
Для однозначних квазіарних преди-
катів монотонність стає еквітонністю.
Предикат P еквітонний, якщо:
P(d) та d d' P(d') = P(d).
Монотонні R-предикати, антитонні
R-предикати, еквітонні P-предикати, анти-
тоннi T-предикати названо [5] RM-преди-
катами, RА-предикатами, PE-предикатами,
TА-предикатами. Класи цих предикатів по-
значаємо , , V
A
V
A PrRAPrRM
V
A
V
A PrTAPrPE , .
Константні предикати F,T,, мо-
нотонні (еквітонні) й антитонні, при цьому
предикати F,T, – однозначні.
Спеціальні предикати-індикатори
Ez наявності у вхідних даних компоненти з
іменем zV задаємо [5] так:
T(Ez) = {d | d(z)} = {d | zasn(d)};
F(Ez) = {d | d(z)} = {d | zasn(d)}.
Предикати-індикатори Ez тотальні,
однозначні, немонотонні, неантитонні.
Кожне xV таке, що x z, неістотне для Ez.
На рівнях ЧКНЛР та ЧКНЛРС мож-
на ототожнювати й розрізняти значення
предметних імен за допомогою спеціаль-
них 0-арних композицій – параметризова-
них за іменами предикатів рівності. Можна
Теоретичні та методологічні основи програмування
5
розглядати дві різновидності цих предика-
тів: слабкої (з точністю до визначеності)
рівності =ху та строгої (точної) рівності xy.
Предикати =ху та ху задаємо так:
T(=xy) = {d | d(x), d(y) та d(x) = d(y)},
F(=xy) = {d | d(x), d(y) та d(x) d(y)};
T(xy) = {d | d(x), d(y) та d(x) = d(y)}
{d | d(x) та d(y)},
F(xy) = {d | d(x), d(y), d(x) d(y)}
{d | d(x), d(y) або d(x), d(y)}.
Предикати =xy та xy також тради-
ційно позначають x = y та x y.
Предикати =xy часткові однозначні,
вони монотонні й еквітонні.
Предикати xy тотальні однозначні,
вони немонотонні й неантитонні:
Приклад 1. Маємо xy([ az ]) = T,
xy([ ayaxaz ,, ]) = T, водночас
xy([ axaz , ]) = F.
Кожне zV таке, що x z та y z, не-
істотне для =xy та для xy.
Предикат P
~
дуальний [5] до преди-
ката P, якщо )()
~
( PFPT та )()
~
( PTPF .
Відображення дуалізації V
A
V
A PrRPrR :
задаємо [5] так: PP
~
)( .
Якщо ,V
APrTSP то (P) = P. Тому
(Ex) = Ex, (xy) = xy, (T) = T, (F) = F.
Також маємо () = , .= )(
Для класів предикатів маємо:
V
A
V
A PrRPrR )( ,
V
A
V
A PrTSPrTS )( ,
)( V
APrP = ,V
A
PrT )( V
APrT =
V
APrP ;
)( V
APrPE = ,V
APrTA )( V
APrTA = ,V
APrPE
)( V
APrRM = ,V
APrRA )( V
APrRA =
V
APrRM .
2. Композиційні алгебри чистих
першопорядкових логік
Семантичною основою КНЛ є ком-
позиційні предикатні системи. Для чистих
першопорядкових логік такі системи ма-
ють вигляд (А, PrА, C), де PrА – певний
клас V-A-квазіарних предикатів, C – мно-
жина композицій відповідного рівня. Така
система задає алгебру даних (A, PrА) і ком-
позиційну алгебру предикатів (PrА, C).
Базовими композиціями ЧКНЛ є
[2, 3] логічні зв’язки і , композиції ре-
номінації v
xR та квантифікації x.
Базовими композиціями ЧКНЛР є
, , ,Rv
x x, =ху.
Базовими композиціями ЧКНЛРС є
, , ,Rv
x x, ху.
Задамо , , x через області істин-
ності й хибності відповідних предикатів:
T(P) = F(P); F(P) = T(P);
T(PQ) = T(P)T(Q); F(PQ) = F(P)F(Q);
T(xP) = {d | d x a T(Р) для деякого aA};
F(xP) = {d | d x a F(Р) для всіх aA}.
Композицію v
xR задаємо умовою:
))(r())((R dPdP v
x
v
x для всіх dVА.
Похідні композиції , &, , х ви-
ражаються [2, 3] через , , х:
PQ = PQ;
P&Q = (PQ);
PQ = (PQ)&(QP);
хР = хР.
Алгебру ),,( CQPrRQR V
A
V
A де
CQ = {, , ,R v
x x}, назвемо чистою пер-
шопорядковою композиційною алгеброю
квазіарних предикатів.
Алгебру ,),( E
V
A
V
AE CQPrRRQ де
CQE = {, , ,R v
x x, =xy}, назвемо чистою
першопорядковою композиційною алгеб-
рою з предикатами слабкої рівності.
Алгебру ,),( ES
V
A
V
AES CQPrRRQ де
CQES = {, , ,R v
x x, xy}, назвемо чистою
першопорядковою композиційною ал-
геброю з предикатами строгої рівності.
Композиції , , ,R v
x x зберігають
[3, 5] однозначність, тотальність, монотон-
ність (еквітонність), антитонність квазіа-
рних предикатів. Тому можна виділити [5]
такі підалгебри алгебри V
AQR :
Теоретичні та методологічні основи програмування
6
),,( CQPrPQP V
A
V
A
),,( CQPrTQT V
A
V
A
),( CQPrTSQTS V
A
V
A ,
),,( CQPrRMQRM V
A
V
A
),,( CQPrRAQRA V
A
V
A
),,( CQPrPEQPE V
A
V
A
),( CQPrTAQTA V
A
V
A .
0-арні композиції =xy часткові, одно-
значні й еквітонні, тому виділяємо такі пі-
далгебри алгебри V
AERQ :
),,( E
V
A
V
AE CQPrPPQ
).,( E
V
A
V
AE CQPrPEPEQ
0-арні композиції xy немонотонні й
неантитонні, тому виділяємо такі підалге-
бри алгебри
V
AES RQ :
,),( ES
V
A
V
AES CQPrPPQ
,),( ES
V
A
V
AES CQPrTTQ
).,( ES
V
A
V
AES CQPrTSTSQ
Те, що є підалгеброю алгебри ,
позначимо . Тоді маємо:
V
A
V
A QPQTS та
V
A
V
A QTQTS ;
V
A
V
A QPQPE та
V
A
V
A QRMQPE ;
V
A
V
A QTQTA та
V
A
V
A QRAQTA ;
V
A
V
A
V
A
V
A
V
A QRQRAQRMQTQP , , , ;
V
AE
V
AE
V
AE RQPQPEQ ;
V
AES
V
AES PQTSQ та
V
AES
V
AES TQTSQ ;
V
AES
V
AES
V
AES RQTQPQ , .
Алгебри ),Pr( 1 C та ),Pr( 2 C дуальні,
якщо ( 1Pr ) = 2Pr та ( 2Pr ) = 1Pr .
Маємо дуальні пари
V
AQP та ,V
AQT
V
AQPE та ,V
AQTA
V
AQRM та ,V
AQRA
V
AES PQ
та
V
AESTQ . Алгебри , , , V
AES
V
A
V
A TSQQRQTS
V
AES RQ автодуальні.
Основні властивості пропозиційних
композицій та кванторів аналогічні вла-
стивостям класичних логічних зв’язок та
кванторів (див. [2, 3]). Водночас [3] для
квазіарних предикатів невірні деякі пов'я-
зані з кванторами закони класичної логіки.
Наведемо (див. також [3, 5]) власти-
вості, пов’язані з композицією реномінації.
R) PP )(R – тотожна реномінація.
RI) )(R)(R ,
, PP v
x
vz
xz .
RR) (R ,
,
xu
yv хP) = (Ru
v хP).
RU) )(R)(R ,
, PP v
x
vz
xy .
Ren) ).(R PzyP y
z
Для RU та Ren z неістотне для P.
R) )(R)(R PP v
x
v
x .
R) )(R)(R)(R QPQP v
x
v
x
v
x .
RR) )(R))(R(R PP w
y
v
x
w
y
v
x .
Тут w
y
v
x R – згортка
v
xR і w
yR , за-
даємо [3, 5] згортку реномінацій так:
)))((R(R))((R dPdP w
y
v
x
w
y
v
x
)).(r( dP v
x
w
y
Rs) R ( ) R ( ), v v
x xyP y P { , }y v x .
R) R ( ) R ( ), v v y
x x zyP z P якщо z
неістотне для P та { , }z v x .
Маємо [5] такі властивості, пов’яза-
ні з елімінацією кванторів:
))(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 .
Розглянемо властивості, пов’язані з
предикатами рівності.
Маємо такі співвідношення:
T(=xy)
T(Ex) T(Ey) T(Ex) T(Ey);
F(=xy)
T(Ex) T(Ey) T(Ex) T(Ey).
Теоретичні та методологічні основи програмування
7
Тому предикати xy можна подати
через предикати =xy та Ez.
Теорема 1. Маємо
xy = (=xy & Ex & Ey) (Ex & Ey).
Опишемо властивості реномінації
предикатів рівності (див. також [6, 7]).
RD) за умови , { }x y u маємо
u
vR (=xy) = =xy та
u
vR (xy) = xy;
за умови }{uy маємо
xu
zv
,
,R (=xy) = =zy та
xu
zv
,
,R (xy) = zy;
yxu
wzv
,,
,,R (=xy) = =zw та
yxu
wzv
,,
,,R (xy) = zw.
Для =xy та xy маємо рефлективність,
симетричність, транзитивність.
RfP) предикати =xx неспростовні;
предикати xx тотожно істинні.
SmP) для кожного dVA маємо
=xy(d) = =yx(d) та xy(d) = yx(d).
TrP) для кожного dVA маємо:
=xy(d) = T та =yz(d) = T =xz(d) = T;
xy(d) = T та yz(d) = T xz(d) = T.
Як наслідок отримуємо:
предикати =xy & =yz =xz неспростовні;
предикати xy & yz xz тотожно істинні
(адже вони тотальні).
REP) для кожних PPrА та dVA
маємо властивість заміни рівних:
=xy(d) = T ))((R))((R ,
,
,
, dPdP vu
yz
vu
xz ;
xy(d) = T ))((R))((R ,
,
,
, dPdP vu
yz
vu
xz .
Розглянемо властивості квантифі-
кації предикатів строгої рівності.
x xy(d) = T існує aА таке, що
d(y) = a d(y) Ey(d) = T.
x xy(d) = F для кожного aА
невірно, що d(y) = a d(y) Ey(d) = F.
Таким чином, x xy = Ey.
Звідси отримуємо: x xy = Ey.
x xy(d) = T d(y) = a для кожного
aА. Якщо |А| 2, то це неможливо; якщо
|А| = 1, то це означає d(y), тобто Ey(d) = T;
x xy(d) = F |А| 2 або |А| = 1 та d(y).
Таким чином, якщо |А| 2, то
x xy(d) = F для всіх dVA;
якщо |А| = 1, то x xy(d) = F за умо-
ви d(y) та x xy(d) = T, за умови d(y),
звідки x xy(d) = Ey(d), за умови |А| = 1.
Звідси отримуємо: якщо |А| 2, то
x xy = F; якщо |А| = 1, то x xy = Ey.
Як наслідок: |А| 2 x xy = T;
|А| = 1 x xy = Ey.
Тепер властивості квантифікації
предикатів слабкої рівності.
x (=xy)(d) = T існує aА таке, що
d(y) = a d(y) Ey(d) = T;
x =xy(d) = F d(y) та для кожно-
го aА неправильно d(y) = a, а це немож-
ливо;
x =xy(d) невизначене d(y).
Таким чином, x =xy = Ey .
Звідси маємо: x =xy = Ey & .
x =xy(d) = T d(y) = a для кожного
aА. Якщо |А| 2, то це неможливо; якщо
|А| = 1, то це означає d(y), тобто Ey(d) = T;
x =xy(d) = F d(y) та |А| 2;
x =xy(d) невизначене d(y).
Таким чином: якщо |А| 2, то
x =xy(d) = F за умови d(y) та x =xy(d) не-
визначене за умови d(y); якщо |А| = 1, то
x =xy(d) = T за умови d(y) та x =xy(d) не-
визначене за умови d(y). Звідси маємо:
якщо |А| 2, то x =xy = Ey & ;
якщо |А| = 1, то x =xy = Ey .
Це дає: |А| 2 x =xy = Ey ;
|А| = 1 x =xy = Ey & .
Таким чином, доведена
Теорема 2. 1) x xy = Ey;
|А| 2 x xy = F, |А| = 1 x xy = Ey;
2) x =xy = Ey ;
|А| 2 x =xy = Ey & ,
|А| = 1 x =xy = Ey .
3. Мови чистих першопорядкових
логік та їх інтерпретації
Побудова композиційної предикат-
ної алгебри дає змогу визначити мову ло-
гіки: терми алгебри є формулами мови.
Теоретичні та методологічні основи програмування
8
Алфавіт мови ЧКНЛ: символи базо-
вих композицій , , ,v
xR x; множина Ps
предикатних символів (ПС) – сигнaтура
мови; множина V предметних імен.
Дамо індуктивне визначення мно-
жини Fr формул мови ЧКНЛ.
Ф0) кожний рPs є формулою; такі
формули назвемо атомарними.
Ф1) нехай , Fr; тоді Fr,
Fr, ,FrRv
x xFr.
Формули вигляду v
xR називаємо
R-формулами.
Алфавіт мови ЧКНЛР відрізняється
від алфавіту мови ЧКНЛ додаванням =ху до
символів базових композицій. До визна-
чення множини Fr додаємо пункт:
ФE) кожний =ху, де х, уV, є форму-
лою; такі формули атомарні.
Алфавіт мови ЧКНЛРC відрізня-
ється від алфавіту мови ЧКНЛ додаванням
ху до символів базових композицій. До
визначення множини Fr додаємо пункт:
ФES) кожний ху, де х, уV, є фор-
мулою; такі формули атомарні.
При зафіксованій множині базових
композицій мови КНЛ відрізняються сиг-
натурою і способами запису формул (ми
використовуємо префіксну форму).
Для запису формул далі використо-
вуємо інфіксну форму та символи похід-
них композицій , &, , x (див. [3]).
Інтерпретуємо мови ЧКНЛ, ЧКНЛР,
ЧКНЛРС на композиційних системах
квазіарних предикатів CS = (А, PrА, C), де
C – множина композицій відповідного рі-
вня. Символи множини Ps позначають
(виділяють) базові предикати в PrА, для
цього задаємо тотальне однозначне
I : Ps PrA. Відображення інтерпретації
формул I : FrPrA є продовженням
I : Ps PrA згідно побудови формул із
простіших за допомогою символів базо-
вих композицій:
IФ) I() = (I()),
I() = (I(), I()),
( ) R ( ( )) v v
x xI R I , I(x) = x(I()).
Для мови ЧКНЛР додатково маємо:
IE) I(=ху) = =ху.
Для мови ЧКНЛРС маємо:
IES) I(ху) = ху.
Трійку J = (CS, Ps, I) назвемо інтер-
претацією мови ЧКНЛ (ЧКНЛР, ЧКНЛРС)
сигнатури Ps. Cкорочено інтерпретації мо-
ви позначаємо як (A, Ps, I) чи (A, I).
Предикат I() – значення формули
при інтерпретації J – позначимо J.
Предметне ім'я xV неістотне для
формули , якщо при кожній інтерпретації
J ім'я x неістотне для предиката J.
Надалі розглядаємо логіки, розши-
рені шляхом виділення підмножини U V
тотально неістотних предметних імен (не-
істотних для всіх базових предикатів).
Вважаємо, що U розв’язна відносно V.
Для КНЛ множину тотально неіс-
тотних імен традиційно задають [3, 5] за
допомогою тотальної : Ps2V, тоді
Psp
pU
)( . Для визначення множин га-
рантовано неістотних для формул імен та-
ку продовжуємо (див. [3]) до : Fr2V.
У випадках ЧКНЛР та ЧКНЛРС ма-
ємо (=ху) = V \{x, y} та (ху) = V \{x, y}.
Якщо х(), то (див. [3]) ім’я х не-
істотне для формули .
Формула примітивна, якщо вона
атомарна або має вигляд ,pRz
x де рPs,
z
xR не має пар тотожних імен,
)(}{ pz .
Виділення в чистих першопорядко-
вих логіках підалгебр T-предикатів, P-пре-
дикатів, TS-предикатів виділяє відповідні
класи інтерпретацій: загальний клас R-ін-
терпретацій та підкласи P-інтерпретацій,
T-інтерпретацій, TS-інтерпретацій. Такі
класи інтерпретацій названо [4, 5] семан-
тиками, їх позначаємо R, P, T, TS.
Нехай – деякий клас інтерпрета-
цій (семантика).
Формула неспростовна (частково
істинна) при інтерпретації J (позн. J |= ),
якщо предикат J – неспростовний.
Теоретичні та методологічні основи програмування
9
Формула неспростовна в (позн.
|= ), якщо J |= при кожній J.
Формула тотально істинна при
інтерпретації J (позн. J | ), якщо преди-
кат J – тотально істинний.
Формула тотально істинна в
(позн. | ), якщо J | при кожній J.
Формула тотожно істинна при ін-
терпретації J (позн. J |=id ), якщо преди-
кат J – тотожно істинний.
Формула тотожно істинна в
(позн. |=id ), якщо J |=id для всіх J.
Якщо семантика зафіксована, то
замість |=, |, |=id пишемо |=, |, |=id .
Формула виконувана при інтер-
претації J, якщо предикат J – виконува-
ний. Формула виконувана в , якщо
виконувана при деякій J.
Твердження 1. J |=id J |= ,
J |=id J | ; |=id |= , |=id | .
Для ЧКНЛ маємо (див. [5]).
Теорема 3. { |
R|= } = { |
R| } =
= { |
R|=id
} = ;
{ |
P| } = { |
P|=id
} = { |
T|= } =
= { |
T|=id
} = ;
{ |
P|= } = { |
T| } = { |
TS|=id
} =
= { |
TS|= } = { |
TS| }.
У випадках T-семантики і TS-семан-
тики предикати слабкої рівності відсутні.
Отже, для ЧКНЛР можна розглядати лише
R-семантику і P-семантику.
Приклад 2. R|= x = x, R|= x = y y = x;
P|= x = x, P|= x = y y = x.
Тому для ЧКНЛР маємо.
Теорема 4. 1) { |
R| } =
= { |
R|=id
} = ; { |
R|= } ;
2) { |
P| } = { |
P|=id
} = ;
{ |
P|= } .
Із теорем 3 та 4 випливає, що для
ЧКНЛ (окрім TS-семантики) та ЧКНЛР
множина тотожно істинних формул поро-
жня. Це не так для ЧКНЛРС.
Приклад 3. Маємо |=id x x та
|=id x y y x (тут – одне з R, P, T, TS).
Отже, для ЧКНЛРС пп.1 і 2 теоре-
ми 3 неправильні, правильним залишаєть-
ся п. 3.
4. Семантичні властивості формул
На основі різних співвідношень між
областями істинності та хибності предика-
тів можна ввести (див. [3–5, 8]) низку від-
ношень, які формалізують фундаментальне
поняття логічного наслідку. Спочатку за-
даємо відношення наслідку для двох фор-
мул при фіксованій інтерпретації 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 J|=T та J|=F ;
4) неспростовнісний, або IR-наслі-
док J|=IR : J|=IR T(J)F(J) = ;
5) дуальний до IR, або DI-наслідок
J|=DI : J|=DI F(J)T(J) = VA.
Відповідні відношення логічного
наслідку в семантиці задаємо за схемою:
|= , якщо J|= для всіх J.
У випадку TS-семантики усі наве-
дені відношення логічного наслідку втра-
чають відмінності [4, 5] і стають єдиним
відношенням, яке позначимо TS|= .
Для наведених відношень логічного
наслідку маємо [4, 5] співвідношення:
R|=T = R|=F = R|=TF ;
P|=IR = T|=DI = TS|= ;
P|=T = T|=F ;
P|=F = T|=T ;
P|=TF = T|=TF .
Серед цих відношень лише 5 різних,
тому достатньо розглядати
P|=IR, P|=T, P|=F, P|=TF, R|=TF.
Відношення
P|=IR, P|=T, P|=F, P|=TF
також позначаємо
|=IR, |=T, |=F, |=TF.
Для зазначених відношень маємо [3–5]:
R|=TF |=TF = |=T |=F ;
|=TF |=T |=IR, |=TF |=F |=IR .
Відношення логічного наслідку ін-
дукують відповідні відношення логічної
еквівалентності. Відношення еквівалент-
Теоретичні та методологічні основи програмування
10
ності при інтерпретації J JT , JF , JTF ,
JIR , JDI визначаємо за такою схемою:
J , якщо J|= та J|= .
Відношення логічної еквівалентнос-
ті PIR, PT, PF, PTF, RTF визначаємо за
схемою:
, якщо
|= та
|= .
Маємо
J для кожної J.
Відношення PIR, PT, PF, PTF та-
кож позначаємо IR, T, F, TF .
Описані вище відношення логічно-
го наслідку рефлексивні й транзитивні, ві-
дношення логічної еквівалентності реф-
лексивні, транзитивні й симетричні.
Властивості відношень логічного
наслідку вивчались в [2–5, 8]. Відношення
логічного наслідку в логіках монотонних
предикатів тa логіках антитонних предика-
тів досліджено в [8].
Особливу роль мають відношення
|=IR та IR , вони традиційно позначаються
[2, 3] як |= та . Це пов’язано з тим фактом,
що логічні зв’язки та узгоджуються з
відношеннями |=IR та IR :
|=IR P|= T| .
IR P|= T| .
Дуже важливим є відношення J TF :
JTF T(J) = T(J) та F(J) = F(J).
Отже, JTF означає, що J та J
– це один і той же предикат.
Маємо такі співвідношення між то-
тожно істинністю та відношеннями силь-
ного наслідку й еквівалентності.
Теорема 5. 1) P|=id
|=TF , водночас зворотне неправильне;
2) P|=id TF , водночас
зворотне неправильне;
3) R|=id
RTF , водночас
зворотне неправильне.
Твердження теореми нетривіальне
для ЧКНЛРС, адже для ЧКНЛ та ЧКНЛР
{ |
P|=id
} = та { |
R|=id
} = , для
них твердження теореми тривіально пра-
вильне.
На основі властивостей предикатів
отримуємо відповідні властивості формул.
Властивості пропозиційного рівня
описано в [2, 3], наведемо тут основні вла-
стивості, пов’язані з реномінаціями, кван-
торами та предикатами рівності.
R) TFR )( .
RI) )()(,
, v
xTF
vz
xz RR .
RU) )()(,
, v
xTF
vz
xy RR , якщо z
неістотне для Ф.
RR) )())(( w
y
v
xTF
w
y
v
x RRR .
R) )()( v
xTF
v
x RR .
R) )()()( v
x
v
xTF
v
x RRR .
Реномінація предикатів рівності:
RD) за умови , { } маємоx y u
xyTFxy
u
vxyTFxy
u
v RR )( тт)( ;
маємо }{ умови за uy
zyTFxy
xu
zvR
,
, )(
та zyTFxy
xu
zvR
,
, )( ,
, , , ,
, , , , ( ) та ( )u x y u x y
v z u xy TF zu v z u xy TF zuR R .
Для предикатів рівності маємо влас-
тивості рефлективності, симетричності, а
також транзитивності й заміни рівних.
Rf) P|= x = x, R|= x = x; |=id x x.
Sm) P|= x = y y = x, R|= x = y y = x;
|=id x y y x.
Tr) P|= х = y y = z х = z,
R|= х = y y = z х = z;
|=id х y y z х z.
ER) |= 1 1 ... n nx y x y
)),()((
,...,,
,...,,
,...,,
,...,,
1
1
1
1
n
n
n
n
vvu
yyz
vvu
xxz
RR
– P чи R;
1 1| ... n nx y x y
)),()((
,...,,
,...,,
,...,,
,...,,
1
1
1
1
n
n
n
n
vvu
yyz
vvu
xxz
RR
– P чи R;
1 1| ...id n nx y x y
)),()((
,...,,
,...,,
,...,,
,...,,
1
1
1
1
n
n
n
n
vvu
yyz
vvu
xxz
RR
– T чи TS.
Kвантифікація предикатів рівності:
QE) x xy TF Ey.
Теоретичні та методологічні основи програмування
11
Для предикатів слабкої рівності по-
дібний вираз можна записати лише при
розширенні сигнатури символом всюди
невизначеного предиката: x =xy TF Ey .
Основою еквівалентних перетво-
рень формул є [2, 3] теорема еквівалент-
ності. Вона формулюється для відношень
RTF, TF, IR . Для T та F теорема непра-
вильна.
Теорема 6. Нехай ' отримано з
формули заміною деяких входжень
1, ..., n на 1, ..., n. Якщо 1
1, ...,
n
n, то
'.
Важливе поняття Rs-Un-еквівалент-
них формул вводимо так (див. також [5]).
Rs-формою R-формули ),(,,
,, vux
zyxR
де { } ( ), u назвемо R-формулу )(v
zR ,
утворену із )(,,
,, vux
zyxR всеможливими спро-
щенням на основі властивостей R, RI, RU,
RR, а також RD (застосування R та RD
може дати Rs-форму, яка не буде R-фор-
мулою). Rs-форми R-формул чи їх запере-
чень назвемо Rs-формулами.
Властивості R, RI, RU, RR, RD га-
рантують: якщо та мають однакові Rs-
форми, то T(J) = T(J) та F(J) = F(J)
для всіх інтерпретацій J.
Нехай Un V – множина імен, трак-
тованих як неозначені (таку Un задаємо за
допомогою предикатів-індикаторів Ez), а
символ V позначає відсутність значення.
Нехай R-формула uxr
vysR ,,
,, така:
{ , , } , { , } r s y Un x v Un . Un-форма
формули uxr
vysR ,,
,, – це вираз ux
vR ,
, .
R-формули та назвемо Rs-Un-
еквівалентними, якщо та мають одна-
кові Rs-форми або ці Rs-форми мають од-
накові Un-форми.
Якщо R-формули та – Rs-Un-
еквівалентні, то та теж назвемо Rs-
Un-еквівалентними. Те, що та є Rs-Un-
еквівалентними, записуємо Un . Вважа-
ємо, що для , яка не є R-формулою чи
запереченням R-формули, її Un-форма збі-
гається із . Звідси Un .
Твердження 2. Якщо Un , то
для кожнoї інтерпретації J = (A, І) маємо:
T(J)
V\UnA = T(J)
V\UnA,
F(J)
V\UnA = F(J)
V\UnA.
Це означає: J (d) = J (d) для всіх
J = (A, І) та dVA, для яких asn(d)Un = ,
тобто Eu(d) = F для всіх uUn.
5. Відношення логічного наслідку
для множин формул
Нехай , Fr, J – інтерпретація.
Далі позначатимемо
)( JT як T (J),
)( JF як F (J),
)( 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 ), якщо J|=T та J|=F .
є IR-наслідком при J (позн.
J|=ID ), якщо T (J) F (J) = .
є DI-наслідком при J (позн.
J|=DI ), якщо F (J) T (J) = VA.
Відповідні відношення логічного
наслідку визначаємо за схемою:
|= , якщо J|= для всіх J.
Аналогом теореми 6 для множин
формул є теорема заміни еквівалентних.
Теорема 7. Нехай , тоді:
, |= , |= ; |= , |= , .
Тут – одне з відношень RTF, TF,
IR ; |= – одне з відношень R|=TF, |=TF, |=IR .
Опишемо властивості відношень
логічного наслідку для множин формул.
Надалі, якщо інше не зазначене, |=
означає одне з R|=TF, |=TF, |=T, |=F, |=IR.
M) нехай та , тоді
|= |= (монотонність).
Властивості декомпозиції формул:
L) , |= , |= .
Теоретичні та методологічні основи програмування
12
R) |= , |= , .
L) , |= , |= та , |= .
R) |= , |= , , .
L) (), |= , , |= .
R) |= , () |= , та
|= , .
Для |=IR додатково маємо (проте це
неправильно [3] для R|=TF, |=TF, |=T, |=F):
L) , |=IR |=IR , .
R) |=IR , , |=IR .
Наявність кожного з R|=TF, |=TF, |=T,
|=F, |=IR гарантує властивість:
С) , |= , .
Наступні властивості гарантують
наявність відповідного відношення:
СL) , , |= ( – T чи IR);
СR) |= , , ( – F чи IR);
СLR) , , |=TF , , .
Для |=IR в силу L та R властивості
СLR, СL, СR зводяться до С.
Загальні умови, які гарантують на-
явність того чи іншого відношення логіч-
ного наслідку, індуковані властивостями С,
СL, СR, СLR та твердженням 2.
Нехай , Fr, Un = {x | Ex};
нехай |= – одне з |=IR, |=T, |=F, |=TF, R|=TF .
Теорема 8. 1) Un , |= , ;
зокрема, , |= , ;
2) Un , ,
P|=T ;
зокрема, , ,
P|=T ;
3) Un
P|=F , , ;
зокрема,
P|=F , , ;
4) Un та
Un , ,
P|=TF , , ;
зокрема, , ,
P|=TF , ,
Справді, згідно твердження 2 за
умови Un для кожнoї J = (A, І) маємо:
T(J)
V\UnA = T(J)
V\UnA,
F(J)
V\UnA = F(J)
V\UnA.
Для доведення пп. 1, 2, 3, 4 далі
використовуємо властивості С, СL, СR,
СLR.
Властивості еквівалентних перетво-
рень, пов'язані з реномінацією, отриму-
ються на основі властивостей R, RI, RU,
RR, RR, R, R. Кожна з них продукує 4
відповідні властивості для відношення ло-
гічного наслідку, коли виділена формула чи
її заперечення знаходиться у лівій чи пра-
вій частині відношення. Наведемо для при-
кладу властивості RL, RR, RL, RR:
RL) R(), |= , |= ;
RR) |= R(), |= , ;
RL) ),( v
xR |= ),( v
xR |= ;
RR) |= , )( v
xR
|= , ))()(( v
x
v
x RR .
Властивості елімінації кванторів:
L) х, |= ,),( EzRx
z |= ;
RL) ),( xRu
v |= ,),(,
, EzR xu
zv |= ;
R) |= х, , Ez |= ),(x
zR ;
RR) |= ),( xRu
v
, Ez |= ),(,
,
xu
zvR ;
vR) , Ey |= х,
, Ey |= ),(, x
yRx ;
RvR) , Ey |= )(, xRu
v
, Ey |= )(),(, ,
, xu
yv
u
v RxR ;
vL) х, Ey, |=
,),(, EyRx x
y |= ;
RvL) ,),( EyxRu
v |=
,),(),( ,
, EyRxR xu
yv
u
v |= .
Для L і R умова: zfu(, , х)
форми для зовнішнього заперечення зайві,
базовими; для RL і RvL:
))(,,( xRfuz u
v .
E-розподіл та первісного означення:
Ed) |= Ey, |= та |= , Ey.
Ev) |= Ez, |= , де zfu(, ).
Теоретичні та методологічні основи програмування
13
Для |=IR в силу L та R властивості
вигляду із запереченням виділеної фо-
рмули є похідними.
Розглянемо властивості для слабкої
рівності. Зауважимо, що знімати запере-
чення, переносячи x = y з лівої частини
відношення у праву і навпаки, можна лише
для |=IR (це випливає з L та R), водночас
для |=T, |=F, |=TF, R|=TF це робити не можна.
Приклад 4. Маємо x = y, x = x |=T
y = y, водночас x = x |T y = y, x = y.
Справді, T( x = y x = x) {d | d(x)
та d(y)} {d | d(y)} = T(y = y); проте для
d = [xa] dT(x = x) та dT(y = y x = y) =
= T(y = y) T(x = y) = T(y = y).
Аналогічно y = y |=F x = y, x = x,
проте y = y, x = y |F x = x.
На основі Sm маємо властивості:
SmL) x = y, |= x = y, y = x, |= ;
SmR) |= , x = y |= , x = y, y = x.
Властивість Tr індукує:
TrL) x = y, y = z, |=
x = y, y = z, x = z, |= ( – T чи IR);
TrR) |= , x = y, y = z
|= , x = y, y = z, x = z ( – F чи IR);
Це випливає із T(x = y) T(y = z) =
= T(x = y) T(y = z) T(x = z).
Приклад 5. Для d = [xa, zb] ма-
ємо dF(x = y) F(y = z) та dF(x = z), тому
dF(x = z) F(x = y) F(y = z). Звідси отри-
муємо x = y, y = z |F x = y & y = z & x = z та
x = y y = z x = z |T x = y, y = z.
Проте x = y, y = z, x = z |=F x = y & y = z & x = z
та x = y y = z x = z |=T
|=T x = y, y = z, x = z.
Звідси TrL неправильна для |=F, а TrR
неправильна для |=T.
Таким чином, транзитивність слаб-
кої рівності порушується для відношень
|=T, |=F, |=TF, R|=TF, тому для ЧКНЛР адеква-
тним залишається лише відношення |=IR.
Властивість RD індукує властивості
реномінації рівності для відношення |=IR.
RDL) за умови , { }x y u маємо
IR
u
v yxR |),( , | IRx y ;
за умови { }y u маємо
IR
xu
zv yxR |),(,
, , | IRz y ;
IR
yxu
uzv yxR |),(
,,
,, , | IRz u ;
RDR) за умови , { }x y u маємо
),(| yxRu
vIR | , IR x y ;
за умови { }y u маємо
),(| ,
, yxR xu
zvIR | , IR z y ;
),(|
,,
,, yxR
yxu
uzvIR | , IR z u .
Властивість ER індукує властивості
заміни рівних для відношення |=IR :
ERL) IR
zu
xvRyx |),(, ,
,
IR
zu
yv
zu
xv RRyx |),(),(, ,
,
,
, ;
ERR) ),(|, ,
,
zu
xvIR Ryx
),(),(|, ,
,
,
,
zu
yv
zu
xvIR RRyx .
Властивість Rf індукує достатню
умову наявності відношення |=IR :
СRf) |=IR x = x, .
Розглянемо тепер властивості для
строгої рівності. Маємо
ELR) |= x y, x y, |= та
x y, |= |= x y, ;
ERLR) ),(| yxRu
v
|),( yxRu
v та
|),( yxRu
v ),(| yxRu
v .
Властивість RD індукує властивості
реномінації строгої рівності.
RDSL) за умови , { }x y u маємо:
|),( yxRu
v |,yx ;
за умови { }y u маємо:
|),(,
, yxR xu
zv , | z y ;
|),(
,,
,, yxR
yxu
uzv , | z u ;
Теоретичні та методологічні основи програмування
14
RDSR) за умови , { }x y u маємо:
),(| yxRu
v | , x y ;
за умови { }y u маємо:
),(| ,
, yxR xu
zv | , z y ;
),(|
,,
,, yxR
yxu
uzv | , z u .
На основі Sm та Tr отримуємо:
SmS) x y, |= x y, y x, |= ;
TrS) x = y, y = z, |=
x = y, y = z, x = z, |= .
Властивість ER індукує такі власти-
вості заміни рівних:
ERSL) |)(,, ,
,
zu
xvRyx
|)(),(,, ,
,
,
,
zu
yv
zu
xv RRyx ;
ERSR) ),(|, ,
,
zu
xvRyx
),(),(|, ,
,
,
,
zu
yv
zu
xv RRyx .
Достатню умову наявності кожного
з R|=TF, |=TF, |=T, |=F, |=IR індукує Rf:
СRfS) |= x x, .
6. Секвенційні числення чистих
першопорядкових логік
Секвенційні числення формалізу-
ють відношення логічного наслідку для
множин формул. Будуємо їх у стилі семан-
тичних таблиць. Ми трактуємо секвенції
як множини формул, специфікованих (від-
мічених) спеціальними символами |– та –| .
Позначаємо секвенції |––|, скорочено .
Секвенційні числення будуємо так:
секвенція |––| вивідна |= .
Формули із (відмічені |–) назвемо
T-формулами, а формули із (відмічені –|)
назвемо F-формулами. Це відповідає се-
мантичному трактуванню формул із як
істинних, а формул із – як хибних.
Формули вигляду |–x, –|x,
)(),( | | xRxR u
v
u
v назвемо T-форму-
лами, а вигляду –|x, |–x, ),(| xRu
v
)(| xRu
v – F-формулами.
Прикладами формул x, x,
)(),( xRxR u
v
u
v назвемо формули ви-
гляду )(),( ),(),( ,
,
,
, xu
yv
xu
yv
x
y
x
y RRRR .
Введемо для множини специфікова-
них формул = |––| множини означених
предметних імен та неозначених предмет-
них імен, або val-змінних та unv-змінних:
val(|––|) = {xV | Ex};
unv(|––|) = {xV | Ex}.
Введемо множину нерозподілених
для імен: ud() = nm() \ (val() unv()).
Виведення в секвенційних числен-
нях має вигляд дерева, вершинами якого є
секвенції. Такі дерева – секвенційні.
Секвенція – наступник секвенції
у секвенційному дереві з коренем ,
якщо в існує шлях = 1,…, n,…, m, …
такий, що = n та = m.
Секвенція вивідна, або має виве-
дення, якщо існує замкнене секвенційне
дерево з коренем – виведення .
Секвенційне дерево замкнене, якщо
кожний його лист – замкнена секвенція.
Секвенційне числення задається ба-
зовими секвенційними формами і умовами
замкненості секвенції. Замкнені секвенції є
аксіомами секвенційного числення.
Правилами виведення секвенційних
числень є секвенційні форми. Вони інду-
куються властивостями відношень логіч-
ного наслідку. Секвенційні форми запису-
ємо у вигляді
або
. Секвенції над
рискою – засновки (зіставлені правим час-
тинам відповідних властивостей відно-
шень логічного наслідку |=), під рискою –
висновки (зіставлені їх лівим частинам).
Умови замкненості секвенції |––|
із множиною unv-змінних Un обґрунтовує
теорема 8. Замкненість |––| означає |= .
Базова умова замкненості індукова-
на властивістю С.
С) існують формули та такі:
Un , та ;
зокрема, існує : та .
Властивості СL, СR, СLR індукують
додаткові умови СL, СR, СLR замкненості
секвенції |––|.
Теоретичні та методологічні основи програмування
15
СL) існують формули та такі:
Un , та ;
зокрема, існує : та ;
СR) існують формули та такі:
Un , та ;
зокрема, існує : та ;
СLR) існують формули , , , :
Un , Un , , та , ;
зокрема, існують формули та :
, та , .
Зрозуміло, що СLR СL та СR.
У випадку числень для |=IR умови
СL, СR, СLR зводяться до С.
Опишемо різновиди секвенційних
числень чистих першопорядкових КНЛ.
Розглянемо числення рівня ЧКНЛ.
Числення QG формалізує R|=TF.
Умова замкненості секвенції: C.
Числення QLR формалізує |=TF. Умо-
ва замкненості секвенції: C CLR.
Числення QL формалізує |=T. Умова
замкненості секвенції: C CL.
Числення QR формалізує |=F. Умова
замкненості секвенції: C CR.
Числення QC формалізує |=IR. Умо-
ва замкненості секвенції: C.
На рівні ЧКНЛР маємо лише відно-
шення |=IR, його формалізує числення QCE.
Умова замкненості секвенції така: C CRf.
Умова CRf індукована властивістю CRf :
CRf) секвенція |––| замкнена, як-
що x = x для деякого xV.
Для числень рівня ЧКНЛРС маємо
додаткову умову CRfS замкненості сек-
венції, індуковану властивістю CRfS :
CRfS) секвенція |––| замкнена,
якщо x x для деякого xV.
Для ЧКНЛРС маємо такі числення.
Числення QEG формалізує R|=TF.
Умова замкненості секвенції: C CRfS.
QELR формалізує |=TF. Умова замк-
неності секвенції: C CLR CRfS.
QEL формалізує |=T. Умова замкне-
ності секвенції: C CL CRfS.
QER формалізує |=F. Умова замкне-
ності секвенції: C CR CRfS.
QEC формалізує |=IR. Умова замкне-
ності секвенції: C CRfS.
Числення QEG, QELR, QEL, QER ма-
ють однакові базові секвенційні форми.
Форми cпрощення формул:
|–R
),(
,
|
|
R
; –|R
),(
,
|
|
R
;
|–R
),(
,
|
|
R
; –|R
),(
,
|
|
R
;
|–RI
),(
),(
,
,|
|
vz
xz
v
x
R
R
; –|RI
),(
),(
,
,|
|
vz
xz
v
x
R
R
;
|–RI
),(
),(
,
,|
|
vz
xz
v
x
R
R
; –|RI
),(
),(
,
,|
|
vz
xz
v
x
R
R
;
|–RU
),(
),(
,
,|
|
vy
uz
v
u
R
R
; –|RU
),(
),(
,
,|
|
vy
uz
v
u
R
R
;
|–RU
),(
),(
,
,|
|
vy
uz
v
u
R
R
; –|RU
),(
),(
,
,|
|
vy
uz
v
u
R
R
.
Для форм типу RU умова: у().
Форми еквівалентних перетворень:
|–RR
)),((
),(
|
|
w
y
v
x
w
y
v
x
RR
R
; –|RR
)),((
),(
|
|
w
y
v
x
w
y
v
x
RR
R
;
|–RR
)),((
),(
|
|
w
y
v
x
w
y
v
x
RR
R
;
–|RR
)),((
),(
|
|
w
y
v
x
w
y
v
x
RR
R
;
|–R
),(
),(
|
|
v
x
v
x
R
R
; –|R
),(
),(
|
|
v
x
v
x
R
R
;
|–R
),(
),(
|
|
v
x
v
x
R
R
; –|R
),(
),(
|
|
v
x
v
x
R
R
;
|–R
),(
),()(
|
|
v
x
v
x
v
x
R
RR
;
Теоретичні та методологічні основи програмування
16
–|R
),(
),()(
|
|
v
x
v
x
v
x
R
RR
;
|–R
),(
)),()((
|
|
v
x
v
x
v
x
R
RR
;
–|R
),(
)),()((
|
|
v
x
v
x
v
x
R
RR
.
Форми декомпозиції формул:
|
,
,
|
|
; |
,
,
|
|
;
|
,
, ,
|
||
; |
,
, ,
|
||
;
|
),(
,,
|
| |
; | .
),(
, ,
|
||
Форми елімінації кванторів:
|
,
,),(
|
| |
x
EzRx
z
;
|
,
,),(
|
| |
x
EzRx
z
;
|–R
),(
,),(
|
|
,
,|
xR
EzR
u
v
xu
zv
;
–|R
),(
,),(
|
|
,
,|
xR
EzR
u
v
xu
zv
;
|v
,,
),(,,
| |
| | |
Eyx
REyx x
y
;
|v
,,
),(,,
| |
| | |
Eyx
REyx x
y
;
|–Rv
,),(
,),(),(
| |
|
,
,| |
EyxR
EyRxR
u
v
xu
yv
u
v
;
–|Rv
,),(
,),(),(
| |
|
,
,| |
EyxR
EyRxR
u
v
xu
yv
u
v
.
Для |–, –| умова: zfu(, x);
для |–R, –|R умова: zfu(, ))( xRu
v .
Форми |–R, –|R, |–, –| назвемо
T-формами. –|v, |–v, –|Rv, |–Rv – це
форми типу v, назвемо їх F-формами;
для цих форм Ey не входить до .
Форми E-розподілу Ed та первісно-
го означення Ev:
, ,
Ed
|| ExEx
;
,
Ev
| Ez
за умови zfu().
Базові форми для строгої рівності:
|–ЕS
,
,
|
|
yx
yx
; –|ЕS
,
,
|
|
yx
yx
;
ЕSmS
,
, ,
|
||
yx
xyyx
;
ЕTrS
, ,
, , ,
||
|||
zyyx
zxzyyx
;
|–RDS
),(
,
,,
,,|
|
yxR
uz
yxu
uzv
;
),(
,
,
,|
|
yxR
yz
xu
zv
, де { }y u ;
),(
,
|
|
yxR
yx
u
v
, }{, де uyx ;
–|RDS
),(
,
,,
,,|
|
yxR
uz
yxu
uzv
;
),(
,
,
,|
|
yxR
yz
xu
zv
, де { }y u ;
),(
,
|
|
yxR
yx
u
v
, де , { }x y u ;
|–RDS
),(
,
,,
,,|
|
yxR
uz
yxu
uzv
;
),(
,
,
,|
|
yxR
yz
xu
zv
, де { }y u ;
Теоретичні та методологічні основи програмування
17
),(
,
|
|
yxR
yx
u
v
, де , { }x y u ;
–|RDS
),(
,
,,
,,|
|
yxR
uz
yxu
uzv
;
),(
,
,
,|
|
yxR
yz
xu
zv
, де { }y u ;
),(
,
|
|
yxR
yx
u
v
, де , { }x y u ;
|–ЕRS
),(,
),(),(,
,
,| |
,
,|
,
,| |
pRyx
pRpRyx
zu
xv
zu
yv
zu
xv
;
–|ЕRS
),(,
),(),(,
,
,| |
,
,|
,
,| |
pRyx
pRpRyx
zu
xv
zu
yv
zu
xv
;
|–ЕRS
),(,
),(),(,
,
,| |
,
,|
,
,| |
pRyx
pRpRyx
zu
xv
zu
yv
zu
xv
;
–|ЕRS
),(,
),(),(,
,
,| |
,
,|
,
,| |
pRyx
pRpRyx
zu
xv
zu
yv
zu
xv
.
Для форм типу ЕRS умова: pPs.
Маємо різновиди базових форм: до-
поміжні (типів R, RІ, RU, RR, RDS); фор-
ми E-розподілу та первісного означення
(Ed та Ev); спеціальні форми рівності
(ЕSmS, ЕTrS та форми типів ЕRS); основнi
– це всі інші базові секвенційні форми.
В численнях QEC форми для зовні-
шнього заперечення зайві, базовими сек-
венційні форми – це |–R, –|R, |–RI, –|RI,
|–RU, –|RU, |–RR, –|RR, |–RR, –|RR, |–R,
–|R, |–R, –|R, |, |, |, |–R, |v,
–|Rv, до яких додаємо форми для рівності
ЕSmS, ЕTrS, |–RDS, –|RDS, |–ЕRS, –|ЕRS та
форми:
|
,
,
|
|
; |
,
,
|
|
.
В численнях QCE базовими секвен-
ційними формами є |–R, –|R, |–RI, –|RI, |–RU,
–|RU, |–RR, –|RR, |–RR,–|RR, |–R, –|R,
|–R, –|R, |, |, |, |, |, |–R, |v,
–|Rv, до яких додаємо:
ЕSm
,
, ,
|
||
yx
xyyx
;
ЕTr
, ,
, , ,
||
|||
zyyx
zxzyyx
;
|–RD
),(
,
,,
,,|
|
yxR
uz
yxu
uzv
;
),(
,
,
,|
|
yxR
yz
xu
zv
, де { }y u ;
),(
,
|
|
yxR
yx
u
v
, де , { }x y u ;
–|RD
),(
,
,,
,,|
|
yxR
uz
yxu
uzv
;
),(
,
,
,|
|
yxR
yz
xu
zv
, де { }y u ;
),(
,
|
|
yxR
yx
u
v
, де , { }x y u ;
|–ЕR
),(,
),(),(,
,
,| |
,
,|
,
,| |
pRyx
pRpRyx
zu
xv
zu
yv
zu
xv
, pPs;
–|ЕR
),(,
),(),(,
,
,| |
,
,|
,
,| |
pRyx
pRpRyx
zu
xv
zu
yv
zu
xv
, pPs.
Базові секвенційні форми числень
QG, QLR, QL, QR однакові, це наведені
вище форми числень QEG, QELR, QEL, QER
з вилученими формами для рівності.
Базові секвенційні форми числення
QC – це форми числень QEC та QEC з ви-
лученими формами для рівності.
Властивості відношень логічного
наслідку для множин формул індукують
основну властивість секвенційних форм (|=
– одне з R|=TF, |=TF, |=T, |=F, |=IR).
Теорема 9.
1. Нехай
||
||
– базова секвен-
ційна форма. Тоді:
a) |= |= ; b) | | .
Теоретичні та методологічні основи програмування
18
2. Нехай
| | | |
| |
– базова
секвенційна форма. Тоді:
a) |= та |= |= ;
b) | | або | .
7. Побудова секвенційного дерева
Опишемо побудову виведення для
заданої скінченної секвенції .
При побудові секвенційні форми за-
стосовуються від висновку до засновків, тоб-
то ми спрощуємо виділену формулу чи роз-
кладаємо її на компоненти.
Секвенції – це множини специфіко-
ваних формул, тому повтори формул у
секвенціях неможливі: якщо в результаті
виконання форми отримуємо специфіко-
вану формулу, яка вже є в секвенції, цю
формулу-копію до секвенції не заносимо.
Cпецифіковані формули вигляду
|–Ex та –|Ex індукуються формами елімінації
кванторів, а також формами E-розподілу та
первісного означення, тому вони відсутні в
початковій секвенції-корені .
Побудова секвенційного дерева роз-
бита на етапи. Вона починається з кореня
дерева. Опишемо етап виведення для пев-
ної незамкненої листа-секвенції .
Нехай – множина формул секвен-
цій на шляху від кореня до даної . Як-
що val() = , не має T-формул та має
F-формули, то виконуємо первісне озна-
чення: збагачуємо секвенцію формулою
|–Ez такою, що zfu(), тобто ми переходи-
мо до секвенції , |–Ez. Це дає непорожність
множини означених імен для кожної вер-
шини-секвенції, яка є наступником , що
надалі гарантує застосовність F-форм.
Далі добудовуємо скінченне підде-
рево з вершиною . Активізуємо (окрім
примітивних) формули секвенції . До ко-
жної активної формули далі застосовуємо
відповідну форму. В процесі застосування
основних форм кожен раз при появі відпо-
відної ситуації виконуємо спрощення, за-
стосовуючи належні допоміжні форми ти-
пів R, RI, RU, RR. Після застосування ос-
новної форми і виконання спрощень ут-
ворені нею формули на даному етапі па-
сивні, до цих формул на цьому етапі основ-
ні секвенційні форми не застосовуються.
Застосування форм рівності в чис-
леннях ЧКНЛР і ЧКНЛРС має особливості.
Форми типу RDS (RD для QCE) до-
поміжні. Форми ЕSmS (ЕSm для QCE) ви-
конуємо кожен раз при появі нової для сек-
венції формули вигляду |–x y (чи |–x = y).
Форми ЕTrS (ЕTr для QCE) викону-
ємо кожен раз при появі пари формул вигля-
ду |–x y та |–y z (вигляду |–x = y та |–y = z),
принаймі одна з яких нова для секвенції.
Форми типу ЕR виконуємо кожен
раз при появі пари формул, одна з яких –
|–x = y, а друга – вигляду )(,
,| pR zu
xv чи
),(,
,| pR zu
xv причому принаймі одна з них но-
ва для секвенції. Форми типу ЕRS виконує-
мо кожен раз при появі пари формул, одна з
яких |–x y, а друга – вигляду ),(,
,| pR zu
xv
),(,
,| pR zu
xv ),(),( ,
,|
,
,| pRpR zu
xv
zu
xv причому
принаймі одна з них нова для секвенції.
Застосування на етапі основних
секвенційних форм проводимо так.
Спочатку виконуємо 1-засновкові
форми, окрім F-форм. При кожному засто-
суванні T беремо нове zVT, яке відсутнє
на шляху від кореня до секвенції, в якій
виконуємо цю T-форму. При цьому усі
застосування T-форми до одної і тої ж T-
формули в секвенціях-наступниках ви-
користовують одне і те ж нове zVT. Мно-
жину усіх нових zVT, використаних при
застосуванні T-форм до T-формул сек-
венції , позначимо vt.
Нехай в є l активних формул, до
яких треба застосувати 2-засновкову фор-
му | чи |. Застосування | чи | ве-
де до побудови для піддерева, що має
n = 2l листів-наступників . Застосування
кожної з форм, окрім F-форм, до активних
формул секвенції не залежить від ре-
зультатів застосування кожної з інших цих
форм. Отже, із при застосуванні таких
форм отримуємо одну і ту ж множину ли-
стів-наступників {1,…, n} незалежно від
порядку виконання цих форм.
Якщо секвенція має активні F-
Теоретичні та методологічні основи програмування
19
формули (це якраз активні F-формули
кожної з секвенцій 1,…, n), то до них
треба застосувати відповідні F-форми.
Нехай , 1,…, n – множини фор-
мул секвенцій на шляхах від до
, 1,…, n. Тоді nm(k) = nm()vt,
val(k) = val() та ud(k) = ud() для кож-
ної k. Позначимо ud() як ud. Якщо
ud , то в 1,…, n маємо нерозподілені
імена. Тому перед застосуванням F-форм
в кожній k спочатку робимо, використо-
вуючи Ed-форму, всеможливі розподіли
імен із ud на означені та неозначені. Це
веде до побудови піддерев висоти h = |ud|
з вершинами k, що дає m = 2h наступників
кожної k – це секвенції 11,…, 1m,…,
n1,…, nm з множинами vdj ud нових
означених імен в секвенціях 1j,…, nj .
Кожна з секвенцій kj має ті ж активні F-
формули, що й секвенція . До цих F-
формул застосовуємо відповідні F-форми,
кожна така форма в kj виконується бага-
тократно для кожного уvdj val(). В
результаті маємо секвенції 11,…, 1m, …,
n1,…, nm . Незалежно від порядку вико-
нання цих F-форм із кожної секвенції kj
буде отримана одна і та ж секвенція kj .
Таким чином, за умови, що вико-
нання T-форм передує виконанню F-
форм, результатом виконання етапу для
секвенції є одна і та ж множина секве-
нцій-наступників {11,…, 1m,…, n1,…, nm}
незалежно від порядку виконання цих
форм. У цьому розумінні побудова сек-
венційного дерева однозначна.
Для того, щоб отримана на етапі
множина секвенцій-наступників даної сек-
венції визначалась однозначно, істотним є
лише порядок виконання T-форм та F-
форм. Стосовно отримання замкненого се-
квенційного дерева чи отримання незамк-
неного шляху, то цей порядок неістотний.
Справді, нехай на етапі після виконання де-
яких F-форм виконуємо T-форму, яка
вводить нове zVT. Тоді продуковані цими
F-формами приклади із таким z обов’яз-
ково з’являться на наступному етапі.
Після виконання усіх форм на етапі
перевіряємо кожну секвенцію-лист на
замкненість. Якщо незамкнена, то пере-
віряємо, чи буде фінальною секвенцією.
Незамкнена вершина-секвенція
виведення секвенції – фінальна, якщо до
неї вже незастосовна жодна секвенційна
форма, або якщо кожне застосування сек-
венційної форми до не вводить нових
формул, відмінних від формул секвенцій
на шляху від до . Поява фінальної сек-
венції означає ситуацію повторення неза-
мкненої секвенції на даному шляху. Це си-
гналізує про наявність в дереві шляху (від
кореня до даної фінальної секвенції), всі
вершини якого незамкнені – незамкненого
шляху. Його поява засвідчує, що побудова
виведення завершена негативно.
Якщо всі листи будованого дерева
замкнені, то отримано замкнене секвенцій-
не дерево, побудова завершена позитивно.
Якщо побудова не завершується,
маємо нескінченне дерево. За лемою Кені-
га нескінченне дерево зі скінченним розга-
луженням має хоча б один нескінченний
шлях. Всі його вершини – незамкнені сек-
венції, такий шлях незамкнений.
Подібним чином проводимо поета-
пну побудову виведення для зліченної сек-
венції. Особливістю побудови є те, що ко-
жне застосування секвенційної форми про-
водимо до скінченної множини доступних
на даний момент формул (див., напр.,
[2, 9]). На початку побудови доступна ли-
ше пара перших формул списків T-формул
та F-формул секвенції (єдина T-формула
чи F-формула, якщо один зі списків поро-
жній). На початку кожного етапу в усіх не-
замкнених секвенціях виконуємо крок дос-
тупу: до списку доступних формул секвен-
ції додаємо по одній формулі з її списків T-
формул та F-формул. Далі діємо так, як
описано вище. При побудові дерева для
зліченної секвенції втрачає сенс поняття
фінальної секвенції та можливі лише два
варіанти: побудова завершена позитивно із
отриманням скінченного замкненого дере-
ва, або побудова не завершується, тоді ма-
ємо нескінченне незамкнене дерево, в яко-
му існує незамкнений шлях. Кожна з фор-
мул початкової секвенції зустрінеться на
цьому шляху і стане доступною.
Теоретичні та методологічні основи програмування
20
Для кожного з побудованих секвен-
ційних числень чистих першопорядкових
КНЛ, що формалізує відповідне відношен-
ня логічного наслідку, справджується
Теорема 10 (коректності). Нехай
секвенція |––| вивідна. Тоді |= .
Якщо |––| вивідна, то для неї по-
будоване замкнене секвенційне дерево.
Для кожної його вершини |––| маємо
|= . Для листів дерева це випливає з ви-
значення замкненої секвенції. Збереження
секвенційними формами відношення логі-
чного наслідку (від засновків до висновку)
випливає з теореми 8. Тому для кореня де-
рева – секвенції |––| – теж маємо |= .
8. Теореми про контрмоделі.
Теореми повноти
Доведення повноти секвенційних
числень опирається на теореми про існу-
вання контрмоделей для незамкненого
шляху в секвенційному дереві, для цього
використовуємо метод модельних множин.
Розглянемо тут теореми про контрмоделі
для числень ЧКНЛРС та ЧКНЛР. Дове-
дення цих теорем подібне до доведення в
[9] відповідних теорем для числень ЧКНЛ.
Теорема про контрмоделі для QEG.
Теорема 11. Нехай – незамкне-
ний шлях у секвенційному дереві, збудо-
ваному для секвенції |––|, нехай Н –
множина всіх специфікованих формул
секвенцій цього шляху. Тоді існують ін-
терпретації A = (A, I1), B = (A, I2) та
, VA такі:
НT) |–Н T(A), –|Н T(A);
НF) |–Н F(B), –|Н F(B).
Пари (A, ) і (B, ) назвемо T-контр-
моделлю i F-контрмоделлю для |––|.
Доведення. Застосування секвенцій-
них форм до секвенцій шляху відбува-
ється до тих пір, поки це можливо, тому
кожна непримітивна формула чи її запере-
чення, що зустрічається на шляху , рано
чи пізно буде розкладена чи спрощена.
Усі секвенції шляху незамкнені,
тому для них не виконується умова за-
мкненості C CRfS. Отже, для множини Н
виконуються такі умови коректності:
НС) не існують , такі: Un ,
|–Н та –|Н;
НCRfS) не існує xV: |–x x Н.
Переходи від нижчої вершини шля-
ху до вищої відбуваються згідно з
певною секвенційною формою, тому для
Н виконуються відповідні умови перехо-
ду. Для секвенційних форм числень
ЧКНЛ такі умови наведено в [9] (позна-
чення для деяких – відмінні від наведених
тут). Наведемо для прикладу умови НR,
НRR, Н, НR та пов’язані з предика-
тами рівності умови НЕS, НЕSmS,
НRDS, НЕRS.
НR) | |( ) R H H ;
| |( ) R H H ;
НRR) HxR xu
yv )(,
,| HxRu
v )(| ;
HxR xu
yv )(,
,| HxRu
v )(| ;
Н) |–хН існує уW: HRx
y )(| ;
–|хН HRx
y )(| для всіх уW;
НR) HxRu
v )(| HR xu
yv )(,
,|
для всіх уW;
HxRu
v )(| існує уW: HR xu
yv )(,
,| ;
НЕS) |–x y Н –|x y Н;
–|x y Н |– x y Н;
НЕSmS) |–x y Н |–y x Н;
НЕTrS) |–x y Н та |–y z Н |–x z Н;
НRDS) HuzHyxR
yxu
uzv |
,,
,,| )( ;
; )( |
,,
,,| HuzHyxR
yxu
uzv
; }{ де ),( |
,
,| HyzuyyxR xu
zv
; }{ де ),( |
,
,| HyzuyyxR xu
zv
; }{, де ),( || HyxuyxyxRu
v
; }{, де ),( || HyxuyxyxRu
v
НЕRS) )(, ,
,| | HpRHyx zu
xv
Теоретичні та методологічні основи програмування
21
;)(,)(, ,
,|
,
,|| HpRHpRHyx zu
yv
zu
xv
)(, ,
,| | HpRHyx zu
xv
.)(,)(, ,
,|
,
,| | HpRHpRHyx zu
yv
zu
xv
Mножинy специфікованих формул
Н, для якої виконуються такі умови корек-
тності та переходу, назвемо GES-модель-
ною.
Побудуємо контрмодель за цією Н.
Нехай W = nm(Н) – множина всіх
предметних імен, що фігурують у Н. Пре-
дикати рівності індукують на W відношен-
ня еквівалентності: x y |– x yН.
Нехай А =
~
W – фактор-множина
множини W за відношенням ~. Нехай v –
клас еквівалентності з представником v.
Визначимо = [vv | vW ]. Таке
відображення є сюр'єкцією WА.
Задамо значення базових предикатів
на та ІМ вигляду )(r v
x :
– якщо |– x yН, то (x y)А() = T;
– якщо –| x yН, то (x y)А() = F;
– |– рН T(рA) та F(рB);
– –| рН T(рA) та F(рB);
– |–рН T(pA) та F(pB);
– –|pН T(pA) та F(pB);
– HpRv
x )(|
)()(r A
v
x pT та );()(r B
v
x pF
– HpRv
x )(|
)()(r A
v
x pT та );()(r B
v
x pF
– HpRv
x )(|
)()(r A
v
x pT та );()(r B
v
x pF
– HpRv
x )(|
)()(r A
v
x pT та ).()(r B
v
x pF
Для атомарних формул і формул ви-
гляду )( pRv
x твердження теореми випливає
з визначення базових предикатів. Далі до-
водимо індукцією за складністю формули
згідно з пунктами визначення Н.
Теореми про контрмоделі для чис-
лень QELR, QEL, QER, QEС формулюються
та доводяться подібно до теореми 11.
Теорема 12. За умов теореми 11 іс-
нують інтерпретація A = (A, I) та VA такі:
НT
S) |–Н A() = T,
–|Н A() T;
НF
S) |–Н B() F,
–|Н B() = F.
Пари (A, ) і (B, ) назвемо TS-контр-
моделлю i FS-контрмоделлю для |––|.
Теорема 13. За умов теореми 11 іс-
нують інтерпретація A = (A, I) та VA такі:
НT
S) |–Н A() = T,
–|Н A() T.
Теорема 14. За умов теореми 11 іс-
нують інтерпретація A = (A, I) та VA такі:
НF
S) |–Н B() F,
–|Н B() = F.
Теорема 15. За умов теореми 11 іс-
нують інтерпретація A = (A, I) та VA такі:
НС) |–Н A() = T,
–|Н A() = F.
Пару (A, ) назвемо IR-контрмодел-
лю для секвенції |––|.
В формулюваннях теорем 12–15
враховано, що числення QELR, QEL, QER,
QEС формалізують відношення в P-семан-
тиці, тому зазначені там предикати A та
B мають бути однозначними.
Для числення QСE теорема про
контрмоделі формулюється аналогічно.
На основі теорем про контрмоделі
для кожного з пропонованих секвенційних
числень, що формалізує відповідне відно-
шення логічного наслідку, отримуємо тео-
реми повноти. Теореми повноти формулю-
ються однотипно для всіх цих числень:
Теорема 16 (повноти). Нехай |= .
Тоді секвенція |––| вивідна.
Наведемо для прикладу доведення
для R|=TF і числення QEG. та для |=IR і чис-
лення QEC (числення RCE). Подібні дове-
дення теорем повноти див. [9].
Теоретичні та методологічні основи програмування
22
Доведення для R|=TF та QEG. Нехай
супротивне:
R|=TF та |––| невивідна,
тоді секвенційне дерево для |––| незамк-
нене. Отже, в цьому дереві існує незамк-
нений шлях. Нехай Н – множина всіх спе-
цифікованих формул секвенцій цього шля-
ху. За теоремою 11 існують T-контрмодель
(A, ) та F-контрмодель (B, ) такі:
|–Н T(A) та –|Н T(A);
|–Н F(B) та –|Н F(B).
Для T-контрмоделі згідно |––| Н
для всіх маємо T(A), для всіх
Ψ маємо T(ΨA). Звідси T(A) та
T(A), тому неправильно T(A) T(A).
Це заперечує A|=T , тому й заперечує
R|=TF .
Для F-контрмоделі згідно |––| Н
для всіх маємо F(B), для всіх
Ψ маємо F(ΨB). Звідси F(B) та
F(B), тому неправильно F(B) F(B).
Це заперечує B|=F та заперечує
R|=TF .
Доведення для |=IR та QEC і QCE.
Нехай супротивне: |=IR та |––| неви-
відна. Тоді секвенційне дерево для |––|
незамкнене. Отже, в існує незамкнений
шлях. Нехай Н – множина всіх спе-
цифікованих формул секвенцій цього шля-
ху. За теоремою 15 існує IR-контрмодель
(А, ): |–Н А() = Т та –|Н
А() = F. Згідно з |––| Н тоді для всіх
маємо А() = Т та для всіх Ψ ма-
ємо ΨА() = F. Це суперечить |=IR .
Висновки
В роботі вивчаються програмно-орі-
єнтовані логічні формалізми – чистi пер-
шопорядковi композиційно-номінативні
логіки квазіарних предикатів з предиката-
ми рівності. Виділено різновиди квазіар-
них предикатів, описано композиційні
предикатні алгебри чистих першопорядко-
вих логік. Розглянуто логіки з предикатами
слабкої рівності та з предикатами строгої
рівності, наведено властивості, пов’язані з
цими предикатами. Описано мови чистих
першопорядкових композиційно-номіна-
тивних логік та їх інтерпретації. Виділено
класи інтерпретацій (семантики) часткових
неоднозначних, часткових однозначних,
тотальних неоднозначних та тотальних
однозначних предикатів. Досліджено се-
мантичні властивості пропонованих логік,
особлива увага приділена відношенням
логічного наслідку для множин формул.
На базі властивостей цих відношень для
чистих першопорядкових логік з предика-
тами рівності запропоновано низку чис-
лень секвенційного типу. Наведено умови
замкненості секвенції та базові секвенційні
форми цих числень, описано побудову ви-
ведення (секвенційного дерева). Для про-
понованих числень доведено теореми ко-
ректності та повноти. Доведення повноти
опирається на теореми про побудову
контрмоделей за незамкненим шляхом в
секвенційному дереві.
1. Handbook of Logic in Computer Science. Ed-
ited 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 Proper-
ties of Logics of Quasiary Predicates. Work-
shop on Foundations of Informatics: Proceed-
ings FOI-2015. Chisinau, Moldova.
P. 180–197.
5. Нікітченко М.С., Шкільняк О.С., Шкільняк
С.С. Чисті першопорядкові логіки квазіа-
рних предикатів. Проблеми програмування.
2016. № 2–3. C. 73–86.
6. Шкільняк С.С., Волковицький Д.Б. Реномі-
нативні композиційно-номінативні логіки з
предикатами рівності. Вісник Київського
національного університету імені Тараса
Шевченка. Сер.: фіз.-мат. науки. 2014.
Вип. 3. C. 198–205.
7. Шкільняк С.С., Волковицький Д.Б. Реномі-
нативні логіки квазіарних предикатів.
Компьютерная математика. 2016. Вып. 1.
C. 46–57.
8. Шкільняк О.С. Відношення логічного на-
слідку в логіках монотонних предикатів тa
Теоретичні та методологічні основи програмування
23
логіках антитонних предикатів. Проблеми
програмування. 2017. № 1. C. 21–29.
9. Шкільняк С.С. Спектр секвенційних чис-
лень першопорядкових композиційно-
номінативних логік. Проблеми програму-
вання. 2013. № 3. C. 22–37.
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.
(2015). Semantic Properties of Logics of
Quasiary Predicates. In Workshop on
Foundations of Informatics: Proceedings FOI-
2015. Chisinau, Moldova. P. 180–197.
5. NIKITCHENKO M. and SHKILNIAK S.
(2016). Pure first-order logics of quasiary
predicates. In Problems in Progamming.
N 2–3. P. 73–86 (in ukr).
6. SHKILNIAK S. and VOLKOVYTSKYI D.
(2014). Renominative composition-
nominative logics with predicates of equality.
In Bulletin of Taras Shevchenko National
University of Kyiv. Series: Physics &
Mathematics. N 3. P. 198–205 (in ukr).
7. SHKILNIAK S. and VOLKOVYTSKYI D.
(2016). Renominative logics of quasiary
predicates. In Computer mathematics. 1.
P. 46–57 (in ukr).
8. SHKILNIAK О. (2017). Logical consequence
relations in logics of monotone predicates and
logics of antitone predicates. In Problems in
Progamming. N 1. P. 21–29 (in ukr).
9. SHKILNIAK S. (2013). Spectrum of sequent
calculi of first-order composition-nominative
logics. In Problems in Progamming. N 3,
P. 22–37 (in ukr).
Одержано 24.04.2017
Про авторів:
Нікітченко Микола Степанович,
доктор фізико-математичних наук,
професор, завідувач кафедри Теорії
та технології програмування.
Кількість наукових публікацій в
українських виданнях – понад 200,
у тому числі у фахових виданнях – 100.
Кількість наукових публікацій в
зарубіжних виданнях – 30.
Scopus Author ID: 6602842336.
H-індекс (Google Scholar): 9 (7 з 2012).
http://orcid.org/0000-0002-4078-1062.
Шкільняк Степан Степанович,
доктор фізико-математичних наук,
професор, професор кафедри Теорії
та технології програмування.
Кількість наукових публікацій в
українських виданнях – понад 200,
у тому числі у фахових виданнях – 100.
Кількість наукових публікацій в
зарубіжних виданнях – 15.
H-індекс (Google Scholar): 4 (3 з 2010).
http://orcid.org/0000-0001-8624-5778.
Місце роботи авторів:
Київський національний університет
імені Тараса Шевченка,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 259 0519, (044) 522 0640 (д).
E-mail: nikitchenko@unicyb.kiev.ua,
sssh@unicyb.kiev.ua.
|