Спектр логік часткових предикатів, орієнтованих на композиційнo-номінативні моделі програм

Критерій неістотності предметних імен для ЧКНЛ еквітонних предикатів дає

Теорема 3.2. Ім'я xV неістотне для формули |= x.

Неістотні імена дозволяють перейменування квантифікованих імен. В загальному випадку це гарантує теорема 3.3S, для еквітонних предикатів -теорема 3.3:

Теорема 3.3. Нехай уV неістотне для . Тоді |= xу.

Теорема 3.3S. Нехай уV строго неістотне для . Тоді x TFу.

Наведемо властивості формул, пов'язані з кванторами та реномінаціями.

NRS) хTF при х{} - строга неістотність верхніх імен.

RS) R(xФ) TF xR(Ф) при x{} - обмежена R-дистрибутивність.

RZS) TF для довільного уV, якщо х строго неістотне для Ф.

Для випадку логіки еквітонних предикатів маємо також властивості:

R) |= R(xФ) xR(Ф) при x{}.

RZ) |= для довільного уV, якщо |=ФxФ.

Rх) |= v1...vnФ.

Для пронесення через х, якщо умова x{} не виконується, треба спочатку замінити хФ на z, де z{} та z (строго) неістотне для Ф. Тому для виконання еквівалентних перетворень довільних формул треба мати достатній запас імен, (строго) неістотних для кожного рPs, - тотально (строго) неістотних імен.

Таким чином, для семантичних моделей КНЛ вимагаємо наявності нескінченної множини (строго) тотально неістотних предметних імен. Предметні імена, (строго) неістотність яких постулюється, називають синтетично (строго) неістотними. В загальному випадку логіки квазіарних предикатів для кожного рPs множину таких імен задамо за допомогою тотальної : Ps2V. Таку функцію продовжимо до : Fr2V :

() = (Ф); () = ()(); (x) = (){x};

= ((){v1,...,vn})(V\{xi | vi(), i{1,…, n}}).

Множина VTs = тотально строго неістотних імен має бути нескінченною.

Для логіки еквітонних предикатів множини синтетично неістотних імен задаємо за допомогою тотальної : Ps2V, яку аналогічно функції продовжуємо до : Fr2V . Множина VT = тотально неістотних імен має бути нескінченною.

Кожне х() строго неістотне для формули . Кожне х() неістотне для .

Далі розглядаються класичноподібні нормальні форми формул ЧКНЛ.

Формула Ш (cтрого) нормальна, якщо всі символи реномінації Ш застосовані тільки до предикатних символів, і всі входження кванторних префіксів у Ш - по різних тотально (cтрого) неістотних іменах. Доводиться (теореми 3.6 та 3.6S):

- для кожної можна збудувати нормальну формулу Ш таку: |= Ш.

- для кожної можна збудувати строго нормальну формулу Ш таку: TF Ш.

У випадку логіки еквітонних предикатів для кожної формули можна побудувати квазізамкнену нормальну формулу таку, що |= |= (теорема 3.7).

Визначаються поняття (строго) варіанти і (строго) С-варіанти, доводяться теореми про (строго) варіанту і (строго) С-варіанту.

Вводяться прeнeкснi опeрацiї над формулами, доводяться твердження про побудову для кожної формули еквівалентної їй пренексної формули.

В підрозділі 3.2 досліджуються композиційно-номінативні логіки кванторно-екваційного рівня. Визначаються семантичні моделі, описується мова таких логік. Для цих логік успадковуються семантичні властивості ЧКНЛ. Зокрема, це теореми еквівалентності, заміни еквівалентних, про розширення, критерії неістотності предметних імен, теореми про нормальні форми, про варіанти і С-варіанти, пренексну форму. Водночас з'являються нові властивості, пов'язані з предикатами рівності =xy.

В підрозділі 3.3 вивчаються КНЛ функціонального рівня - функціональні композиційно-номінативні логіки (ФКНЛ). Визначаються семантичні моделі, описується мова таких логік. Для ФКНЛ успадковуються семантичні властивості логік кванторного рівня. Зокрема, це теореми еквівалентності та заміни еквівалентних, теорема про розширення, критерій неістотності предметних імен для формул.

Наводяться спеціальні властивості формул ФКНЛ, пов'язані із суперпозицією.

Подібно випадку ЧКНЛ, визначаються множини синтетично неістотних і строго неістотних, тотально неістотних і тотально строго неістотних предметних імен.

Визначаються та досліджуються класичноподібні нормальні форми в ФКНЛ.

Формула Ш (строго) нормальна, якщо усі символи суперпозиції формули Ш застосовані тільки до функціональних чи предикатних символів, а всі входження кванторних префіксів у Ш - по різних (строго) тотально неістотних іменах.

Доводиться, що для кожної можна збудувати нормальну (строго нормальну) Ш таку, що |= Ш (відповідно TF Ш).

У випадку ФКНЛ еквітонних предикатів для кожної можна збудувати квазізамкнену нормальну таку, що |= |= .

Для ФКНЛ вводиться поняття пренексної форми, визначаються пренексні операції. Доводиться можливість зведення формул до пренексної форми.

В підрозділі 3.4. досліджуються КНЛ функціонально-екваційного рівня - функціонально-екваційні композиційно-номінативні логіки (ФЕКНЛ).

Семантичними моделями ФЕКНЛ є композиційні системи квазіарних функцій і предикатів (VА, FnAPrA, C), де C визначена базовими композиціями , , S, 'x, x, =. Алфавіт мови ФЕКНЛ складається з множин V, Dns, Fns, Ps предметних імен, деномінаційних, функціональних, предикатних символів та символів базових композицій , , x, , =. Множини Тr термів та Fr формул мови вводимо індуктивно.

Т1. Кожний деномінаційний та функціональний символ є (атомарним) термом.

