Logics of quasiary predicates of quantifier-equational level
First-order composition-nominative logics of partial single-valued, total multiple valued and partial multiple-valued quasiary predicates of quantifierequational level are studied. We define basic semantic properties of the introduced logics, particularly the properties of the relations of logical c...
Gespeichert in:
| Datum: | 2015 |
|---|---|
| Hauptverfasser: | , |
| Format: | Artikel |
| Sprache: | Ukrainisch |
| Veröffentlicht: |
PROBLEMS IN PROGRAMMING
2015
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/104 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Institution
Problems in programming| _version_ | 1859475646819860480 |
|---|---|
| author | Nikitchenko, M.S. Shkilniak, S.S. |
| author_facet | Nikitchenko, M.S. Shkilniak, S.S. |
| author_sort | Nikitchenko, M.S. |
| baseUrl_str | https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| collection | OJS |
| datestamp_date | 2018-10-02T21:09:26Z |
| description | First-order composition-nominative logics of partial single-valued, total multiple valued and partial multiple-valued quasiary predicates of quantifierequational level are studied. We define basic semantic properties of the introduced logics, particularly the properties of the relations of logical consequence for sets of formulas and the Х–Y-valued relations of logical consequence. On this basis we construct sequent calculi for logics of single-valued quasi-ary predicates of quantifier-equational level. |
| first_indexed | 2025-07-17T09:32:50Z |
| format | Article |
| fulltext |
Теоретичні та методологічні основи програмування
© М.С. Нікітченко, C.С. Шкільняк, 2012
ISSN 1727-4907. Проблеми програмування. 2012. № 4 19
УДК 004.42:510.69
М.С. Нікітченко, С.С. Шкільняк
ЛОГІКИ КВАЗІАРНИХ ПРЕДИКАТІВ КВАНТОРНО-
ЕКВАЦІЙНОГО РІВНЯ
Досліджено першопорядкові композиційно-номінативні логіки часткових однозначних, тотальних не-
однозначних та часткових неоднозначних квазіарних предикатів кванторно-екваційного рівня. Наведе-
но основні семантичні властивості таких логік, зокрема, властивості відношень логічного наслідку для
множин формул, Х–Y-означених відношень логічного наслідку. На цій основі для логік однозначних ква-
зіарних предикатів кванторно-екваційного рівня побудовано числення секвенційного типу.
Вступ
Розвиток інформаційних технологій
та програмування зумовлює розширення
сфери застосування математичної логіки.
На даний момент розроблено багато різ-
номанітних логічних систем (див., напр.,
[1]), які доводять свою ефективність при
розв'язанні широкого кола задач інформа-
тики й програмування. В основі таких си-
стем, як правило, лежить класична логіка
предикатів [2]. Ця логіка добре дослідже-
на, вона має багатий досвід застосування,
на її основі будуються спеціальні логіки,
орієнтовані на вирішення тих чи інших
конкретних задач. Водночас поява нових
застосувань логіки в інформатиці та програ-
муванні висвітила принципові обмеження
класичної логіки предикатів, які ускладню-
ють її використання. Така логіка базується
на традиційних математичних структурах
однозначних тотальних скінченно-арних
відображень, вона недостатньо враховує
неповноту, частковість інформації про
предметну область, її структурованість.
Обмеження класичної логіки виводять на
перший план проблему побудови нових,
програмно-орієнтованих логічних форма-
лізмів на спільній для логіки і програму-
вання основі. За таку основу природно взя-
ти композиційно-номінативний підхід [3]
до побудови моделей програм і орієнтова-
них на них логік. На базі цього підходу ро-
зроблено [4] низку різноманітних логічних
систем, що знаходяться на різних рівнях
абстрактності та загальності. Логіки, збу-
довані на основі композиційно-номіна-
тивного підходу, названо композиційно-
номінативними.
Передумовою виникнення компо-
зиційно-номінативних логік (КНЛ) стала
необхідність посилення можливостей кла-
сичної логіки для розв'язання нових задач
інформатики й програмування. КНЛ базу-
ються на загальних класах часткових відо-
бражень, заданих на довільних наборах
іменованих значень. Такі відображення на-
звано квазіарними.
Метою даної роботи є дослідження
першопорядкових композиційно-номінати-
вних логік часткових однозначних, тота-
льних неоднозначних та часткових неод-
нозначних квазіарних предикатів квантор-
но-екваційного рівня. В роботі описано
мови і семантичні моделі таких логік, роз-
глянуто різні формалізації відношення ло-
гічного наслідку. Досліджено властивості
цих відношень в різних семантиках. На цій
основі для КНЛ однозначних квазіарних
предикатів кванторно-екваційного рівня
побудовано числення секвенційного типу.
Логіка тотальних однозначних пре-
дикатів – це класична логіка. Логіки одно-
значних часткових предикатів названі ло-
гіками з неокласичною семантикою, логіки
тотальних неоднозначних предикатів – ло-
гіками з пересиченою семантикою, логіки
часткових неоднозначних предикатів при-
родно назвати логіками із загальною се-
мантикою. Такі нестандартні семантики
для пропозиційної логіки та різноманітні
відношення логічного наслідку вивчались
О.Д. Смирновою [5]. В роботі [6] подібні
семантики та формалізації відношення ло-
гічного наслідку узагальнені на випадок
КНЛ реномінативного та кванторного рів-
Теоретичні та методологічні основи програмування
нів, подальші дослідження таких логік
проведені, зокрема, в [7–10].
Поняття, які тут не визначаються,
тлумачимо в сенсі робіт [4, 6–8].
1. Композиції та композиційні
системи квазіарних предикатів
Згідно композиційно-номінативного
підходу (КНП), композиційно-номінативні
логіки будуємо за семантико-синтаксич-
ною схемою. Це означає, що спочатку
задаємо інтенсіональні (змістовні) моделі
логік. Такі моделі найперше визначаються
рівнями розгляду даних, тому для їх задан-
ня фіксуємо рівень абстракції розгляду.
Інтенсіональні моделі індукують мову
логіки. Далі будуємо відповідні розгля-
нутому рівню екстенсіональні моделі, які
задають семантичні аспекти логік. Такими
моделями є предикатні композиційні
системи – трійки вигляду (D, Pr, C), де D –
множина (клас) даних, Pr – множина
(клас) предикатів, заданих на D, C –
множина (клас) композицій (операцій)
породження нових предикатів, вона
задається множиною базових композицій
відповідного рівня. Предикатна
композиційна система задає дві алгебри:
алгебру (алгебраїчну систему) даних
(D, Pr) та алгебру предикатів (Pr, C),
терми якої трактуються як формули мови
логіки. Нарешті, будуємо формально-аксі-
оматичні логічні числення, які задають
синтаксичні аспекти логік. Основними їх
різновидностями є формальні системи
гільбертівського типу та системи ґенценів-
ського типу (секвенційні числення).
Основним семантичним поняттям
логіки є поняття предиката.
В загальному випадку під предика-
том на множині D будемо розуміти дові-
льну (часткову неоднозначну, взагалі ка-
жучи), функцію вигляду P : D → {T, F}, де
{T, F} – множина істиннісних значень.
Областю істинності та областю хи-
бності предиката Р на D назвемо множини:
T(P) = PP
–1(T) = {d∈D | T∈P(d)};
F(P) = PP
–1(F) = {d∈D | F∈P(d)}.
Тут P(d) розуміємо як повний образ d
при функції (відображенні) P.
Якщо предикат Р однозначний, то
T(P)∩F(P) = ∅.
Якщо предикат Р тотальний, то
T(P)∪F(P) = D.
Для однозначних предикатів області
істинності та хибності можна визначити
так:
T(P) = {d∈D | P(d)↓ = T};
F(P) = {d∈D | P(d)↓ = F}.
Тут і надалі для однозначних функ-
цій пишемо f(d)↓, якщо f(d) визначене, та
f(d)↑, якщо f(d) невизначене.
Логіка тотальних однозначних пре-
дикатів – це класична логіка. Логіки одно-
значних часткових предикатів – це логіки з
неокласичною семантикою, логіки тоталь-
них неоднозначних предикатів – логіки
з пересиченою семантикою. Логіки частко-
вих неоднозначних предикатів природно
назвати логіками із загальною семанти-
кою. Такі нестандартні семантики для
пропозиційної логіки та різноманітні від-
ношення логічного наслідку запропоновані
О.Д. Смирновою [5]. У роботі [6] подібні
семантики та формалізації відношення ло-
гічного наслідку узагальнені на випадок
КНЛ реномвінативного та кванторного рі-
внів.
Предикат P на D назвемо:
– тотально істинним, якщо T(P) = D;
– тотально хибним, якщо F(P) = D;
– тотожно істинним, якщо T(P) = D
та F(P) = ∅;
– тотожно хибним, якщо T(P) = ∅ та
F(P) = D;
– тотально насиченим, якщо T(P) =
= F(P) = D;
– неспростовним, або частково іс-
тинним, якщо F(P) = ∅;
– виконуваним, якщо T(P) ≠ ∅.
Побудову КНЛ починаємо з гранич-
но-абстрактних рівнів, поступово їх конкре-
тизуючи. Такі рівні відрізняються тракту-
ванням рівня розгляду даних. Можна виді-
лити [4] відносно бідні пропозиційний і
сингулярний рівні та дуже багатий номіна-
тивний рівень.
Hа пропозиційному рівні предикати
мають вигляд Р : D →{T, F}, де D – сукуп-
ність абстрактних даних.
20
Теоретичні та методологічні основи програмування
На номінативному рівні складні да-
ні будуються із простіших на основі від-
ношень іменування (номінативних відно-
шень), такі дані названі номінатами. Цей
рівень розпадається на низку підрівнів, ос-
новним з яких є підрівень однозначних
номінатів (іменних множин), на ньому далі
виділяємо реномінативний та першопоряд-
кові рівні. Визначальною особливістю пер-
шопорядкових рівнів є наявність компози-
цій квантифікації. Базовим першопорядко-
вим рівнем є кванторний, який також на-
зиватимемо, за аналогією з класичною ло-
гікою, рівнем чистих першопорядкових
КНЛ. Наступними першопорядковими рі-
внями є кванторно-екваційний, функціона-
льний та функціонально-екваційний. Осно-
вну увагу в роботі приділимо логікам кван-
торно-екваційного рівня, такі логіки можна
назвати чистими першопорядковими КНЛ
з рівністю (скор. ЧКНЛР).
Іменні множини (ІМ) – це множини
пар, перша компонента яких – ім’я, а друга
– його значення. Функції та предикати, за-
дані на ІМ, називають квазіарними. Фор-
мальне визначення ІМ таке.
V-іменна множина (V-ІМ) над A – це
однозначна функція вигляду δ : V→ A.
Тут V та A – множини предметних
імен та предметних значень.
V-ІМ будемо подавати у вигляді
[v1aa1,...,vnaan,...], де vі∈V, aі∈A, vі ≠ vj
при і ≠ j.
Клас всіх V-ІМ над A позначимо VA.
Вводимо функцію asn : VA→2V так:
asn(δ) = {v∈V | vaa∈δ для деякого a∈A}.
Визначимо δ ║Х = {vaa∈δ | v∈X⊆V}.
Замість δ ║(V \Х) та δ ║(V \{x}) бу-
демо писати δ ║–Х та δ ║–x .
Операцію накладки для ІМ вводимо
так: δ1∇δ2 = δ2∪ (δ1 ||(V \ asn(δ2))).
Операцію реномінації
r 1
1
,...,
,...,
n
n
v v
x x : VА → VA задамо так: r 1
1
,...,
,...,
n
n
v v
x x (δ) =
= [v1aδ(x1),...,vnaδ(xn)]∪(δ║(V\{v1,...,vn})).
Замість y1,…, yn також скорочено
писатимемо y .
Предикат вигляду Р : VA → {T, F}
називають V-квазіарним предикатом на A.
Клас V-квазіарних предикатів на A
позначаємо PrA.
Ім'я x∈V строго неістотне для V-
квазіарного предиката P : VA → {T, F}, як-
що P(d∇xaa) = P(d║–x) для довільних
d∈VA та a∈A.
Фундаментальною властивістю ві-
дображень, які використовуються в про-
грамуванні, є монотонність щодо розши-
рення даних новими компонентами.
Предикат P : VA→{T, F} монотонний,
якщо з умови d ⊆ d' випливає P(d) ⊆ P(d').
Для однозначних часткових функ-
цій, зокрема, предикатів, вводиться понят-
тя еквітонності. Еквітонність предиката оз-
начає, що прийняте ним значення зберіга-
ється при розширенні даних.
Предикат P : VA → {T, F} еквітон-
ний, якщо з умови P(d)↓ та d ⊆ d′ випливає
P(d′)↓ = P(d).
Для однозначних часткових преди-
катів поняття монотонності та еквітонності
рівносильні.
Еквітонність можна трактувати як
збереження "інформативності" предиката
при збільшенні "інформативності" вхідних
даних. Проте для тотальних монотонних
предикатів при розширенні вхідних даних
"інформативність" може тільки зменшува-
тися, тому прийнятною для тотальних пре-
дикатів є дуальна до монотонності власти-
вість антитонності. Водночас для однозна-
чних предикатів поняття антитонності ма-
лозмістовне.
Універсальні методи побудови пре-
дикатів визначають композиції, вони ви-
ступають ядром логіки певного типу. Згід-
но КНП, композиції уточнюємо як функції
(операції) над іменованими предикатами.
Композиції пропозиційного рівня
називають логiчними зв'язками, найпоши-
ренішими з них є заперечення ¬, диз'юнк-
ція ∨, кон'юнкція &, імплікація →, еквіва-
ленція ↔.
Предикати ¬(P), ∨(P, Q) →(P, Q),
&(P, Q), ↔(P, Q) далі будемо позначати
¬P, P∨Q, P→Q, P&Q, P↔Q.
Зазначені предикати задаємо так.
T(¬P) = F(P);
21
Теоретичні та методологічні основи програмування
F(¬P) = T(P).
T(P∨Q) = T(P)∪T(Q);
F(P∨Q) = F(P)∩F(Q).
T(P&Q) = T(P)∩T(Q);
F(P&Q) = F(P)∪F(Q).
T(P→Q) = F(P)∪T(Q);
F(P→Q) = T(P)∩F(Q).
T(P↔Q) = (T(P)∩T(Q))∪(F(P)∩F(Q));
F(P↔Q) = (T(P)∩F(Q))∪(F(P)∩T(Q)).
Базовими композиціями пропози-
ційного рівня будемо вважати ¬ та ∨.
Композиції →, &, ↔ є похідними.
Базовими композиціями реноміна-
тивного рівня є ¬, ∨ та композиція реномі-
нації R v
x : PrА → PrА.
Базовими композиціями кванторно-
го рівня є ¬, ∨, R v
x та композиція кванти-
фікації ∃x : PrА → PrА.
Базовими композиціями кванторно-
екваційного рівня є ¬, ∨, реномінації R ,v
x
квантори ∃x та спеціальні 0-арні компози-
ції – параметризовані за іменами предика-
ти рівності =ху .
Для визначення цих композицій за-
дамо предикати R v
x (P), ∃xP, =xy областями
їх істинності й хибності:
T(R v
x (P)) = r v
x (T(P));
F(R v
x (P)) = r v
x (F(P));
T(∃xP) = {d∈VA | T∈Р(d∇xaa) для
деякого a∈A};
F(∃xP) = {d∈VA | F∈Р(d∇xaa) для
всіх a∈A};
T(=xy ) = {d∈VA | d(x)↓, d(y)↓ та
d(x) = d(y)};
F(=xy ) = {d∈VA | d(x)↓, d(y)↓ та
d(x) ≠ d(y)}.
Похідна композиція ∀x : PrА → PrА
виражається через ¬ та ∃x. Предикат ∀xP
можна задати так:
T(∀xP) = {d∈VA | T∈Р(d∇xaa) для
всіх a∈A};
F(∀xP) = {d∈VA | F∈Р(d∇xaa) для
деякого a∈A}.
Теорема 1. Композиції ¬, ∨, R v
x ,
∃x, =xy зберігають властивості монотонно-
сті та антитонності.
Семантичними моделями ЧКНЛР є
композиційні системи квазіарних предикатів
кванторно-екваційного рівня (VА, PrA, C),
де C визначається базовими композиціями
¬, ∨, R v
x , ∃x, =ху . Терми відповідної ком-
позиційної алгебри (PrA, C) трактуємо як
формули мови ЧКНЛР.
2. Семантичні властивості
композиційно-номінативних логік
квазіарних предикатів
Опишемо мову ЧКНЛР.
Алфавiт мови: символи базових
композицій, множина Ps предикатних си-
мволів (ПС), множина V предметних імен.
Множину Ps назвемо сигнатурою мови.
Дамо визначення множини Fr фор-
мул мови ЧКНЛР.
1. Кожний р∈Ps та символ =ху є
формулою, такі формули атомарні.
2. Якщо Φ та Ψ – формули, то ¬Φ,
∨ФΨ, v
xR Φ , ∃xΦ – формули.
Надалі вживаємо символи похідних
композицій &, →, ↔, ∀x. "Формули", за-
писані з їх використанням, вважаємо ско-
роченнями "справжніх" формул. Замість
=xy також писатимемо в традиційному ви-
гляді x = y:
Позначаємо nm(Φ) множину всіх
предметних імен із V, які фігурують у фор-
мулі Φ.
Відображення інтерпретації формул
J : Fr→PrA визначається за допомогою то-
тального однозначного відображення
I : Ps → PrA, яке позначає символами Рs
базові предикати.
1. J(р) = I(p) для кожного р∈Ps;
J(=ху) = I(=ху) = =ху для всіх х, у∈V.
2. J(¬Φ) = ¬(J(Φ)),
J(∨ΦΨ) = ∨(J(Φ), J(Ψ)),
J ( )v
xR Φ = R v
x (J(Φ)), J(∃xΦ) = ∃x(J(Φ)).
Відображення I : Ps → Pr прив'язує
алгебраїчну систему (АС) даних (А, Pr) до
мови ЧКНЛР. Отримуємо АС з доданою
22
Теоретичні та методологічні основи програмування
сигнатурою [4] вигляду ((A, PrA), I), яку
позначаємо (A, I). Така АС фактично ви-
значає композиційну систему (VA, PrA, C),
тому АС з доданою сигнатурою є інтегро-
ваними семантичними моделями, які пов'я-
зують
на моделі
мови A
елі мови A
ім'я x с
а, я
мову із неокласичними АС даних.
Предикат J(Φ), який є значенням
формули Φ при інтерпретації
= (A, I), позначаємо ΦA.
Ім'я x∈V строго неістотне для фор-
мули Φ, якщо для кожної мод
трого неістотне для ΦA.
Формула примітивн кщо вона
атомарна або має вигляд v
xR p , причому
відсутні тотожні перейменування та ν не
містит
т
а (позн.
A |=Φ)
-неспростовна для
кожної
A-виконувана, якщо ΦA вико-
нувани
A-викону-
вана дл
), якщо ΦA –
тоталь
),
якщо A
сяться на кванторно-
еквацій
жина тотально істинних
форму
множи
них та неспросто-
вних формул порожні.
ь строго неістотних для p імен.
Φ (час ково) істинна при інтерпре-
тації на A, або A-неспростовн
, якщо ΦA неспростовний.
Φ всюди iстинна, або неспростовна
(позн. |= Φ), якщо Φ A
моделі мови A.
Φ виконувана при інтерпретації на
A = (A, I), або
й.
Φ виконувана, якщо Φ
я кожної моделі мови A.
Φ тотально істинна при інтерпре-
тації на A = (A, I) ( позн. A |≡ Φ
но істинний предикат.
Φ тотально iстинна ( позн. |≡ Φ
|≡ Φ для кожної моделі мови A.
Дослідження композиційно-номіна-
тивних логік часткових однозначних, тота-
льних неоднозначних і часткових неодно-
значних квазіарних предикатів реноміна-
тивного та кванторного рівнів проведені,
зокрема, в [6–9]. Відповідні властивості
таких логік перено
ний рівень.
Наведемо основні з них.
Теорема 2. 1) у випадку неокласич-
ної семантики мно
л порожня;
2) у випадку пересиченої семантики
на неспростовних формул порожня;
3) у випадку загальної семантики
множини тотально істин
Справді, у випадку неокласичної
семантики кожний ПС можна проінтер-
претувати як всюди невизначений пре-
дикат, на такій моделі мови кожна фор-
мула теж проінтерпретується як всюди
невизначений предикат. У випадку пере-
сиченої семантики кожний ПС можна
проінтерпретувати як тотально насичений
предикат, на такій моделі мови кожна
формула теж проінтерпретується як то-
тально насичений предикат. У випадку
загальної семантики на одній моделі
мови кожний ПС можна проінтерпрету-
вати як всюди невизначений предикат,
а на другій моделі мови – як тотально на-
сичений предикат.
Важливе поняття дуальних моделей
мови вводимо так (тут S позначає допов-
нення до S у VA).
АС B = (A, IB) дуальна до A = (A, IB A),
якщо ( ) ( )B AT FΦ = Φ та ( ) ( )B AF TΦ = Φ
для кожного Φ∈Ps.
Тоді АС A = (A, IA) дуальна до
B = (A, IB). B
Якщо A = (A, IA) – АС з частковими
однозначними предикатами, то дуальна
B = (A, IB) – АС з тотальними неоднознач-
ними предикатами, та навпаки.
B
Теорема 3. Нехай B = (A, IB) дуаль-
на до A = (A, I
B
A). Тоді для кожної Φ∈Fr:
1) ( ) ( )B AT FΦ = Φ та ( ) ( )B AF TΦ = Φ ;
2) ΦA монотонний ⇒ ΦB антитонний;
Φ
B
A антитонний ⇒ ΦBB монотонний.
Звідси маємо: ΦA неспростовний на
АС A із частковими однозначними преди-
катами ⇔ ΦB тотально істинний на дуаль-
ній АС B із тотальними неоднозначними
предикатами.
B
Таким чином, неокласична семан-
тика та пересичена семантика дуальні.
Відношення логічного наслідку.
На основі різних співвідношень між
областями істинності та хибності преди-
катів на множині формул можна ввести [6]
5 "природних" відношень логічного нас-
лідку.
Спочатку задамо відношення нас-
лідку для двох формул при інтерпретації
на фіксованій моделі мови A.
23
Теоретичні та методологічні основи програмування
1) "Істиннісний" наслідок A|=T :
Φ A|=T Ψ ⇔ T(ΦA) ⊆ T(ΨA).
2) "Хибнісний" наслідок A|=F :
Φ A|=F Ψ ⇔ F(ΨA) ⊆ F(ΦA).
3) "Cильний" наслідок A|=TF :
Φ A|=TF Ψ ⇔ T(ΦA) ⊆ T(ΨA) та
F(ΨA) ⊆ F(ΦA).
4) "Неспростовнісний" наслідок
A|=Cl : Φ A|=Cl Ψ ⇔ T(ΦA)∩F(ΨA) = ∅.
5) "Насичений" наслідок A|=Cm :
Φ A|=Cm Ψ ⇔ F(ΦA)∪T(ΨA) = VA.
Відповідні відношення логічного
наслідку |=T , |=F , |=TF , |=Cl , |=Cm визна-
чаємо за такою схемою:
Φ |=∗ Ψ ⇔ Φ A|=∗ Ψ для кожної мо-
делі мови A.
Тут і надалі, якщо інше не вказане,
∗ – це одне з Cl, Cm, T, F, TF.
Ψ є слабким логічним наслідком Φ
(позн. Φ ||= Ψ), якщо A |= Φ ⇒ A |= Ψ для
кожної моделі мови A.
Ψ є слабким тотальним наслідком Φ
(позн. Φ ||≡ Ψ), якщо A |≡ Φ ⇒ A |≡ Ψ для
кожної моделі мови A.
Введені відношення |=T , |=F , |=TF ,
|=Cl , |=Cm , ||=, ||≡ рефлексивні й транзитивні.
Теорема 4. Нехай АС B = (A, IB) ду-
альна до АС A = (A, I
B
A). Тоді:
1) Φ A|=T Ψ ⇔ Φ B|=B F Ψ та Φ A|=F Ψ
⇔ Φ BB|=T Ψ;
2) Φ A|=Cl Ψ ⇔ Φ B|=B Cm Ψ та Φ A|=Cm Ψ
⇔ Φ B |=Cl Ψ.
В загальній семантиці кожна АС B є
дуальною до деякої АС A, тому в загальній
семантиці маємо:
Φ |=T Ψ ⇔ Φ |=F Ψ ⇔ |=TF Ψ.
У випадку неокласичної семантики
немає жодної пари формул, які перебу-
вають у відношенні |=Cm .
У випадку пересиченої семантики
немає жодної пари, які перебувають у від-
ношенні |=Cl .
У випадку загальної семантики не-
має жодної пари формул, які перебувають
у відношенні |=Cl чи |=Cm .
Отже, для загальної семантики має-
мо єдине природне змістовне відношення
логічного наслідку |=TF .
Для неокласичної семантики можна
розглядати |=T , |=F , |=TF , |=Cl ; для переси-
ченої – |=T , |=F , |=TF , |=Cm .
Відношення логічного наслідку ін-
дукують відповідні відношення логічної
еквівалентності. Такі відношення рефлек-
сивні, транзитивні й симетричні. Відно-
шення еквівалентності в АС A A∼T , A∼F ,
A∼TF , A∼Cl , A∼Cm та відношення логічної ек-
вівалентності ∼T , ∼F , ∼TF , ∼Cl , ∼Cm визнача-
ємо за такою схемою:
Φ A∼∗ Ψ, якщо Φ A|=∗ Ψ та Ψ A|=∗ Φ;
Φ ∼∗ Ψ, якщо Φ |=∗ Ψ та Ψ |=∗ Φ.
Зауважимо, що Φ ∼TF Ψ ⇔ для кож-
ної моделі мови A маємо T(ΦA) = T(ΨA) та
F(ΨA) = F(ΦA), тобто ΦA = ΨA.
Теорема 5. Для кожної моделі мови
A маємо:
1) Φ A|=T Ψ ⇔ ¬Ψ A|=F ¬Φ та
Φ A|=F Ψ ⇔ ¬Ψ A|=T ¬Φ;
2) Φ A∼T Ψ ⇔ ¬Ψ A∼F ¬Φ та
Φ A∼F Ψ ⇔ ¬Ψ A∼T ¬Φ.
Поведінка введених відношень ло-
гічного наслідку та логічної еквівалентно-
сті вельми специфічна (див., наприклад,
[6]). Зокрема, невірними будуть такі спів-
відношення:
Φ A|=T Ψ ⇒ ¬Ψ A|=T ¬Φ,
¬Ψ A|=T ¬Φ ⇒ Φ A|=T Ψ,
Φ A|=F Ψ ⇒ ¬Ψ A|=F ¬Φ,
¬Ψ A|=F ¬Φ ⇒ Φ A|=F Ψ;
Φ A∼T Ψ ⇒ ¬Ψ A∼T ¬Φ,
¬Ψ A∼T ¬Φ ⇒ Φ A∼T Ψ,
Φ A∼F Ψ ⇒ ¬Ψ A∼F ¬Φ,
¬Ψ A∼F ¬Φ ⇒ Φ A∼F Ψ.
Таким чином, для |=T та |=F закон
контрапозиції невірний, для ∼T та ∼F вже не
можна знімати заперечення в обох частинах
еквівалентності.
Для відношень ∼Cl, ∼Cm, ∼TF справ-
джується теорема семантичної еквiвален-
тності (∗ – одне з Cl, Cm, TF).
Теорема 6. Нехай Φ' отримана з фо-
рмули Φ заміною деяких входжень формул
Φ1, ..., Φn на Ψ1, ..., Ψn вiдповiдно. Якщо
Φ1 ∼∗ Ψ1, ..., Φn ∼∗ Ψn, то Φ ∼∗ Φ'.
Для відношень ∼T та ∼F теорема 11
невірна. Справді, можлива ситуація, коли
24
Теоретичні та методологічні основи програмування
вірно Ξ ∼T
Φ та невірно ¬Ξ ∼T
¬Φ, адже
¬Ξ ∼T
¬Φ ⇔ Ξ ∼F
Φ; можливо також, що
вірно Ξ ∼F
Φ та невірно ¬Ξ ∼F
¬Φ.
Для кожного р∈Ps множину строго
неістотних предметних імен задаємо за до-
помогою тотальної функції ν : Ps→2V. Така
функція [7] продовжується ν : Fr→2V . При
цьому ν(=xy) = V \{х, у}. Для семантичних
моделей ЧКНЛР постулюємо наявність
нескінченної множини ( )
p Ps
p
∈
νI тотально
строго неістотних імен.
Властивості формул ЧКНЛР. Роз-
глянемо властивості, пов'язані з компози-
ціями. Вони відбивають відповідні власти-
вості цих композицій. Основні властивості
пропозиційних композицій аналогічні від-
повідним властивостям логічних зв’язок
класичної логіки. Це комутативність і асо-
ціативність ∨ та &, ідемпотентність ∨ та
&, закони контрапозиції, зняття подвійно-
го заперечення, де Моргана. Їх можна опи-
сати, використовуючи ∼TF .
До основних властивостей формул,
пов'язаних з композицією реномінації, на-
лежать відомі [4, 6] RТ. R¬, R∨, RR, NR, а
також ΦN. Ці властивості можна описати,
використовуючи ∼TF . Наприклад.
ΦN) нехай у∈V строго неістотне для
Φ. Тоді ,
, ( )y v
z xR Φ ∼TF ( )v
xR Φ .
Властивості формул, пов'язані з
композиціями квантифікації в основному
аналогічні [4, 6] відповідним властивостям
класичної логіки. Водночас далеко не всі
закони класичної логіки справджуються
для логік квазіарних предикатів. Зокрема,
навіть для однозначних предикатів не зав-
жди справджуються закони класичної ло-
гіки |=∀xθ→θ, |= θ→∃xθ, ∀xθ ||= θ, а також
більш загальні твердження |=
|=
( ),x
zx R∀ θ→ θ
( ) ,x
zR xθ → ∃ θ ∀xθ ||= ( ).x
zR θ
В класичній логіці кожна формула
вигляду ¬∃xΦ & Φ невиконувана. Для ло-
гіки квазіарних предикатів це вже не так:
існують [10] виконувані формули вигляду
¬∃xΦ & Φ.
До основних властивостей формул,
пов'язаних з композиціями квантифікації
та реномінації, належать [4, 6] NR, RSN,
R∃, R∃S, а також R∃R – згортка пари імен
реномінації за квантифікованим іменем:
R∃R) ,
, ( )u x
v yR x∃ Φ ∼TF (u
v )R x∃ Φ (тут
{ }x u∉ ); зокрема, маємо (ху )R x∃ Φ ∼TF ∃хФ.
Основними властивостями рівності
є рефлексивність, cиметричність, транзи-
тивність, заміна рівних:
Rf) |= х = х та |≡ х = х ;
Sm) х = y ∼TF y = x ;
Tr) |= х1 = y1 → y = z → x = z та
|≡ х = y → y = z → x = z ;
EФ) |= х1 = y1 →…→ хn = yn →
→ 1
1
,...,
,..., ( )n
n
v v
x xR Φ → та 1
1
,...,
,..., ( )n
n
v v
y yR Φ
|≡ х1 = y1 →…→ хn = yn →
→ 1
1
,...,
,..., ( )n
n
v v
x xR Φ → 1
1
,...,
,..., ( ).n
n
v v
y yR Φ
3. Спеціальні відношення
логічного наслідку
Введені відношення логічного нас-
лідку можна поширити на довільні мно-
жини формул.
Відношення логічного наслідку
для множин формул. Спочатку задамо
відношення наслідку для множин формул
при інтерпретації на фіксованій моделі мо-
ви АС A. Для довільних Γ⊆ Fr та Δ ⊆ Fr
визначаємо:
Γ A|=Cl Δ, якщо
( ) ( )A AT F
Φ∈Γ Ψ∈Δ
Φ ∩ Ψ =I I ∅
A
)
;
Γ A|=Cm Δ, якщо
; ( ) ( ) V
A AF T
Φ∈Γ Ψ∈Δ
Φ ∪ Ψ =U U
Γ A|=T Δ, якщо
( ) (A AT T
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U ;
Γ A|=F Δ, якщо
( ) ( )A AF F
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U ;
Γ A|=TF Δ, якщо
( ) ( )A AT T
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U та
( ) ( )A AF F
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U .
Відношення логічного наслідку для
множин формул |=T, |=F, |=TF, |=Cl, |=Cm ви-
значаємо за такою схемою:
25
Теоретичні та методологічні основи програмування
Γ |=∗ Δ, якщо Γ A|=∗ Δ для кожної мо-
делі мови A.
Відношення |=T , |=F , |=TF , |=Cl ,
|=Cm рефлексивні, але не транзитивні.
Теорема 7. Нехай АС B = (A, IB) ду-
альна до АС A = (A, I
B
A). Тоді:
1) Γ A|=T Δ ⇔ Γ B|=F Δ та
Γ A|=F Δ ⇔ Γ B|=T Δ;
2) Γ A|=Cl Δ ⇔ Γ B|=Cm Δ та
Γ A|=Cm Δ ⇔ Γ B|=Cl Δ.
Звідси випливає, що у випадку зага-
льної семантики
Γ A|=T Δ ⇔ Γ A|=F Δ ⇔ Γ A|=TF Δ.
Таким чином, для загальної семан-
тики природно розглядати лише відно-
шення |=TF .
Для неокласичної семантики можна
розглядати |=T , |=F , |=TF , |=Cl ; для переси-
ченої – |=T , |=F , |=TF , |=Cm .
Теорема 8 (заміни еквівалентних).
Нехай Φ ∼TF Ψ. Тоді: Φ, Γ |=∗ Δ ⇔ Ψ, Γ |=∗ Δ
та Γ |=∗ Δ, Φ ⇔ Γ |=∗ Δ, Ψ.
Замість ∼TF тут можна брати ∼Cl чи
∼Cm . Тоді |=∗ буде відповідно відношенням
|=Cl чи |=Cm . Отримуємо ще дві різновид-
ності теореми заміни еквівалентних – для
логіки часткових однозначних предикатів
(із |=Cl ) та для логіки тотальних неодно-
значних предикатів (із |=Cm ).
Розглянемо властивості відношень
логічного наслідку для множин формул.
До властивостей пропозиційного
рівня належать U, С, ¬¬|–, ¬¬–|, ∨|–, ∨–|,
¬∨|–, ¬∨–|. Вони справджуються для кож-
ного з відношень логічного наслідку даної
семантики. Ці властивості наведено в [9].
Для |=Cl та |=Cm також справджу-
ються відомі ¬|– та ¬–|, але вони невірні
для |=T , |=F та |=TF .
Властивості реномінації RT, R¬,
R∨, RR, ΦN, R∃, R∃S, R∃R індукують низ-
ку відповідних властивостей відношень
логічного наслідку для множин формул,
вони отримуються на основі теореми за-
міни еквівалентних. Ці властивості справ-
джуються для |=TF, у відповідних семанти-
ках вони вірні й для |=T, |=F, |=Cl, |=Cm.
Властивості RT|–, RT–|, ¬RT|–, ¬RT–|,
RR|–, RR–|, ¬RR|–, ¬RR–|, R¬|–, R¬–|, ¬R¬|–,
¬R¬–|, R∨|–, R∨–|, ¬R∨|–, ¬R∨–|, ΦN|–, ΦN–|,
¬ΦN|–, ¬ΦN–|, R∃|–, R∃–|, ¬R∃|–, ¬R∃–|,
R∃S|–, R∃S–|, ¬R∃S|–, ¬R∃S–| наведено в [9].
Укажемо тут властивості, індуковані R∃R.
R∃R|–) ,
, (u x
v y ),R x∃ Φ Γ |=∗ Δ ⇔
⇔ (u
v ),R x∃ Φ Γ |=∗ Δ. Зокрема,
(x
y ),R x∃ Φ Γ |=∗ Δ ⇔ ∃хΦ, Γ |=∗ Δ.
R∃R–|) Γ |=∗ Δ, ,
, (u x
v y )R x∃ Φ ⇔
⇔ Γ |=∗ Δ, (u
v )R x∃ Φ . Зокрема,
Γ |=∗ Δ, (x
y )R x∃ Φ ⇔ Γ |=∗ Δ, ∃хΦ.
¬R∃R|–) ,
, (u x
v y ),R x¬ ∃ Φ Γ |=∗ Δ ⇔
⇔ (u
v ),R x¬ ∃ Φ Γ |=∗ Δ. Зокрема,
(x
y ),R x¬ ∃ Φ Γ |=∗ Δ ⇔ ¬∃хΦ, Γ |=∗ Δ.
¬R∃R–|) Γ |=∗ Δ, ,
, (u x
v y )R x¬ ∃ Φ ⇔
⇔ Γ |=∗ Δ, (u
v )R x¬ ∃ Φ . Зокрема,
Γ |=∗ Δ, (x
y )R x¬ ∃ Φ ⇔ Γ |=∗ Δ, ¬∃хΦ.
Для |=T , |=F, |=TF не можна знімати
заперечення, переносячи формулу з лівої
частини у праву і навпаки, тому ми фор-
мулюємо додаткові властивості для випадку
зовнішнього заперечення на реномінацію.
Х–Y-означені відношення логічно-
го наслідку. В логіках квазіарних преди-
катів значення предиката P на даному d
може бути різним залежно від того, вхо-
дить чи не входить до d компонента з пев-
ним предметним іменем. Тому при інтер-
претаціях формул на моделях мови необ-
хідно явно вказувати множини означених
та неозначених імен. Поняття Х–Y-озна-
ченої іменної множини та Х–Y-означеного
логічного наслідку введені в [7].
Для диз’юнктних Х, Y ⊆ V (диз’юнк-
тність означає Х∩Y = ∅) множину Х–Y-оз-
начених V-ІМ задамо так:
V, Х–YA = {d∈VA | Х ⊆ im(d) та Y ∩ im(d) = ∅}.
В Х–Y-означених ІМ імена із Х ма-
ють значення, імена із Y не мають значення.
Для довільних диз’юнктних мно-
жин Z, W, U ⊆ V маємо:
26
Теоретичні та методологічні основи програмування
, , ( \ )V W U V W Y U Z Y
Y Z
A A− ∪ − ∪
⊆
= U .
Для диз’юнктних Х, Y ⊆ V задамо
Х–Y-означені області істинності й хибності
квазіарного предиката Р:
TХ–Y (P) = {d∈VA | T∈Р(d) та Х ⊆ im(d),
Y ∩ im(d) = ∅} = {d∈V, Х–YA | T∈Р(d)}.
FХ–Y (P) = {d∈VA | F∈Р(d) та Х ⊆ im(d),
Y ∩ im(d) = ∅} = {d∈V, Х–YA | F∈Р(d)}.
Теорема 9. За умови y∈Y справджу-
ються співвідношення (тут { }x u∉ ):
TY–Z
,
,( (u x
v y ))R P ⊆ TY–Z( ( )u
v )R xP∃ ,
FY–Z ( ( )u
v )R xP∃ ⊆ FY–Z
,
,( (u x
v y ))R P .
Зокрема, при y∈Y маємо (див. [7]):
TY–Z ( x
yR (Р)) ⊆ TY–Z (∃x(Р)),
FY–Z (∃x(Р)) ⊆ FY–Z ( x
yR (Р)).
Задамо Х–Y-означені відношення на-
слідку для двох формул при інтерпретації на
фіксованій моделі мови A.
Φ A, Х–Y |=Cl Ψ, якщо
TХ–Y (ΦA)∩FХ–Y (ΨA) = ∅;
Φ A, Х–Y |=Cm Ψ, якщо
TХ–Y (ΦA)∪FХ–Y (ΨA) = V, Х–YA;
Φ A, Х–Y |=T Ψ, якщо
TХ–Y (ΦA) ⊆ TХ–Y (ΨA);
Φ A, Х–Y |=F Ψ, якщо
FХ–Y (ΨA) ⊆ FХ–Y (ΦA);
Φ A, Х–Y |=TF Ψ, якщо
TХ–Y (ΦA) ⊆ TХ–Y (ΨA) та FХ–Y (ΨA) ⊆ FХ–Y (ΦA).
Тут і надалі в записах вигляду
A, Х–Y |= та Х–Y |= множини Х, Y – диз’юнктні.
Якщо Y = ∅, то маємо Х-означені ві-
дношення наслідку A, Х |=Cl, A, Х |=Cm, A, Х |=T,
A, Х |=F, A, Х |=TF . Якщо Х = ∅, то маємо
Y-неозначені відношення наслідку A, –Y |=Cl,
A, –Y |=Cm, A, –Y |=T, A, –Y |=F, A, –Y |=TF .
У випадку Х = Y = ∅ мaємо відно-
шення A|=Cl, A|=Cm, A|=T, A|=F, A|=TF .
Поширимо вищевведені відношення
на довільні множини формул.
Γ A, Х–Y |=Cl Δ, якщо
. ( ) ( )X Y A X Y AT F− −
Φ∈Γ Ψ∈Δ
Φ ∩ Ψ =∅I I
Γ A, Х–Y |=Cm Δ, якщо
. , ( ) ( ) V X Y
X Y A X Y AF T −
− −
Φ∈Γ Ψ∈Δ
Φ ∪ Ψ =U U A
)
Γ A, Х–Y |=T Δ, якщо
( ) (X Y A X Y AT T− −
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U .
Γ A, Х–Y |=F Δ, якщо
( ) (X Y A X Y AF F− −
Ψ∈Δ Φ∈Γ
)Ψ ⊆ ΦI U .
Γ A, Х–Y |=TF Δ, якщо
( ) (X Y A X Y AT T− −
Φ∈Γ Ψ∈Δ
)Φ ⊆ ΨI U та
( ) (X Y A X Y AF F− −
Ψ∈Δ Φ∈Γ
)Ψ ⊆ ΦI U .
Аналогічним чином вводимо Х-оз-
начені та Y-неозначені відношення наслід-
ку для множин формул:
A, Х |=Cl, A, Х |=Cm, A, Х |=T, A, Х |=F, A, Х |=TF
та A, –Y |=Cl, A, –Y |=Cm, A, –Y |=T, A, –Y |=F, A, –Y |=TF .
У випадку Х = Y = ∅ отримуємо від-
ношення A |=Cl, A |=Cm, A |=T, A |=F, A |=TF .
Відношення Х–Y-означеного логіч-
ного наслідку для множин формул
A, Х–Y |=Cl, A, Х–Y |=Cm, A, Х–Y |=T, A, Х–Y |=F,
A, Х–Y |=TF визначаємо за такою схемою:
Γ Х–Y |=∗ Δ, якщо Γ A, Х–Y |=∗ Δ для
кожної моделі мови A.
Аналогічно вводимо Х-означені та
Y-неозначені відношення логічного наслід-
ку для множин формул.
Із визначень отримуємо:
1) Γ A|=∗ Δ ⇒ Γ A, Х |=∗ Δ ⇒ Γ A, Х–Y |=∗ Δ;
Γ A |=∗ Δ ⇒ Γ A, –Y |=∗ Δ ⇒ Γ A, Х–Y |=∗ Δ;
2) Γ |=∗ Δ ⇒ Γ Х |=∗ Δ ⇒ Γ Х–Y |=∗ Δ;
Γ |=∗ Δ ⇒ Γ –Y |=∗ Δ ⇒ Γ Х–Y |=∗ Δ;
3) нехай та Γ ⊆ Λ та Δ ⊆ Σ; тоді
Γ A, Х–Y |=∗ Δ ⇒ Λ A, Х–Y |=∗ Σ та
Γ Х–Y |=∗ Δ ⇒ Λ Х–Y |=∗ Σ.
Теорема 10. Нехай z тотально стро-
го неістотне та z∉nm(Γ∪Δ). Тоді:
Γ A, {z}∪Х–Y |=∗ Δ ⇔ Γ A, Х–Y |=∗ Δ та
Γ {z}∪Х–Y |=∗ Δ ⇔ Γ Х–Y |=∗ Δ.
Теорема 11. Нехай Z, W, U ⊆ V – ди-
з’юнктні множини предметних імен. Тоді
Γ A, W–U |=∗ Δ ⇔ для кожної Y ⊆ Z
маємо Γ A, W∪Y–U∪(Z\Y) |=∗ Δ.
27
Теоретичні та методологічні основи програмування
Теорема 12. Нехай Z, W, U ⊆ V – ди-
з’юнктні множини предметних імен. Тоді:
Γ A, W–U |=∗ Δ, ∃хΦ ⇔ для кожної Y ⊆ Z
Γ A, W∪Y–U∪(Z\Y) |=∗
|=∗ Δ, ∃хΦ, 1
( ),..., ( ),...,
n
x x
y yR RΦ Φ
де всі yi∈ W∪Y;
Γ A, W–U |=∗ Δ, (u
v )R x∃ Φ ⇔ для кожної Y ⊆ Z
Γ A, W∪Y–U∪(Z\Y) |=∗
|=∗ Δ, ( ),u
vR x∃ Φ
1
, ,
, ,( ),..., ( ),...,
n
u x u x
v y v yR RΦ Φ
де всі yi∈W∪Y.
Теорема 13. Нехай Z ⊆ V. Тоді:
Γ A |=∗ Δ, ∃хΦ ⇔ для кожної непо-
рожньої Y ⊆ Z маємо
Γ A, Y–(Z\Y) |=∗ Δ, ∃хΦ,
1
( ),..., ( ),...,
n
x x
y yR RΦ Φ
де всі yi∈Y,
та Γ A, {t}–Z |=∗Δ, ∃хΦ, ( ),x
tR Φ де t тотально
строго неістотне, t∉пт(Γ, Δ, ∃хΦ);
Γ A |=∗ Δ, (u
v )R x∃ Φ ⇔ для кожної не-
порожньої Y ⊆ Z маємо Γ A, Y–(Z\Y) |=∗
|=∗ Δ, ( ),u
vR x∃ Φ
1
, ,
, ,( ),..., ( ),...,
n
u x u x
v y v yR RΦ Φ
де всі yi∈Y,
та Γ A, {t}–Z |=∗ Δ, ( ),u
vR x∃ Φ ,
, ( ),u x
v tR Φ
де t∉пт(Γ, Δ, (u
v )R x∃ Φ ), t тотально строго
неістотне.
Для формул вигляду v
xR Φ введено
[7] поняття U-неозначуваної форми. Тут
довільну U ⊆ V трактуємо як множину не-
означених імен. Це означає, що при інтер-
претаціях усі імена U не мають значення.
Нехай така: усі
r
1 1 1
1 1 1
,... , ,... , ,...
,... , ,... , ,...
k n m
k n m
r r x x u u
s s y y v vR Φ
1,…, rk, s,…, sk, y1,…, yn ∈U, {x1,…, xn}∩U = ∅,
{v1,…, vm}∩U = ∅.
U-неозначувана форма формули
– це вираз вигляду
, де ⊥ – спеціальний символ,
який позначає невизначене значення.
1 1 1
1 1 1
,... , ,... , ,...
,... , ,... , ,...
k n m
k n m
r r x x u u
s s y y v vR Φ
1 1
1
,... , ,...,
,..., , ,...,
n m
m
x x u u
v vR⊥ ⊥ Φ
Нехай a
bR Φ та c
eR Φ мають одна-
кові U-неозначувані форми. Тоді для кож-
ної моделі мови A маємо:
( ) ( )a c
A e AbR d R dΦ = Φ для всіх d∈V, –UA, де
усі імена U не мають значення. Таким чи-
ном, отримуємо властивість:
UnD) якщо v
xR Φ та z
yR Φ мають од-
накові U-неозначувані форми, то
,v
xR Φ Γ A, –U |=∗ ,z
yR Φ Δ.
Теорема 14. Нехай z тотально неіс-
тотне та z∉пт(Γ, Δ, ∃хΦ), тоді за умови z∈X
маємо:
Γ, ∃хΦ Х–Y |=∗ Δ ⇔ Γ, ∃хΦ {z}Х–Y |=∗ Δ ⇔
⇔ Γ, ( )x
zR Φ {z}∪Х–Y |=∗ Δ;
нехай z тотально неістотне та
z∉пт(Γ, Δ, (u
v )R x∃ Φ ), тоді при z∈X маємо:
Γ, (u
v )R x∃ Φ Х–Y |=∗ Δ ⇔
⇔ Γ, (u
v )R x∃ Φ {z}∪Х–Y |=∗ Δ ⇔
⇔ Γ, ,
, ( )u x
v yR Φ {z}∪Х–Y |=∗ Δ.
4. Секвенційні числення логік
квазіарних предикатів кванторно-
екваційного рівня
Властивості відношення логічного
наслідку для множин формул є семантич-
ною основою побудови для КНЛ числень
секвенційного типу. Таке числення для за-
даного відношення |=∗ будується так, що
секвенція |–Γ–|Δ має виведення ⇔ Γ |=∗ Δ.
Секвенції трактуємо як множини формул,
специфікованих (відмічених) спеціальни-
ми символами |– та –| , які не входять до ал-
фавіту мови. Позначаємо секвенції як |–Γ–|Δ,
або, не деталізуючи, як Σ.
Секвенційні числення для відно-
шень |=Cl, |=T, |=F, |=TF КНЛ однозначних
квазіарних предикатів кванторного рівня
збудовано в [9]. В даній роботі розглянемо
побудову секвенційного числення для від-
ношення |=Cl логіки однозначних квазіарних
предикатів кванторно-екваційного рівня,
таке відношення далі позначатимемо |=. На
відміну від [9], використовуємо спеціальні
секвенційні форми елімінації кванторів під
реномінацією, що робить зайвим викорис-
тання секвенційних форм для пронесення
кванторів через реномінації.
Секвенційні числення кванторно-
екваційного рівня можна розглядати як ок-
ремий випадок прикладних секвенційних
числень кванторного рівня. Виведення в
28
Теоретичні та методологічні основи програмування
прикладних численнях – це виведення сек-
венцій з доданими власними аксіомами
(збагачених секвенцій). Виведення в при-
кладному численні секвенції Σ означає ви-
ведення збагаченої секвенції ΣR = Σ∪|–Ах, де
|–Ах = {|–A | A∈Ах}, Ах – множина власних
аксіом. Тому числення кванторно-еквацій-
ного рівня можна трактувати як прикладні,
в яких Ах складається з таких аксіом для рів-
ності: рефлексивності ∀x(x = x), симетрич-
ності ∀x∀y(x = y → y = x), транзитивності
∀x∀y∀z(x = y → y = z → x = z) (тут x, y, z –
тотально строго неістотні); заміни рівних
∀x∀y(x = y → ( ,
, ( )z u
x vR p ↔ ,
, ( )))z u
y vR p для всіх
p∈Ps та , ,z u v (тут x, y – тотально строго
неістотні, відмінні від , ,z u v ).
Виведення в секвенційних числен-
нях має вигляд дерева, вершинами якого є
секвенції. Такі дерева називають секвен-
ційними. Формально визначення секвен-
ційного дерева дається [2, 4] індуктивно.
Аксіомами секвенційного числення
виступають замкнені секвенції. Замкне-
ність |–Γ–|Δ означає, що Γ |= Δ.
Базова умова замкненості: секвенція
Ξ замкнена, якщо існує формула Φ така, що
|–Φ∈Ξ та –|Φ∈Ξ.
Додаткова умова UnD замкненості
секвенції у даній вершині секвенційного де-
рева визначається на основі властивості
UnD. Нехай U – множина всіх неозначених
імен у даній вершині Ξ.
Секвенція Ξ U-замкнена, якщо:
UnD) існує пара формул |–
v
xR A∈Ξ та
–|
u
yR A∈ Ξ: v
xR A та u
yR A мають однакові
U-неозначувані форми.
Якщо секвенція |–Γ–|Δ U-замкнена, то
Γ A, Х–U |= Δ для довільних A та Х ⊆ V, де
Х ∩ U = ∅.
Секвенційне дерево замкнене, якщо
кожний його лист – замкнена секвенція.
Правилами виведення секвенційних
числень є секвенційні форми. Вони є син-
таксичними аналогами семантичних влас-
тивостей відношення |=.
Секвенція Σ вивідна, або має виве-
дення, якщо існує замкнене секвенційне
дерево з коренем Σ.
Беручи до уваги семантичні власти-
вості відношення |=, вводимо такі базові
секвенційні форми:
|–¬ |
|
,
,
A
A
−
−
Σ
¬ Σ
; –|¬ |
|
,
,
A
A
−
−
Σ
¬ Σ
;
|–∨ | |
|
, ,
,
A B
A B
− −
−
Σ Σ
∨ Σ
; –|∨ | |
|
, ,
,
A B
A B
− −
−
Σ
∨ Σ
;
|–RT |
,
| ,
( ),
( ),
v
x
z v
z x
R A
R A
−
−
Σ
Σ
; –|RT |
,
| ,
( ),
( ),
v
x
z v
z x
R A
R A
−
−
Σ
Σ
;
|–ΦN |
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
−
−
Σ
Σ
при у∈ν(A);
–|ΦN |
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
−
−
Σ
Σ
при у∈ν(A);
|–R∃R |
,
| ,
( ),
( ),
u
v
u x
v y
R xA
R xA
−
−
∃ Σ
∃ Σ
при { }x u∉ ;
–|R∃R |
,
| ,
( ),
( ),
u
v
u x
v y
R xA
R xA
−
−
∃ Σ
∃ Σ
при { }x u∉ ;
|–R∃p |
|
,
( ),x
y
xA
R xA
−
−
∃ Σ
∃ Σ
; –|R∃p |
|
,
( ),x
y
xA
R xA
−
−
∃ Σ
∃ Σ
;
|–RR |
|
( ),
( ( )),
v w
x y
v w
x y
R A
R R A
−
−
Σ
Σ
o
; –|RR |
|
( ),
( ( )),
v w
x y
v w
x y
R A
R R A
−
−
Σ
Σ
o
;
|–R¬ |
|
( ),
( ),
v
x
v
x
R A
R A
−
−
¬ Σ
¬ Σ
; –|R¬ |
|
( ),
( ),
v
x
v
x
R A
R A
−
−
¬ Σ
¬ Σ
;
|–R∨ |
|
( ) ( ),
( ),
v v
x x
v
x
R A R B
R A B
−
−
∨ Σ
∨ Σ
;
–|R∨ |
|
( ) ( ),
( ),
v v
x x
v
x
R A R B
R A B
−
−
∨ Σ
∨ Σ
;
|–∃R
,
| ,
|
( ),
( ),
u x
v z
u
v
R A
R xA
−
−
Σ
∃ Σ
;
–|∃R
,
| , |
|
( ), ( ),
( ),
u x u
v y v
u
v
R A R xA
R xA
− −
−
∃ Σ
∃ Σ
.
Для |–∃R ім’я { }x u∉ , ім’я z тотально
строго неістотне та z∉пт(Σ, ( )u
vR x∃ Φ ) .
|–∃ |
|
( ),
,
x
yR A
xA
−
−
Σ
∃ Σ
; –|∃ | |
|
( ), ,
,
x
zR A xA
xA
− −
−
∃ Σ
∃ Σ
.
Для |–∃ ім’я у тотально строго неісто-
29
Теоретичні та методологічні основи програмування
тне та у∉пт(Σ, А).
Для будованих числень не будемо
явно вносити до секвенції аксіоми рівно-
сті, а враховуватимемо їх за потребою. Це
означає введення додаткової умови
замкненості секвенції та допоміжних
секвенційних форм.
Додаткова умова замкненості вра-
ховує аксіому рефлексивності:
секвенція Ξ замкнена, якщо
–| x = x ∈ Ξ для деякого x∈V.
Для врахування аксіом симетрично-
сті й транзитивності вводимо такі допомі-
жні форми:
ЕSm | |
|
, ,
,
x y y x
x y
− −
−
= =
= Σ
Σ
;
ЕTr | | |
| |
, , ,
, ,
x y y z x z
x y y z
− − −
− −
= = =
= = Σ
Σ
.
Для врахування аксіом заміни рів-
них вводимо такі допоміжні форми:
|–ЕPs
, ,
| | , | ,
,
| | ,
, ( ), ( ),
, ( ),
z u z u
a v b v
z u
a v
a b R p R p
a b R p
− − −
− −
=
= Σ
Σ
;
–|ЕPs
, ,
| | , | ,
,
| | ,
, ( ), ( ),
, ( ),
z u z u
a v b v
z u
a v
a b R p R p
a b R p
− − −
− −
=
= Σ
Σ
.
Секвенційні числення із такими ба-
зовими формами назвемо QЕCl-численнями.
Побудова секвенційного дерева.
Процедура побудови секвенційного дерева
мусить враховувати, що значення предика-
та P(d) може бути різним залежно від того,
входить чи не входить до d компонента з
певним предметним іменем. Тому при за-
стосуванні –|∃ та –|∃R-форм приклади для
формул вигляду –|∃xΦ та –| (u
v )R x∃ Φ мо-
жуть мати тільки вигляд –| ( )x
yR Φ та
–|
,
, ( ),u x
v yR Φ де у – означене. Отже, при за-
стосуванні –|∃ та –|∃R-форм треба перебра-
ти всі можливі розподіли наявних предме-
тних імен на означені й неозначені. Це
можна реалізувати побудовою відповідних
розгалужень секвенційного дерева: якщо у
вершині Ξ маємо перше на етапі застосу-
вання –|∃ чи –|∃R-форми, нехай це буде до
формули –|∃xΦ чи –| (u
v ),R x∃ Φ то для Ξ бу-
дується багато вершин-"сестер", які є безпо-
середніми предками Ξ, мають одну й ту ж
множину наявних імен та відрізняються
лише різними множинами означених імен і
відповідними множинами прикладів вигля-
ду –| ( )x
yR Φ чи –|
,
, ( ),u x
v yR Φ де у – означене.
Поетапна процедура побудови де-
рева для секвенції Σ починається з кореня
дерева. Кожне застосування секвенційної
форми проводиться до скінченної множи-
ни доступних на даний момент формул. На
початку кожного етапу виконується крок
доступу. Це означає, що до списку доступ-
них формул додаємо по одній формулі зі
списку |–-формул та списку –|-формул. Якщо
в секвенції немає недоступних |–-формул
чи –|-формул (відповідний список вичер-
пано), то на подальших кроках доступу до-
даємо по одній формулі невичерпаного спи-
ску. На початку побудови дерева доступна
лише пара перших формул списків (або
єдина |–-формула чи –|-формула, якщо один
зі списків порожній). Перед побудовою де-
рева для Σ зафіксуємо деякий нескінченний
список TN "нових" тотально строго неісто-
тних імен такий: що імена із TN не зустрі-
чаються у формулах секвенції Σ.
Із кожною вершиною пов’язуємо
множини наявних та означених предмет-
них імен. Множина наявних імен – це
множина імен усіх формул, які доступні на
шляху від кореня до даної вершини. Мно-
жина означених імен явно виділяється ли-
ше на шляхах, де були хоч раз застосовані
–|∃-форми. Усі тотально строго неістотні
імена, введені |–∃ та |–∃R-формами на шля-
ху від кореня до даної вершини, гаранто-
вано означені.
Нехай виконано k етапів процедури.
На етапі k+1 перевіряємо, чи буде кожен з
листів дерева замкненою секвенцією (бе-
ремо до уваги тільки доступні формули сек-
венцій). Якщо всі листи замкнені, то про-
цедура завершена позитивно, отримано
замкнене секвенційне дерево. Якщо ні, то
для кожного незамкненого листа ξ робимо
наступний крок доступу, після чого добу-
довуємо скінченне піддерево з вершиною
ξ наступним чином.
Ативізуємо всі доступні (окрім при-
30
Теоретичні та методологічні основи програмування
мітивних) формули ξ. Далі по черзі до ко-
жної активної формули застосовуємо від-
повідну секвенційну форму.
Секвенційні форми типів RT, ΦN,
R∃R, R∃p допоміжні: перед застосуванням
інших, основних секвенційних форм, усу-
ваємо, у разі наявності, тотожні перейме-
нування та пари імен реномінацій за неіс-
тотним чи квантифікованим верхнім іме-
нем, застосовуючи належну кількість разів
зазначені допоміжні форми.
Спочатку виконуємо всі |–∃ та |–∃R-
форми. Застосування такої форми додає
нове тотально неістотне ім’я у до множини
означених імен вершини, таке у беремо як
перше незадіяне на даному шляху від
кореня ім’я зі списку TN. Ім’я у гарантова-
но означене, додаємо його до множин на-
явних та означених імен. Після цього до
кожної з решти активних формул застосо-
вуємо відповідну форму – одну з форм ти-
пів RR, R¬, R∨, ¬, ∨. Вони не змінюють
множини наявних та означених імен. Далі
застосовуємо –|∃ та –|∃R-форми. Це робимо
таким чином.
Якщо першим застосуванням форми
елімінації квантора на шляху від кореня до
даної вершини була –|∃ чи –|∃R-форма, то на
цьому шляху ще не було виділення означе-
них та неозначених імен. Нехай в даній
вершині маємо множину Z наявних імен
(імена доступних формул). Тоді, застосо-
вуючи цю форму (–|∃R до –| (u
v )R x∃ Φ чи
–|∃ до –|∃xΦ), із даної вершини будуємо скін-
ченне розгалуження дерева. Для цього роз-
глядаємо всі можливі розподіли імен Z на
означені (утворюють множину Y ⊆ Z) та не-
означені (утворюють множину Z\Y). Для ко-
жної Y ⊆ Z будуємо безпосереднього предка
даної вершини-секвенції, додаючи приклади
–| ( )x
yR Φ чи –|
,
, ( )u x
v yR Φ для кожного z∈Y.
Для вершини-предка із Y = ∅ беремо (зі спи-
ску TN) нове тотально строго неістотне t та
додаємо приклад вигляду –| ( )x
tR Φ чи
|
,
, ( );u x
v tR Φ для такої вершини-предка t –
означене, Z – множина неозначених, {t}∪Z –
множина наявних імен.
Нехай на шляху від кореня до даної
вершини –|∃ чи –|∃R-форма застосовується
вперше, проте на шляху вже були застосу-
вання |–∃ чи |–∃R-форм. Тоді в даній вер-
шині вже виділено множину W означених
імен (вони тотально неістотні гарантовано
означені). Нехай X – множина всіх інших
наявних імен, вони ще не розподілені на
означені та неозначені (W∪X – множина
наявних імен вершини). Розглядаючи все-
можливі розподіли імен X на означені (утво-
рюють Y ⊆ X) та неозначені (утворюють X\Y),
для кожної Y ⊆ Z будуємо безпосереднього
предка даної вершини-секвенції, додаючи
приклади для кожного z∈ W∪Y.
Нехай –|∃ чи –|∃R-форма застосову-
ється вперше на етапі, проте на шляху від
кореня до даної вершини вже були засто-
сування таких форм. Це означає, що в да-
ній вершині виділено множини W означе-
них та U неозначених імен. Нехай на поча-
тку етапу після виконання кроку доступу
до множини наявних імен було додано
множину X імен нових доступних формул;
до першого виконання на даному етапі –|∃
чи –|∃R-форми імена X не розподілені на
означені й неозначені (проте від початку
етапу можливе розширення множини озна-
чених імен); тоді W∪U∪X – множина наяв-
них імен вершини. Розглядаючи всеможливі
розподіли імен X на означені й неозначені,
для кожної Y ⊆ X будуємо безпосереднього
предка даної вершини, додаючи в ньому
приклади для кожного z∈W∪Y.
Нехай застосування –|∃ чи –|∃R-
форми – це не перше застосування на етапі
форми такого типу. Тоді в даній вершині
виділено множини W означених та U не-
означених імен, а нерозподілених імен не-
має, тобто W∪U – множина наявних імен
вершини. Тоді добудовуємо єдиного безпо-
середнього предка даної вершини-секвенції,
додаючи приклади для кожного z∈W (фак-
тично додаємо приклади для нових озна-
чених на даному етапі імен).
Для врахування аксіом рівності піс-
ля кожного застосування базової форми
кванторного рівня при потребі робимо на-
ступні додаткові кроки.
Нехай на попередньому кроці була
отримана формула |–a = b, або |–a = b стала
доступною на початку етапу. Тоді за до-
помогою ЕSm додаємо |–b = a. При появі
31
Теоретичні та методологічні основи програмування
|–a = b та |–b = с за допомогою форми ЕTr
додаємо |–a = с; фактично, враховуючи
ЕSm, це означає, що до наявних |–a = b,
|–b = a, |–b = с, |–с = b додаємо |–a = с, |–с = a.
Після отримання |–a = b (фактично
вже маємо |–a = b та |–b = a) далі, використо-
вуючи форми типу ЕPs, для кожної наявної
доступної формули вигляду |–
,
, ( )z u
a vR p до-
даємо |–
,
, ( ),z u
b vR p для кожної наявної досту-
пної –|
,
, ( )z u
a vR p додаємо –|
,
, ( )z u
b vR p . Так ро-
бимо багатократно належну кількість ра-
зів. Наприклад, маючи |–a = b, |–b = a та
|–c = d, |–d = c, за появою |–
, ,
, , ( )z t u
a c vR p додаємо
|–
, ,
, , ( )z t u
b c vR p , |– , ,
, , ( )z t u
a d vR p , |– , ,
, , ( )z t u
b d vR p .
Після виконання основної секвен-
ційної форми формула пасивна. До пасив-
них та утворених на даному етапі формул
базові форми не застосовуються. Всі по-
втори специфікованих формул у секвенції
усуваємо.
При побудові секвенційного дерева
можливі такі випадки:
1) процедуру завершено позитивно,
маємо скінченне замкнене дерево;
2) процедуру завершено негативно,
маємо скінченне незамкнене дерево;
3) процедура не завершується, має-
мо нескінченне секвенційне дерево. За ле-
мою Кеніга [2] нескінченне дерево зі скін-
ченним розгалуженням має хоча б один
нескінченний шлях.
У випадках 2) і 3) у дереві існує
скінченний або нескінченний незамкнений
шлях ℘, вершини якого не можуть бути
замкненими секвенціями, адже до замкне-
ної секвенції незастосовна жодна форма, і
процес побудови дерева для цього шляху
обривається. Кожна з формул секвенції Σ
зустрінеться на ℘ і стане доступною.
Коректність та повнота QECl-чис-
лень. Нехай для секвенції |–Γ–|Δ побудова-
не замкнене дерево. Із вищенаведеної про-
цедури побудови секвенційного дерева ви-
пливає, що для кожної його вершини |–Λ–|Κ
з множинами означених імен W та неозна-
чених імен U справджується Λ A, W–U |= Κ
для кожної моделі мови A.
Для листів дерева це випливає з ви-
значень замкненої та U-замкненої секвен-
цій.
Збереження секвенційними форма-
ми вищезазначеного відношення логічного
наслідку (від засновків до висновків) ви-
конується для допоміжних форм типу RT,
ΦN, R∃R, R∃p та форм типу ¬, ∨, RR, R¬,
R∨, ΦN, а також допоміжних форм для рі-
вності ЕSm, ЕTr, ЕPs. Це випливає із від-
повідних властивостей відношення |= , а
також відповідних властивостей рівності.
Для форм |–∃ i |–∃R таке збереження випли-
ває з теореми 14.
Для –|∃ та –|∃R збереження відповід-
них відношень логічного наслідку при русі
до вершини Σ, яка містить активну форму-
лу вигляду –|∃xΦ чи –| (u
v ),R x∃ Φ від вер-
шин, які є її безпосередніми предками та
містять відповідні приклади вигляду –
| ( )x
yR Φ чи –|
,
,
u x
v ( )R ,y Φ гарантується теоре-
мами 12 та 13.
Таким чином, для побудованого
QECl-числення справджується
Теорема 15 (коректності). Нехай
секвенція |–Γ–|Δ вивідна. Тоді Γ |= Δ.
Для доведення повноти QECl-чис-
лень опираємося на метод модельних (хін-
тікківських) множин [5].
Нехай Н – множина специфікова-
них формул із виділеною множиною озна-
чених імен W ⊆ nm(Н); тоді U = nm(Н) \ W –
множина її неозначених імен.
Множину Н назвемо модельною,
якщо виконуються відомі [7] умови НС,
НСU, НRT, НΦN, Н¬, Н∨, НR¬, НR∨, Н∃,
а також умови НR∃R, НR∃p, Н∃R та умови
для рівності НСЕ, НЕS, НЕT, НЕP.
Наведемо тут умови НСЕ, НЕS,
НЕT, НЕP та НR∃R, НR∃p, Н∃, Н∃R:
НСЕ) жодна формула вигляду –| x = x
не може належати до Н;
НЕS) якщо |– x = y∈Н, то |– y = x∈Н;
НЕT) якщо |– x = y∈Н тa |– y = z∈Н, то
|– x = z∈Н;
НЕP) якщо |– x = y∈Н тa
|–
,
, ( )z u
y vR p ∈Н, то |– ,
, ( )z u
x vR p ∈Н;
якщо |– x = y∈Н тa –|
,
, ( )z u
y vR p ∈Н, то
32
Теоретичні та методологічні основи програмування
–|
,
, ( )z u
x vR p ∈Н;
НR∃R) якщо |– ,
, ( )u x
v yR x∃ Φ ∈Н, то
|– ( )u
vR x∃ Φ ∈Н; якщо –|
,
, ( )u x
v yR x∃ Φ ∈Н, то
–| ( )u
vR x∃ Φ ∈Н;
НR∃p) якщо |– ( )x
yR x∃ Φ ∈Н, то
|–∃хΦ∈Н; якщо –| ( )x
yR x∃ Φ ∈Н, то –|∃хΦ∈Н;
Н∃) якщо |–∃хΦ∈Н, то існує у∈W
таке, що |– ( )x
yR Φ ∈Н; якщо –|∃хΦ∈Н, то
–| ( )x
yR Φ ∈Н для всіх у∈W;
Н∃R) якщо |– ( )u
vR x∃ Φ ∈Н, то існує
у∈W таке, що |–
,
, ( )u x
v yR Φ ∈Н; якщо
–| ( )u
vR x∃ Φ ∈Н, то –|
,
, ( )u x
v yR Φ ∈Н для
всіх у∈W.
Теорема 16. Нехай ℘ – незамкне-
ний шлях у секвенційному дереві, Н –
множина всіх специфікованих формул
секвенцій цього шляху. Тоді існують АС
A = (A, I) та δ∈VA такі:
1) |–Φ∈Н ⇒ ΦА(δ) = Т ;
2) –|Φ∈Н ⇒ ΦА(δ) = F.
Те, що множина Н – модельна, до-
водимо традиційним способом (подібне
доведення див., напр., [4, 9]).
Нехай W – множина всіх означених
предметних імен, що фігурують у Н.
Рівність індукує на W відношення
еквівалентності: x ∼ y ⇔ |– x = y∈Н.
Нехай A = ~
W – фактор-множина
множини W за відношенням ~. Позначимо
як [v] клас еквівалентності з представни-
ком v. Визначимо δ = [va[v] | v∈W ]. Таке
відображення δ є сюр'єкцією W→А.
Задамо значення базових предика-
тів на δ та на ІМ вигляду r v
x (δ).
Якщо |– x = y∈Н, то x ∼ y, тому
(x = y)А(δ) = T за побудовою δ.
Якщо |– р∈Н, то задамо рА(δ) = Т;
якщо –| р∈Н, то задамо рА(δ) = F.
Якщо |–
v
xR (р)∈Н, то рА(r v
x (δ)) = Т;
якщо –|
v
xR (р)∈Н, то рА(r v
x (δ)) = F.
В усіх інших випадках значення ба-
зових предикатів задаємо довільним чи-
ном, беручи до уваги обмеження щодо
строго неістотності: для всіх d, h∈VA та-
ких, що d║–ν(p) = h║–ν(p), необхідно
рA(d) = рA(h). Це гарантує, що імена у∈ν(p)
строго неістотні для рА.
Далі доведення ведеться індукцією
за складністю формули згідно з побудовою
модельної множини.
Для атомарних формул і формул ви-
гляду ( )v
xR p твердження 1) та 2) теореми
випливають із визначення значень базових
предикатів. Крок індукції для тверджень 1)
та 2) доводиться стандартним чином, ана-
логічне доведення див. [4, 9].
На основі теореми 16 отримуємо
теорему повноти для QECl-числень.
Теорема 17 (повноти). Нехай Γ |= Δ.
Тоді секвенція |–Γ–|Δ вивідна.
Теорема повноти доводиться тради-
ційним способом, доведення аналогічних
теорем див. [4, 9].
Висновки
Досліджено першопорядкові компо-
зиційно-номінативні логіки часткових од-
нозначних, тотальних неоднозначних та
часткових неоднозначних квазіарних пре-
дикатів кванторно-екваційного рівня. Опи-
сано мови і семантичні моделі цих логік,
розглянуто різні формалізації відношення
логічного наслідку. Наведено основні се-
мантичні властивості таких логік, зокрема,
властивості відношень логічного наслідку
для множин формул, Х–Y-означених відно-
шень логічного наслідку. На цій основі для
логік однозначних квазіарних предикатів
кванторно-екваційного рівня побудовано
числення секвенційного типу, доведено
коректність та повноту цих числень.
1. Handbook of Logic in Computer Science. Ed-
ited by S. Abramsky, Dov M. Gabbay and
T. S. E. Maibaum. – Oxford Univ. Press. –
Vol. 1–5, 1993–2000.
2. Клини С. Математическая логика. – М.,
1973. – 480 с.
33
Теоретичні та методологічні основи програмування
3. Никитченко Н.С. Композиционно-номина-
тивный подход к уточнению понятия
программы // Проблеми програмування. –
1999. – № 1. – С. 16–31.
4. Нікітченко М.С., Шкільняк С.С. Матема-
тична логіка та теорія алгоритмів. – К.,
2008. – 528 с.
5. Смирнова Е.Д. Логика и философия – М.,
1996. – 304 с.
6. Шкільняк С.С. Відношення логічного нас-
лідку в композиційно-номінативних логі-
ках // Проблеми програмування. – 2010. –
№ 1. – C. 15–38.
7. Шкильняк С.С. Логики квазиарных преди-
катов первого порядка // Кибернетика и
системный анализ. – 2010. – № 6. –
С. 32–49.
8. Шкільняк С.С. Спеціальні відношення ло-
гічного наслідку в логіках квазіарних пре-
дикатів // Проблеми програмування. –
2011. – № 4. – C. 36–48.
9. Шкільняк С.С. Секвенційні числення пер-
шопорядових логік однозначних квазіарних
предикатів // Проблеми програмування. –
2012. – № 1. – C. 34–51.
10. Нікітченко М.С., Шкільняк С.С. Компози-
ційно-номінативні логіки кванторно-еква-
ційного рівня // Вісник Київського ун-ту.
Серія: кібернетика. – 2011. – Вип. 11. –
C. 32–40.
Одержано 10.02.2012
Про авторів:
Нікітченко Микола Степанович,
доктор фізико-математичних наук,
завідувач кафедри теорії та технології
програмування,
Шкільняк Степан Степанович,
доктор фізико-математичних наук,
доцент кафедри теорії та технології
програмування.
Місце роботи авторів:
Київський національний університет
імені Тараса Шевченка,
01601, Київ,
вул. Володимирська, 60.
Тел.: (044) 259 0519,
(044) 522 0640 (д)
e-mail: ttp@unicyb.kiev.ua
34
|
| id | pp_isofts_kiev_ua-article-104 |
| institution | Problems in programming |
| keywords_txt_mv | keywords |
| language | Ukrainian |
| last_indexed | 2025-07-17T09:32:50Z |
| publishDate | 2015 |
| publisher | PROBLEMS IN PROGRAMMING |
| record_format | ojs |
| resource_txt_mv | ppisoftskievua/38/d2696b22848d7fe7935bc86634732a38.pdf |
| spelling | pp_isofts_kiev_ua-article-1042018-10-02T21:09:26Z Logics of quasiary predicates of quantifier-equational level Логики квазиарных предикатов кванторно-эквационального уровня Логіки квазіарних предикатів кванторно-екваційного рівня Nikitchenko, M.S. Shkilniak, S.S. Composition-nominative logics Композиционно-номинативные логики Композиційно-номінативні логіки First-order composition-nominative logics of partial single-valued, total multiple valued and partial multiple-valued quasiary predicates of quantifierequational level are studied. We define basic semantic properties of the introduced logics, particularly the properties of the relations of logical consequence for sets of formulas and the Х–Y-valued relations of logical consequence. On this basis we construct sequent calculi for logics of single-valued quasi-ary predicates of quantifier-equational level. Исследованы первопорядковые композиционно-номинативные логики частичных однозначных, тотальных неоднозначных и частичных неоднозначных квазиарных предикатов кванторно-эквационального уровня. Приведены основные семантические свойства таких логик, в частности, свойства отношений логического следствия для множеств формул, Х–Y-означенных отношений логического следствия. На этой основе для логик однозначных квазиарных предикатов кванторно-эквационального уровня построены исчисления секвенциального типа. Досліджено першопорядкові композиційно-номінативні логіки часткових однозначних, тотальних неоднозначних та часткових неоднозначних квазіарних предикатів кванторно-екваційного рівня. Наведено основні семантичні властивості таких логік, зокрема, властивості відношень логічного наслідку для множин формул, Х–Y-означених відношень логічного наслідку. На цій основі для логік однозначних квазіарних предикатів кванторно-екваційного рівня побудовано числення секвенційного типу. PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2015-09-22 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/104 PROBLEMS IN PROGRAMMING; No 4 (2012) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 4 (2012) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 4 (2012) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/104/104 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| spellingShingle | Composition-nominative logics Nikitchenko, M.S. Shkilniak, S.S. Logics of quasiary predicates of quantifier-equational level |
| title | Logics of quasiary predicates of quantifier-equational level |
| title_alt | Логики квазиарных предикатов кванторно-эквационального уровня Логіки квазіарних предикатів кванторно-екваційного рівня |
| title_full | Logics of quasiary predicates of quantifier-equational level |
| title_fullStr | Logics of quasiary predicates of quantifier-equational level |
| title_full_unstemmed | Logics of quasiary predicates of quantifier-equational level |
| title_short | Logics of quasiary predicates of quantifier-equational level |
| title_sort | logics of quasiary predicates of quantifier-equational level |
| topic | Composition-nominative logics |
| topic_facet | Composition-nominative logics Композиционно-номинативные логики Композиційно-номінативні логіки |
| url | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/104 |
| work_keys_str_mv | AT nikitchenkoms logicsofquasiarypredicatesofquantifierequationallevel AT shkilniakss logicsofquasiarypredicatesofquantifierequationallevel AT nikitchenkoms logikikvaziarnyhpredikatovkvantornoékvacionalʹnogourovnâ AT shkilniakss logikikvaziarnyhpredikatovkvantornoékvacionalʹnogourovnâ AT nikitchenkoms logíkikvazíarnihpredikatívkvantornoekvacíjnogorívnâ AT shkilniakss logíkikvazíarnihpredikatívkvantornoekvacíjnogorívnâ |