Т2. Нехай t, t1,..., tn - терми. Тоді t1...tn - терм.

1. Кожний предикатний символ є (атомарною) формулою.

2. Нехай t та s - терми. Тоді =ts - формулa.

3. Нехай - формулa, t1,..., tn - терми. Тоді t1...tn - формулa.

4. Нехай та - формули. Тоді , Ф, x - формули.

Моделі мови ФЕКНЛ - АС з доданою сигнатурою ((A, FnAPrA), I), Вони пов'язують мову ФЕКНЛ із АС даних. Тотальне однозначне I : FsРsFnAPrA, де I('v) = 'v для 'vDns, природним чином визначає відображення J : FrТrFnAРrА.

Для ФЕКНЛ успадковуються семантичні властивості логік кванторного та функціонального рівнів. З'являються нові специфічні властивості, пов'язані з рівністю. Зокрема, це теорема 3.10 рівності, критерій неістотності предметних імен для термів:

Теорема 3.11. хV неістотне для терма |= у( = , 'y)) |= ( = , 'y)).

За допомогою функцій : Tr Fr2V та : Tr Fr2V визначаються множини синтетично неістотних і строго неістотних, тотально неістотних і тотально строго неістотних предметних імен. Доводиться (теореми 3.9, 3.9S): кожне х(g) строго неістотне для терма чи формули g, кожне х(g) неістотне для терма чи формули g.

Далі розглядаються нормальні, стандартні нормальні та квазізамкнені нормальні форми в ФЕКНЛ. Доводиться (теореми 3.13, 3.13S): для кожної можна збудувати нормальну (стандартну нормальну) формулу Ш таку, що |= Ш; для кожної можна збудувати строго нормальну (стандартну строго нормальну) формулу Ш таку, що TF Ш. У випадку логіки еквітонних предикатів для кожної формули можна збудувати квазізамкнену нормальну формулу таку, що |= |= (теорема 3.14).

Для ФЕКНЛ доведені теореми, які узагальнюють відповідні теореми класичної логіки: про С-варіанту, строго С-варіанту, зведення формул до пренексної форми.

В підрозділі 3.5 досліджуються гомоморфізми неокласичних АС з доданою сигнатурою. Для таких АС вводяться поняття гомоморфізму, повного, сюр'єктивного, сильного гомоморфізму, ізоморфізму, -позитивних та позитивних формул. Для неокласичних АС з еквітонними функціями і предикатами доводяться теореми про гомоморфізми та ізоморфізми. Вони узагальнюють відповідні теореми класичної логіки.

Для АС із повнототальними еквітонними функціями і предикатами справджується

Теорема 3.15. Нехай : А>В - гомоморфізм АС A в АС B. Тоді:

1) для кожних терма t сигнатури та dVA маємо (tA(d)) tB((d));

2) для кожної -позитивної формули сигнатури для довільних dVA, якщо A(d) = Т та B((d)), то B((d)) = Т.

Наводиться приклад 3.4, який засвідчує, що для АС із еквітонними функціями і предикатами при несюр'єктивному стандартне визначення гомоморфізму не зовсім адекватне, теорема 3.15 для таких АС невірна. Тому гомоморфізм треба посилити.

Теорема 3.16. Нехай сюр'єктивне : А>В - гомоморфізм АС A в АС B. Тоді:

1) для кожних терма t сигнатури та dVA маємо (tA(d)) tB((d));

2) для кожної позитивної формули сигнатури для довільних dVA, якщо А(d) = Т та В((d)), то В((d)) = Т.

Теорема 3.17 (про ізоморфізм). Нехай : А>В - ізоморфізм АС A в АС B. Тоді:

1) для кожних терма t сигнатури та dVA маємо (tA(d)) tB((d));

2) для кожних формули сигнатури та dVА маємо A(d) B((d)).

В підрозділі 3.6 вивчаються властивості відношення логічного наслідку для множин формул КНЛ першого порядку. Наводяться властивості такого відношення кванторного, функціонального, функціонально-екваційного рівнів. Ці властивості є семантичною основою побудови секвенційних числень відповідних рівнів.

Далі розглядаються питання семантичної несуперечливості множин формул.

В підрозділі 3.7 досліджуються розширення логік еквітонних предикатів - логіки локально-еквітонних предикатів та логіки еквісумісних і локально-еквісумісних предикатів, які визначені на даних з неповною інформацією.

V-квазіарний предикат Р на A локально-еквітонний, якщо для довільних d, d'VA з умов P(d), d d' та d' \d скінченна, випливає Р(d') = Р(d).

V-IM d та d' сумісні, якщо функція dd' однозначна. Це позначимо d d'.

Предикат Р еквісумісний (ЕСП), якщо для довільних d, d'VA із d d', Р(d) та Р(d') випливає Р(d) = Р(d').

Предикат Р локально-еквісумісний (ЛЕСП), якщо для довільних d, d'VA таких, що (d' \d)(d \d') скінченна, із d d', Р(d) та Р(d') випливає Р(d) = Р(d').

Теорема 3.24. 1. Кожний ЕСП можна розширити до еквітонного.

2. Кожний ЛЕСП можна розширити до локально-еквітонного.

Доводиться (теореми 3.25, 3.25), що композиції , , R, x зберігають локально-еквітонність, еквісумісність та локально-еквісумісність V-квазіарних предикатів.

Теорема 3.26. Для кожної АС із еквісумісними (локально-еквісумісними) предикатами A = (А, IА) можна збудувати систему еквітонних (локально-еквітонних) розширень B = (А, IB). При цьому для кожної формули предикат В є еквітонним (локально-еквітонним) розширенням відповідного A.

Властивості логік локально-еквітонних, еквісумісних і локально-еквісумісних предикатів аналогічні відповідним властивостям логік еквітонних предикатів.

В четвертому розділі збудовано та досліджено формально-аксіоматичні системи гільбертівського типу для першопорядкових логік повнототальних еквітонних предикатів кванторного, кванторно-екваційного, функціонально-екваційного рівнів - чисті, чисті з рівністю, функціонально-екваційні неокласичні числення. Логічні аксіоми та правила виведення цих числень відображають закони композиційної предикатної алгебри відповідного рівня. Наведено приклади виведень в таких численнях, сформульовано та доведено теорему дедукції.

Доведено синтаксичні варіанти семантичних теорем третього розділу, зокрема, теорем еквівалентності, рівності, про неістотність предметних імен, про нормальні форми. Для побудованих числень доведені теореми коректності та повноти.

Отримані результати узагальнюють відповідні твердження класичної логіки.

В підрозділі 4.1 будуються числення для КНЛ кванторного рівня - чисті неокласичні числення. Таке числення визначається як трійка T = (L, Ax, P), де L - мова логіки із заданою множиною формул Fr, Ax Fr - множина аксіом, P - множина правил виведення. Ax розбита на множини Aлог логічних аксіом і Aвл власних аксіом.

Множина Aлог задається такими схемами аксіом:

АхПР) Ах) xyyx

АхRx) v1...vnФ АхR) R() R()

АхR) R() R() R() АхRR) R(R()) R()

АхRТ) АхN) xxx

АхR) (x) x(), x{} АхNR) , х z

АхNР) px p - записані для всіх рPs, ці аксіоми визначають множини (p).

Множина P складається з відомих пропозиційних правил розширення, скорочення, асоціативності, перетину П1-П4, та кванторних правил:

П5) , x |- x П6) ФуФ |-

Модель мови A = (A, I) назвемо моделлю числення T, якщо кожна аксіома числення T істинна при інтерпретації на A.

Формула Ф істинна в численні T (T|= Ф), якщо Ф істинна на кожній його моделі.

Теорема істинності (коректності). Якщо T |- Ф, то T |= Ф.

Далі розглядаються приклади виведень в чистих неокласичних численнях. Для цих числень формулюється і доводиться теорема дедукції (теорема 4.3), доводяться синтаксичні варіанти семантичних тверджень про неістотність предметних імен та про нормальні форми. Доводиться теорема повноти чистих неокласичних числень:

Теорема 4.9. Для кожної формули числення T з умови T |= випливає T |- .

Ідея доведення полягає в моделюванні виведення квазізамкненої нормальної формули в численні T шляхом побудови виведення аналогічної їй формули класичної логіки ' у відповідній теорії першого порядку та навпаки.

Числення КНЛ повнототальних еквітонних предикатів кванторно-екваційного рівня можна трактувати як прикладні чисті неокласичні числення, у яких до множини власних аксіом входять спеціальні аксіоми рефлексивності рівності та рівності для формул. Для таких числень справджуються теореми коректності й повноти.

В підрозділі 4.2 будуються числення для КНЛ повнототальних еквітонних предикатів функціонально-екваційного рівня. Наводяться логічні аксіоми і правила виведення таких числень, розглядаються приклади виведень, формулюється і доводиться теорема дедукції (теорема 4.12). Для цих числень справджуються синтаксичні аналоги розглянутих у розділі 3 семантичних теорем. Це, зокрема, теореми рівності й еквівалентності, теореми про властивості, пов'язані з неістотними предметними іменами, теореми про варіанту, про нормальні форми. Для функціонально-екваційних неокласичних числень доводяться теореми коректності та повноти (теорема 4.15).

В п'ятому розділі будуються формально-аксіоматичні системи ґенценівського типу - секвенційні числення - для першопорядкових неокласичних логік кванторно-екваційного функціонального та функціонально-екваційного рівня. Семантичною основою побудови є властивості відношення логічного наслідку для множин формул логіки відповідного рівня. Розглядаються різні варіанти таких числень.

Досліджено властивості збудованих числень, для них доведені теореми коректності та повноти. Отримано важливі наслідки теореми повноти, зокрема, теорема компактності, теорема про існування моделі. Із використанням збудованих числень для логік еквітонних квазіарних предикатів доведено інтерполяційну теорему. На її базі для цих логік доведено теореми про визначність. Отримані результати узагальнюють відомі результати класичної логіки, зокрема, такі, як теорема компактності та її наслідки, інтерполяційна теорема Крейга, теорема Бета про визначність.

В підрозділі 5.1 збудовані секвенційні числення неокласичних логік кванторного рівня. Розглядаються QBN-числення, орієнтовані на різнокванторні секвенційні форми, та QZN-числення для секвенцій без обмежень різнокванторності.

Наведемо базові секвенційні форми QZN-числень.

|- -| |- -|

|-RT -|RT |-RR -|RR

|-R -|R |-R -|R

|-N при умові у(A) -|N при умові у(A)

|-R при умові y{} -|R при умові y{}

|-R -|R

Для |-R та -|R умови: y{}, zVT (тотально неістотне) та znm((А)).

|- при умові уVT та упт(, А) -|

Теорема 5.2 (коректності). Нехай секвенція |--| вивідна. Тоді |= .

Далі описується процедура побудови секвенційного дерева в QZN-численнях.

Для доведення повноти секвенційних числень використовується метод модельних (хінтікківських) множин. Дається визначення модельної множини специфікованих формул. Доводиться теорема про побудову контрмоделі за незамкненим шляхом:

Теорема 5.3. Нехай - незамкнений шлях у секвенційному дереві, Н - множина всіх специфікованих формул секвенцій цього шляху, нехай W = nт(Н). Тоді існують АС А = (А, І) з |А| = |W| та VA з im() = W такі, що:

1) |-Н А() = Т ; 2) -|Н А() = F.

Теорема 5.4 (повноти). Нехай |= . Тоді секвенція |--| вивідна.

Секвенційні числення кванторно-екваційного рівня можна розглядати як окремий випадок прикладних числень кванторного рівня. Виведення в прикладному численні з множиною власних аксіом Ах секвенції означає виведення збагаченої секвенції R = {|- | Ах}. Числення кванторно-екваційного рівня трактуємо як прикладні, в яких Ах = {x =xx , xy (=xy =yx ), xyz (=xy =yz =xz )}.

Розглядаються QEBN-числення, які орієнтовані на різнокванторні секвенції, та QEZN-числення, де секвенції не мають обмежень різнокванторності. Формулювання та доведення теорем коректності й повноти для QEBN і QEZN-числень ідентичні формулюванням та доведенням відповідних теорем для QBN і QZN-числень.

В підрозділі 5.2 збудовані секвенційні числення неокласичних логік функціонального рівня. Розглядаються дві різновидності таких числень: FBN-числення, орієнтовані на різнокванторні секвенційні форми, та FZN-числення для секвенцій без обмежень різнокванторності. Наводяться базові секвенційні форми цих числень.

Описується процедура побудови секвенційного дерева в FZN-численнях. Дається визначення модельної множини специфікованих формул. Формулюється та доводиться теорема про побудову контрмоделі за незамкненим шляхом (теорема 5.5).

Формулювання та доведення теорем коректності та повноти для FZN і FBN-числень аналогічне їх формулюванню та доведенню для QZN-числень.

В підрозділі 5.3 будуються секвенційні числення неокласичних логік функціонально-екваційного рівня. Такі числення можна розглядати як окремий випадок прикладних секвенційних числень функціонального рівня, в яких множина власних аксіом складається з таких: x ('x = 'x), xy ('x = 'y 'y = 'x), xyz ('x = 'y 'y = 'z 'x = 'z), xy ('x = 'y (f, 'x, ) =(f, 'y, )), xy ('x = 'y ((p, 'x, ) (p, 'y, )).

Розглядаються FEBN-числення, орієнтовані на різнокванторні секвенційні форми, та FEZN-числення для секвенцій без обмежень різнокванторності. Наводяться базові секвенційні форми таких числень. Описується процедура побудови секвенційного дерева в цих численнях, дається визначення модельної множини.

Формулювання і доведення теорем коректності та повноти для FEZN та FEBN-числень аналогічне їх формулюванню та доведенню для QZN-числень.

В підрозділі 5.4 вивчаються наслідки теореми повноти. В першу чергу, це теорема (принцип) компактності, теорема про існування моделі. Доведені також теореми про еквівалентність синтаксичної та семантичної несуперечливості, про взаємну суперечливість та взаємну несуперечливість множин формул.

Теорема 5.6 (принцип компактності). Нехай |= . Тоді існують скінченні секвенції 0 та 0 такі, що 0 |= 0.

Модель сумісності - це АС A = (А, IА): для деякого dVA А(d) = T для всіх .

Теорема 5.7 (про існування моделі). Нехай синтаксично несуперечлива (кожна секвенція |--|(&) невивідна). Тоді має зліченну або скінченну модель сумісності.

В підрозділі 5.5 для КНЛ еквітонних предикатів доведена інтерполяційна теорема, на основі якої для логік еквітонних предикатів отримані теореми про визначність.

Теорема 5.10 (інтерполяційна). Нехай секвенція -| має виведення. Тоді існує формула сигнатури () ()() така, що секвенції -| та -| мають виведення.

Нехай Ps. Моделі істинності A = (M, IA) та В = (M, IВ) множини формул назвемо -тотожними, якщо для кожного p маємо pA pВ.

Модель істинності - це АС A = (А, IА): для кожних dVA та маємо А(d) T.

Предикатний символ q семантично визначний через предикатні символи {p1, …, pn}, де q{p1, …, pn}, якщо для кожних {p1, …, pn}-тотожних еквітонних моделей істинності A = (M, IA) та В = (M, IВ) множини формул маємо qA qВ.

Предикатний символ q синтаксично визначний через {p1, …, pn} у множині формул , якщо існує формула із () ={p1, …, pn} така, що |= q.

Теорема 5.12. Нехай q синтаксично визначний через {p1,…, pn} у множині формул . Тоді q семантично визначний через {p1,…, pn}.

Теорема 5.13. Нехай q семантично визначний через {p1, …, pn}. Тоді q синтаксично визначний через {p1, …, pn} у множині формул .

В шостому розділі досліджуються нетрадиційні КНЛ. Вивчаються логіки квазіарних предикатів із знятим обмеженням однозначності, для яких пропонуються різні семантики та різні формалізації відношення логічного наслідку. КНЛ квазіарних предикатів є основою для побудови спеціальних логік Це проілюстровано побудовою композиційно-номінативних модальних, транзиційних та темпоральних логік. На базі КНЛ квазіарних предикатів збудовано КНЛ над ієрархічними номінативними даними, для яких характерне використання складних імен.

В підрозділі 6.1 для композиційно-номінативних логік вивчається фундаментальне поняття логічного слідування, яке формалізується за допомогою відношень логічного наслідку. Для пропозиційної логіки нестандартні семантики та різноманітні відношення логічного наслідку запропоновані в роботах О.Д.Смирнової. В дисертаційній роботі подібні семантики та різні формалізації відношення логічного наслідку узагальнені для композиційно-номінативних логік часткових однозначних, тотальних та часткових неоднозначних предикатів.

Логіка тотальних однозначних предикатів - це класична логіка. Логіки однозначних часткових предикатів - це логіки з неокласичною семантикою. Логіки тотальних неоднозначних предикатів називають логіками з пересиченою семантикою. Логіки часткових неоднозначних предикатів назвемо логіками із загальною семантикою (в О.Д.Смирнової - логіки з релевантною семантикою).

Для неоднозначних предикатів під еквітонністю будемо розуміти монотонність. Для тотальних неоднозначних предикатів вона означає, що при розширенні вхідних даних “інформативність” предиката може тільки зменшуватися, тому в класі таких предикатів поняття еквітонності (монотонності) не зовсім адекватне. Дуальним до еквітонності є поняття антиеквітонності (в загальному випадку функцій на впорядкованих множинах таку властивість називають антитонністю).

V-квазіарний предикат P : VA{T, F} антиеквітонний, якщо для довільних d, d'VA із умови d d' випливає P(d) P(d').

Це поняття цілком природне для тотальних неоднозначних предикатів, водночас воно малозмістовне для однозначних предикатів.

Теорема 6.1. Композиції , , R, x зберігають еквітонність та антиеквітонність V-квазіарних предикатів в кожній із семантик.

Співвідношення T((Р)) T(x(Р)), F(x(Р)) F((Р)), T(x(Р)) T((Р)), F((Р)) F(x(Р)) позначимо відповідно TR, FR, TR, FR.

Теорема 6.2. 1) Для загального випадку квазіарних предикатів не справджуються усі чотири співвідношення TR, FR, TR, FR.

2) Для еквітонних предикатів вірні TR і FR та невірні FR і TR.

3) Для антиеквітонних предикатів вірні FR і TR та невірні TR і FR.

АС B = (A, IB) назвемо дуальною до A = (A, IA), якщо для кожного Ps маємо та . Тоді маємо: A = (A, IA) дуальна до B = (A, IB).

Якщо A = (A, IA) - АС з частковими однозначними предикатами, то дуальна B = (A, IB) - АС з тотальними неоднозначними предикатами, та навпаки.

Теорема 6.3. Нехай АС B = (A, IB) дуальна до АС A = (A, IA). Тоді для кожної формули маємо: 1) та .

2) A еквітонний B антиеквітонний та A антиеквітонний B еквітонний.

Неокласична семантика та пересичена семантика дуальні: A неспростовний на АС з частковими однозначними предикатами A B тотально істинний (тобто T(B) = VB) на дуальній АС B з тотальними неоднозначними предикатами.

На базі різних співвідношень між областями істинності та хибності предикатів на множині формул задамо 5 “природних” відношень логічного наслідку. Спочатку задамо відношення наслідку для двох формул при інтерпретації на фіксованій АС A.

1) Істиннісний наслідок A|=T : A|=T T(A) T(A).

2) Хибнісний наслідок A|=F : A|=F F(A) F(A).

3) Cильний наслідок A|=TF : A|=TF (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, I) з умови A | випливає A | .

Нехай B = (A, IB) дуальна до A = (A, IA). Тоді маємо: A|=T B|=F , A|=F B|=T ; A|=Cl B|=Cm ; A|=Cm B |= Cl .

В певному розумінні “природним” для неокласичної семантики є наслідок |=Cl , для пересиченої - наслідок |=Cm , для загальної - наслідок |=TF .

Відношення логічного наслідку індукують відповідні відношення еквівалентності AT , AF , ATF , ACl , ACm та логічної еквівалентності T , F , TF , Cl , Cm .

Введені відношення логічного наслідку поширюються на множини формул.

Властивості відношень логічного наслідку далі розглядаються в різних семантиках для загального випадку квазіарних предикатів та для випадків еквітонних і антиеквітонних предикатів. На основі розглянутих властивостей отримуємо наступні співвідношення для множин формул, які перебувають у відповідних відношеннях.

1. Неокласична семантика:

|=TF |=T , |=TF |=F , |=T |=Cl , |=F |=Cl ; |=t |=Cl , |=F ||=, |=T ||; |=Cm = ;

|=t |=T , |=t |=F , |=TF |=t ; |=T ||=, |=F ||, ||= |=Cl , || |=Cl .

2. Пересичена семантика:

|=TF |=T , |=TF |=F , |=T |=Cm , |=F |=Cm ; |=t |=Cm , |=F ||=, |=T ||; |=Cl = ;

|=t |=T , |=t |=F , |=TF |=t ; |=T ||=, |=F ||, ||= |=Cm , || |=Cm .

3. Загальна семантика:

|=TF = |=T = |=F ; |=t |=TF , |=TF |=t ; |=TF || = ||= ; |=Cl = та |=Cm = .

4. Загальна семантика еквітонних чи загальна семантика антиеквітонних предикатів:

|=TF |=T , |=TF |=F ; |=t |=TF , |=TF |=t ; |=T || , |=F ||= ; |=Cl = , |=Cm = .

В різних семантиках для загального випадку та для випадків еквітонних і антиеквітонних предикатів розглядаються властивості відношень логічного наслідку для множин формул. Зокрема, властивості, пов'язані з елімінацією кванторів.

В підрозділі 6.2 досліджуються КНЛ над ієрархічними номінативними даними. Необхідність їх вивчення пов'язана з тим, що при застосуванні логіки першого порядку до програм над складними, ієрархічними даними виникає певна невідповідність між мовою логіки та мовою програм, адже логіки першого порядку базуються на алгебрах неструктурованих даних. Для подолання такої невідповідності існують певні механізми, які дозволяють промоделювати складні дані через атомарні. Але при цьому значні зусилля витрачаються на саме моделювання і на дослідження його властивостей. Для уникнення цих складнощів М.С.Нікітченко висунув ідею побудови логік, безпосередньо базованих на алгебрах ієрархічних даних.

Множину іменованих ієрархічних номінативних даних HD(V, A) над множинами базових імен V та базових значень A визначаємо індуктивно. Задамо

ND0(V, A) = A, NDk+1(V, A) =. Тоді HD(V, A) =.

Тут - множина всіх скінченних однозначних відображень із V в NDk(V, A). Така однозначність гарантує однозначність іменування.

Ієрархічні номінативні дані можна подавати у вигляді орієнтованого дерева та у вигляді іменної множини зі складними іменами - елементами множини V+. Подання у вигляді іменної множини назвемо лінійною нормальною формою ієрархічного даного.

Даються визначення порівнянних та непорівнянних складних імен, диз'юнктних ієрархічних даних. Вводяться операція + об'єднання диз'юнктних даних, параметрична операція видалення компонент з іменами, порівнянними з заданими х1,..., хn . На множині HD(V, A) визначається операція реномінації:

.

Використання в реномінаціях складних імен робить згортку реномінацій проблематичною: подати у вигляді однієї реномінації неможливо. Для запису згортки пропонується подання реномінації в стандартній формі із використанням операцій +, із простими v1,..., vm, іменування v, застосування d до імені.

Предикати, задані на ієрархічних номінативних даних, тобто предикати вигляду Р : HD(V, A) {T, F}, назвемо H-квазіарними. Клас цих предикатів позначимо PrV_А.

Далі розглядаються логіки H-квазіарних предикатів на реномінативному та кванторному рівнях. Композицію реномінації стандартно визначаємо через операцію реномінації на ієрархічних даних: . Специфічні властивості реномінації тут пов'язані зі складними іменами, зокрема, це згортка реномінацій.

При визначенні композицій x та x треба врахувати складність кванторних імен та можливість вести квантифікацію як за всіма ієрархічними, так і за базовими даними. Останній випадок розглядається в роботі. Композиція x тоді задається так:

Специфічні властивості композицій x та x, що відрізняють їх від відповідних композицій логік квазіарних предикатів, пов'язані з складними іменами, зокрема, з поглинанням конкретніших імен порівнянними загальнішими. Наприклад:

1. x.ухР = хР; x.ухР = хР; x.ухР = хР; x.ухР = хР.

2. xх.уР = xх.уР хР; xх.уР х.уР; xх.у Р = xх.уР хР; xх.у Р х.уР.

Семантичними моделями КНЛ над ієрархічними номінативними даними є композиційні системи H-квазіарних предикатів вигляду (HD(V, A), PrV_А, C). Із синтаксичного погляду мови КНЛ H-квазіарних предикатів та квазіарних предикатів відповідного рівня мало відрізняються (наявністю складних імен). Інтегрованими семантичними моделями, які пов'язують мову КНЛ H-квазіарних предикатів відповідного рівня із АС даних, є АС з доданою сигнатурою вигляду ((HD(V, A), PrV_А), I).

Визначення істинності та виконуваності формул, відношень |=, ||=, , TF, |= такі ж, як і для КНЛ квазіарних предикатів. Для КНЛ H-квазіарних предикатів справджуються теореми семантичної еквівалентності та заміни еквівалентних.

Далі наводяться основні властивості формул КНЛ H-квазіарних предикатів та властивості відношення логічного наслідку для множин формул.

В підрозділі 6.3 на базі логік квазіарних предикатів і традиційних модальних логік пропонуються композиційно-номінативні модальні логіки. Центральним поняттям цих логік є поняття композиційно-номінативної модальної системи (КНМС). Такі системи описують світи розгляду модальної логіки і є їх моделями. КНМС - це об'єкт M = (Cms, Ds, Dns), де Cms = (D, R, Pr, C) - композиційна модальна система, Ds - дескриптивна система, Dns - денотаційна система. Компоненти D, R, Pr, C визначаються так. D - це множина станів світу; R - множина відношень на станах вигляду R D Dn ; Pr - множина предикатів на D; C - множина композицій на Pr.

Вибираючи ті чи інші базові модальні композиції та пов'язані з ними відношення з R, дістаємо відповідні різновидності КHМС.

Важливим випадком КНМС є транзиційні модальні системи (ТМС). В межах таких систем можуть розглядатися традиційні модальні логіки. Для ТМС множина R складається з відношень вигляду R D D. ТМС, у яких R складається з єдиного бінарного відношення , а базовими модальними композиціями є (необхідно) і (можливо), назвемо загальними. ТМС, у яких R складається з єдиного бінарного відношення , а базовими модальними композиціями є (завжди буде), (завжди було), (колись буде), (колись було), назвемо темпоральними КНМС.

Наводиться опис мови КНМС кванторного рівня, уточнюється відображення інтерпретації для транзиційних та темпоральних КНМС.

Залежно від властивостей , отримуються відповідні типи загальних ТМС і темпоральних КНМС, подібні до класичних модальних та темпоральних структур.

ВИСНОВКИ

Дисертація присвячена вирішенню важливої наукової проблеми розробки програмно-орієнтованих логічних систем. В роботі побудовано та досліджено спектр логік часткових предикатів, орієнтованих на композиційно-номінативні моделі програм.

Основними науковими результатами дисертаційної роботи є такі.

1. На основі розвитку поняття даного виділено рівні розгляду, які визначають інтенсіональні моделі композиційно-номінативних логік. Запропоновано спектр таких логік за рівнем абстракції розгляду та за обмеженнями на клас квазіарних предикатів.

2. Досліджено композиції та композиційні системи квазіарних функцій і предикатів на пропозиційному, реномінативному та першопорядкових рівнях: кванторному, кванторно-екваційному, функціональному, функціонально-екваційному.

3. Досліджено на абстрактному рівні поняття алгебри, алгебраїчної системи, їх гомоморфізмів, запропонована класифікація таких гомоморфізмів. Розглянуто алгебраїчні системи з квазіарними функціями та предикатами, названі неокласичними, досліджено гомоморфізми таких систем. Для композиційно-номінативних логік еквітонних предикатів доведено теореми про гомоморфізми та ізоморфізми.

4. Побудовано композиційно-номінативні логіки квазіарних предикатів реномінативного та першопорядкових рівнів. Описано мови та досліджено семантичні властивості логік відповідного рівня, зокрема, нормальні форми, відношення логічного наслідку для множин формул.

5. Виділено та досліджено неокласичні логіки, близькі до класичної логіки предикатів. Це композиційно-номінативні логіки еквітонних предикатів та їх розширення: логіки локально-еквітонних, еквісумісних, локально-еквісумісних предикатів. Такі логіки мають більші виразні можливості, ніж класичні логіки, а також ширші класи семантичних моделей, водночас ці логіки зберігають основні її закони.

6. Для логік повнототальних еквітонних предикатів відповідного рівня збудовано формально-аксіоматичні системи гільбертівського типу. Досліджено властивості побудованих числень, для них доведено теореми коректності та повноти.

7. На основі властивостей відношення логічного наслідку для множин формул для логік еквітонних предикатів відповідного рівня збудовано формально-аксіоматичні системи ґенценівського типу - секвенційні числення. Досліджено властивості таких числень, для них доведені теореми коректності та повноти, отримано наслідки теореми повноти. На основі збудованих числень доведено інтерполяційну теорему. Із її використанням для логік еквітонних предикатів доведено теореми про визначність.

8. Досліджено композиційно-номінативні логіки часткових однозначних, тотальних та часткових неоднозначних квазіарних предикатів. Для них запропоновано різні семантики та різні формалізації відношення логічного наслідку. Досліджено властивості таких відношень, визначено співвідношення між різними наслідками в різних семантиках.

9. Збудовані в роботі композиційно-номінативні логіки квазіарних предикатів є основою для побудови нових спеціальних логік. Це проілюстровано побудовою композиційно-номінативних модальних логік, в рамках яких виділено транзиційні та темпоральні композиційно-номінативні логіки.

10. На базі логік квазіарних предикатів побудовано композиційно-номінативні логіки часткових предикатів над ієрархічними номінативними даними, орієнтовані на опис властивостей поширених в програмуванні відображень, заданих на даних із складною структурою. Запропоновано семантичні моделі та мови таких логік, досліджено їх властивості.

Таким чином, в дисертаційній роботі побудовано та досліджено спектр нових програмно-орієнтованих логік, що знаходяться на різних рівнях абстрактності й загальності. Низка отриманих результатів є узагальненнями відомих тверджень класичної логіки. Результати роботи можуть застосовуватись при розробці інформаційних та програмних систем, зокрема, систем верифікації та специфікації програм.

СПИСОК ОПУБЛІКОВАНИХ ПРАЦЬ ЗА ТЕМОЮ ДИСЕРТАЦІЇ

1. Нікітченко М.С. Композиційно-номінативні логіки еквітонних предикатів / М.С.Нікітченко, С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2000. - Вип. 2. - С. 300-314.

2. Нікітченко М.С. Чисті композиційно-номінативні числення / М.С.Нікітченко, С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2000. - Вип. 3. - С. 290-303.

3. Никитченко Н.С. Неоклассические логики предикатов / Н.С.Никитченко, С.С.Шкильняк // Пробл. программирования. - 2000. - № 3-4. - С. 3-17.

4. Нікітченко М.С. Композиційно-номінативні логіки першого порядку / М.С.Нікітченко, С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2001. - Вип. 1. - С. 260-274.

5. Нікітченко М.С. Композиційно-номінативні числення першого порядку / М.С.Нікітченко, С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2001. - Вип. 2. - С. 302-313.

6. Нікітченко М.С. Семантичні аспекти посткласичних логік / М.С.Нікітченко, С.С.Шкільняк // Пробл. программирования. - 2001. - № 1-2. - С. 3-12.

7. Шкільняк С.С. Нормальні форми в неокласичній логіці / С.С.Шкільняк // Пробл. программирования. - 2001. - № 3-4. - С. 14-22.

8. Шкільняк С.С. Безкванторні неокласичні логіки / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2001. - Вип. 4. - С. 323-331.

9. Нікітченко М.С. Часткові та модальні логіки - засоби моделювання предметних областей / М.С.Нікітченко, С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2001. - Вип. 5. - С. 138-147.

10. Нікітченко М.С. Композиційно-номінативні модальні логіки / М.С.Нікітченко, С.С.Шкільняк // Пробл. программирования. - 2002. - № 1-2. - С. 27-33.

11. Шкільняк С.С. Безкванторні неокласичні числення / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2002. - Вип. 1. - С. 276-282.

12. Шкільняк С.С. Еквівалентні перетворення та нормальні форми в неокласичній логіці / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2002. - Вип. 2. - С. 278-287.

13. Шкільняк С.С. Функціонально-екваційні неокласичні логіки: синтаксичні властивості та нормальні форми / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. Вип. 3. - 2002. - С. 260-267.

14. Шкільняк С.С. Неокласичні секвенційні числення / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2002. - Вип. 4. - С. 261-274.

15. Шкільняк С.С. Неокласичні кванторні логіки з рівністю / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2003. - Вип. 1. - С. 222-225.

16. Шкільняк С.С. Cеквенційні числення неокласичних логік функціонального рівня / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2003. - Вип. 2. - С. 223-228.

17. Шкільняк С.С. Cеквенційні числення неокласичних логік / С.С.Шкільняк // Доповіді Академії наук України, секція "Кібернетика та обчислювальна техніка". - 2003. - № 6. - С. 58-63.

18. Нікітченко М.С. Логіки локально-еквітонних предикатів: семантичні властивості та секвенційні числення / М.С.Нікітченко, С.С.Шкільняк // Пробл. программирования. - 2003. - № 2. - С. 28-41.

19. Нікітченко М.С. Композиційні логіки номінативних даних / М.С.Нікітченко, С.С.Шкільняк // Пробл. программирования. - 2003. - № 3. - С. 29-40.

20. Шкільняк С.С. Функціонально-екваційні неокласичні логіки: числення секвенційного типу / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2003. - Вип. 4. - С. 302-309.

21. Нікітченко М.С. Семантичні властивості неокласичних логік та секвенційні числення / М.С.Нікітченко, С.С.Шкільняк // Вісник Київського ун-ту. Серія: кібернетика. - 2003. -Вип. 4. - С. 25-35.

22. Шкільняк С.С. Властивості неокласичних секвенційних числень / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2004. - Вип. 1. - С. 286-293.

23. Нікітченко М.С., Шкільняк С.С. Композиційнo-номінативнi логіки предикатів над даними з неповною інформацією // Пробл. программирования. - 2004. - № 2-3. - С. 74-80.

24. Нікітченко М.С. Ієрархія композиційно-номінативних логік / М.С.Нікітченко, С.С.Шкільняк // Пробл. программирования. - 2004. - № 4. - С. 5-14.

25. Шкільняк С.С. Композиційно-номінативні логіки квазіарних предикатів / С.С.Шкільняк // Вісник Київського ун-ту. Серія: фіз.-мат. науки. - 2004. - Вип. 4. - С. 278-287.

26. Шкільняк С.С. Фінітарні логіки квазіарних предикатів / С.С.Шкільняк // Вісник Київського ун-ту. Серія: кібернетика. - 2005. - Вип. 6. - С. 47-55.

27. Нікітченко М.С. Логіки, орієнтовані на специфікації програм / М.С.Нікітченко, С.С.Шкільняк, Л.Л. Омельчук // Пробл. программирования. - 2006. - № 2-3. - С. 17-24.

28. Нікітченко М.С. Спектр композиційно-номінативних логік / М.С.Нікітченко, С.С.Шкільняк // Вісник Київського ун-ту. Серія: кібернетика. - 2006. - Вип. 7. - С. 44-48.

29. Нікітченко М.С. Інтенсіонально-орієнтований підхід до побудови логічних систем / М.С.Нікітченко, С.С.Шкільняк // Пробл. програмування. - 2007. - № 2. - C. 15-40.

30. Шкільняк С.С. Неокласичні алгебри та їх гомоморфізми / С.С.Шкільняк // Наукові записки НаУКМА. Серія: Комп'ютерні науки. - 2009. - Т. 99. - C. 14-22.

31. Шкільняк С.С. Відношення логічного наслідку в композиційно-номінативних логіках / С.С.Шкільняк // Пробл. програмування. - 2010. - № 1 - C. 15-38.

32. Нікітченко М.С. Композиційно-номінативні логіки над ієрархічними даними / М.С.Нікітченко, С.С.Шкільняк // Пробл. програмування. - 2010. - № 2-3 - C. 48-57.

33. Шкільняк С.С. Логіки квазіарних предикатів / С.С.Шкільняк // Theoretical and Applied Aspects of Program Systems Development (TAAPSD'2004): international conference: abstracts. - К., 2004. - С. 90-96.

34. Nikitchenko N.S. Spectrum of finitary composition nominative logics / N.S.Nikitchenko, S.S.Shkilniak // CSIT Conference 2005: international conference: proceedings. - Yerevan, Armenia, 2005. - С. 113-116.

35. Шкільняк С.С. Семантичні властивості та секвенційні числення композиційно-номінативних логік / С.С.Шкільняк // Theoretical and Applied Aspects of Program Systems Development (TAAPSD'2006): international conference: abstracts. - К., 2006. - С. 190-196.

36. Nikitchenko N.S. Formalisms for Specification of Programs over Nominative Data / N.S.Nikitchenko, L.L.Omelchuk, S.S.Shkilniak // Electronic computers and informatics (ECI 2006): international conference: proceedings. - Koљice-Herl'any, Slovakia, 2006. P. 134-139.

37. Нікітченко М.С. Семантичні властивості композиційно-номінативних логік / М.С.Нікітченко, С.С.Шкільняк // Theoretical and Applied Aspects of Program Systems Development (TAAPSD'2009): international conference: abstracts. - К., 2009. - С. 50-59.

38. Nikitchenko N.S. Properties of Fixed Point Operators in Algebras of Partial Predicates / N.S.Nikitchenko, S.S.Shkilniak, I.A.Antonova // INFORMATICS 2009: international conference: proceedings. - Herl'any, Slovakia, 2009. - P. 184-191.

39. Shkilniak S.S. First-order Logics of Quasi-ary Predicates / S.S.Shkilniak // Automata, algorithms and information technologies: international workshop: abstracts. - Kyiv, 2010. - P. 22.

В роботі [1] М.С.Нікітченку належать визначення еквітонних та V-повних функцій, R-комутанта, похідної композиції; в роботах [2, 5] - ідея побудови числень; в роботі [4] - ідея побудови логік функціональних рівнів та визначення суперпозиції; в роботах [3, 6] - аналіз семантичних аспектів класичної логіки, дослідження предикатних композиційно-номінативних систем та побудова семантичних моделей посткласичних логік; в роботах [9, 10] - ідея побудови композиційно-номінативних модальних логік та побудова числень таких логік; в роботі [18] - ідея побудови логік з максимально широкими класами моделей, побудова числень ЛЕ-логік; в роботі [19] - абстрактна обчислюваність над номінативними даними, побудова алгебри номінативних даних; в роботі [21] - визначення еквітонних функцій, побудова RGN та QGN-числень; в роботі [23] - мотивація та ідея побудови логік над даними з неповною інформацією, побудова числень ЕС-логік та ЛЕС-логік; в роботах [24, 27, 28] - опис композиційно-номінативного підходу, інфінітарних та сингулярних логік; в роботі [29] - методологічні аспекти інтенсіонально-орієнтованого підходу, методологія розвитку понять даного та функції; в роботі [32] - ідея побудови логік над ієрархічними даними, поняття реномінанти, побудова числень. В роботі [27] Л.Л.Омельчук належить опис автоматизованої системи доведення теорем теорії метаномінативних даних.

Размещено на Allbest.ru

...