Композиційно-номінативні логіки предикатів над даними з неповною інформацією

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

Full description

Saved in:
Bibliographic Details
Date:2004
Main Authors: Нікітченко, М.С., Шкільняк, С.С.
Format: Article
Language:Ukrainian
Published: Інститут програмних систем НАН України 2004
Subjects:
Online Access:https://nasplib.isofts.kiev.ua/handle/123456789/2313
Tags: Add Tag
No Tags, Be the first to tag this record!
Journal Title:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Cite this:Композиційно-номінативні логіки предикатів над даними з неповною інформацією/ М.С. Нікітченко, С.С. Шкільняк // Проблеми програмування. — 2004. — N 2,3. — С. 74-80. — Бібліогр.:13 назв. — укр.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-2313
record_format dspace
spelling nasplib_isofts_kiev_ua-123456789-23132025-02-23T20:23:43Z Композиційно-номінативні логіки предикатів над даними з неповною інформацією Нікітченко, М.С. Шкільняк, С.С. Теоретические и методологические основы программирования Предикати над даними з неповною інформацією уточнюються як еквісумісні та локально-еквісумісні предикати. Запропоновані композиційно-номінативні логіки еквісумісних та локально-еквісумісних предикатів, що є природними розширеннями логік еквітонних та локально-еквітонних предикатів. Такі логіки зберігають основні дедуктивні властивості класичних логік. але мають істотно багатший клас семантичних моделей. Розглядаються семантичні властивості цих логік, будуються відповіднi секвенційні числення. Побудовані логіки можна розглядати як формалізми для опису та моделювання різноманітних предметних областей з урахуванням частковості та неповноти інформації. Предикаты над данными с неполной информацией уточняются как эквисовместимые и локально- эквисовместимые предикаты. Предложены композиционно-номинативные логики эквисовместимых предикатов, являющихся естественными расширениями логик эквитонных и локально-эквитонных предикатов. Такие логики сохраняют основные дедуктивные свойства классических логик, но имеют существенно более богатый класс семантических моделей. Рассматриваются семантические свойства этих логик, строятся соответствующие секвенциальные исчисления. Построенные логики можно рассматривать как формализмы описания и моделирования различных предметных областей, учитывающие частичность и неполноту информации Predicates over data with incomplete information are specified as equicompatible and local equicompatible predicates/ Composition nominative logics of such predicates, which are natural extensions of logics of equitone and local equitone predicates? are proposed. These logics preserve the main deductive properties of classical logic, but have a more rich class of models. The constructed logics can be considered as formalisms for description and modelling of various subject domains with partial and incomplete information. Робота виконана в рамках проекту INTAS 2000-447. 2004 Article Композиційно-номінативні логіки предикатів над даними з неповною інформацією/ М.С. Нікітченко, С.С. Шкільняк // Проблеми програмування. — 2004. — N 2,3. — С. 74-80. — Бібліогр.:13 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2313 510.6 681.3.06 uk application/pdf Інститут програмних систем НАН України
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language Ukrainian
topic Теоретические и методологические основы программирования
Теоретические и методологические основы программирования
spellingShingle Теоретические и методологические основы программирования
Теоретические и методологические основы программирования
Нікітченко, М.С.
Шкільняк, С.С.
Композиційно-номінативні логіки предикатів над даними з неповною інформацією
description Предикати над даними з неповною інформацією уточнюються як еквісумісні та локально-еквісумісні предикати. Запропоновані композиційно-номінативні логіки еквісумісних та локально-еквісумісних предикатів, що є природними розширеннями логік еквітонних та локально-еквітонних предикатів. Такі логіки зберігають основні дедуктивні властивості класичних логік. але мають істотно багатший клас семантичних моделей. Розглядаються семантичні властивості цих логік, будуються відповіднi секвенційні числення. Побудовані логіки можна розглядати як формалізми для опису та моделювання різноманітних предметних областей з урахуванням частковості та неповноти інформації.
format Article
author Нікітченко, М.С.
Шкільняк, С.С.
author_facet Нікітченко, М.С.
Шкільняк, С.С.
author_sort Нікітченко, М.С.
title Композиційно-номінативні логіки предикатів над даними з неповною інформацією
title_short Композиційно-номінативні логіки предикатів над даними з неповною інформацією
title_full Композиційно-номінативні логіки предикатів над даними з неповною інформацією
title_fullStr Композиційно-номінативні логіки предикатів над даними з неповною інформацією
title_full_unstemmed Композиційно-номінативні логіки предикатів над даними з неповною інформацією
title_sort композиційно-номінативні логіки предикатів над даними з неповною інформацією
publisher Інститут програмних систем НАН України
publishDate 2004
topic_facet Теоретические и методологические основы программирования
url https://nasplib.isofts.kiev.ua/handle/123456789/2313
citation_txt Композиційно-номінативні логіки предикатів над даними з неповною інформацією/ М.С. Нікітченко, С.С. Шкільняк // Проблеми програмування. — 2004. — N 2,3. — С. 74-80. — Бібліогр.:13 назв. — укр.
work_keys_str_mv AT níkítčenkoms kompozicíjnonomínativnílogíkipredikatívnaddanimiznepovnoûínformacíêû
AT škílʹnâkss kompozicíjnonomínativnílogíkipredikatívnaddanimiznepovnoûínformacíêû
first_indexed 2025-11-25T05:16:36Z
last_indexed 2025-11-25T05:16:36Z
_version_ 1849738188245958656
fulltext 1 УДК 510.6, 681.3.06 М.С. Нікітченко, С.С. Шкільняк Композиційно-номінативні логіки предикатів над даними з неповною інформацією∗∗∗∗ Предикати над даними з неповною інформацією уточнюються як еквісумісні та локально-еквісумісні предикати. Запропоновані композиційно-номінативні логіки еквісумісних та локально-еквісумісних предикатів, що є природними розширеннями логік еквітонних та локально-еквітонних предикатів. Такі логіки зберігають основні дедуктивні властивості класичних логік. але мають істотно багатший клас семантичних моделей. Розглядаються семантичні властивості цих логік, будуються відповіднi секвенційні числення. Побудовані логіки можна розглядати як формалізми для опису та моделювання різноманітних предметних областей з урахуванням частковості та неповноти інформації. Вступ Сучасні методи моделювання предметних областей повинні враховувати такі їх особливості, як неповнота та нечіткість наявної інформації [1]. Існують різноманітні теорії обробки такої інформації (теорії нечітких множин, теорії можливості, ймовірнісні теорії та інші), які орієнтовані на дослідження того чи іншого аспекту неповноти чи нечіткості інформації. Важливе місце серед таких теорій займають спеціальні логіки [2, 3], орієнтовані на зазначені особливості предметних областей. Метою даної статті є дослідження класів предикатів, які визначаються на даних з неповною інформацією, та розбудова відповідних логік таких предикатів. Особливістю цих логік є широке використання парадигм композиційності і номінативності та семантико-синтаксичний стиль їх побудови. Для мотивації формального визначення таких логік розглянемо невеликий приклад. Припустимо, що ми хочемо надіслати новорічне електронне привітання своєму другу. Для цього ми повинні з’ясувати наявність його електронної адреси. Тому спочатку ми викликаємо відповідну поштову програму та проглядаємо книгу адрес. Якщо адреса записана в книзі, то можемо надсилати привітання. Які предикати використовуються в цьому прикладі, як їх можна формалізувати? Дуже природним видається ввести предикат P, який буде істинним, якщо адреса друга знаходиться в адресній книзі, та невизначеним, якщо її там немає. Ми можемо трактувати предикат P як заданий на тих даних, що містяться в нашому комп’ютері. Розглянемо тепер ситуацію, коли адреси в книзі немає (предикат P невизначений), але адреса є в іншому файлі (наприклад, в листі подруги). Це фактично означає, що адресна книжка містить дані d з неповною інформацією, але потрібна нам інформація присутня в розширеному даному d'. В цьому випадку можна розширити предикат P до предикату P', який буде істинним як на d', так і на d. Для того, щоб таке розширення предикатів було можливим та коректним, необхідно на множині даних ввести відношення часткового порядку ⊆ (одне дане є розширенням іншого даного), а також вимагати, щоб розширення було однозначним. Остання вимога означає: якщо різні дані можуть бути розширені до одного більшого даного, то значення предиката на таких даних повинні співпадати. Така умова називається еквісумісністю. В цьому випадку розширений предикат буде мати властивість еквітонності: якщо предикат визначений з певним значенням на деякому даному, то він буде приймати те ж саме значення на будь-якому розширенні цього даного. ∗ Робота виконана в рамках проекту INTAS 2000-447. 2 Таким чином, дослідження предикатів над даними з неповною інформацією зводиться до дослідження еквісумісних та еквітонних предикатів. Якщо ми обмежимося розглядом розширень лише скінченною інформацією, то виникають класи локально- еквісумісних та локально-еквітонних предикатів. Які логіки ми будемо використовувати для дослідження зазначених класів предикатів? Найчастіше для таких досліджень використовується класична логіка предикатів. Але така логіка, попри численні позитивні властивості, має багато обмежень які ускладнюють її застосування в моделюванні. Класична логіка орієнтується на традиційні математичні структури тотальних n-арних функцій та предикатів, вона недостатньо враховує неповноту, частковість інформації про предметну область, її динаміку. Тому особливої актуальності набуває проблема розбудови нових логік, які базуються на істотно загальніших класах відображень. На основі проведеного в роботах [4, 5] аналізу класичної логіки можна стверджувати, що такими мусять бути часткові відображення, які задаються на довільних наборах іменованих значень – квазіарні відображення. Клас квазіарних предикатів надзвичайно потужний, тому для збереження основних властивостей класичної логіки його варто обмежити. Дуже природне обмеження задається властивістю еквітонності, яка означає, що значення відображення не змінюється при розширенні, поповненні даних. При умові збереження значень такі відображення також допускають довизначення на звужених даних (даних з неповною інформацією). Логіки еквітонних предикатів названі [4] неокласичними (НКЛ), бо вони зберігають основні закони класичної логіки при істотному розширенні класу моделей. Це дозволяє використовувати теоретичні результати і багатий досвід застосування класичної логіки в програмуванні та моделюванні. Природно поставити питання про побудову неокласичних логік з максимально широкими класами моделей. В роботі [6] побудована логіка локально-еквітонних предикатів – ЛЕ-логіка. Для локально-еквітонних предикатів вимагається збереження значення при розширенні даних лише на скінченну кількість іменованих компонент, тому вони є узагальненням еквітонних предикатів. Клас моделей ЛЕ-логіки є розширенням класу моделей логіки еквітонних предикатів. В даній роботі пропонуються композиційно-номінативні неокласичні логіки часткових предикатів, які є природними узагальненнями еквiтонних та локально-еквітонних предикатів. Такі предикати будемо називати еквісумісними та локально-еквісумісними. Логіки еквісумісних та локально-еквісумісних предикатів відповідно назвемо ЕС-логіками та ЛЕС-логіками. Побудовані логіки зберігають основні закони класичної логіки, але мають істотно ширший клас семантичних моделей. В статті досліджуються семантичні та синтаксичні властивості ЕС-логік і ЛЕС-логік. Стосовно семантичного аспекту, зокрема, розглянуте відношення логічного наслідку для множин формул. Стосовно синтаксичного аспекту для таких логік побудовані аксіоматичні системи секвенційного типу − секвенційні ЕС-числення. 1. Основні поняття та семантичні властивості ЕС-логік і ЛЕС-логік Будемо дотримуватись позначень робіт [5–8]. Для зручності читання нагадаємо основні поняття та визначення. Нехай A – множина базових даних, V – множина предметних імен (предметних змінних). V-іменна множина (V-ІМ) над A – це довільна однозначна функцію із V в A. Множину всіх V-IM над A позначаємо VA та задаємо у вигляді [v1aа1,...,vn aаn,...] (тут vi∈V, ai∈A, причому vi≠vj при i≠j). Для V-ІМ вводимо операцію звуження за множиною Х⊆V: d║Х = [vaa∈d | v∈X]. 3 Функцію im: VA→2V визначаємо умовою im(d) = pr1(d). Замість d║(V\{ х}) та d║(V\Х) для спрощення будемо писати d║-х та d║–Х. Визначимо операцію ∇ накладки V-ІМ d2 на V-ІМ d 1: d1∇d2 = d2∪(d1║(V\ im(d2))). Параметричну операцію реномінації r n n vv xx ,..., ,..., 1 1 визначаємо так: r n n vv xx ,..., ,..., 1 1 (d) = [v1ad(x1),...,vnad(xn)]∪(d║(V\{ v1,..., vn})). Ввівши позначення вигляду y для y1,..., yn, замість r n n vv xx ,..., ,..., 1 1 також пишемо r v x . V-IM d та d' сумісні, що позначимо d≈d', якщо функція d∪d' однозначна. Неважко переконатись, що для еквісумісних V-IM справджується Твердження 1. Нехай d1≈d2. Тоді d1║–Х ≈ d2║–Х та r v x (d1) ≈ r v x (d2). Довільну часткову функцію вигляду VA→R назвемо V-квазіарною функцією. Довільний часткову предикат вигляду Р : VA→{T, F} назвемо V-квазіарним предикатом на A. Множину V-квазіарних предикатів на A позначимо РrА. Параметрична композиція реномінації R n n vv xx ,..., ,..., 1 1 : РrА→РrА задається так: R n n vv xx ,..., ,..., 1 1 (Р)(d) = P(r n n vv xx ,..., ,..., 1 1 (d)). Замість R n n vv xx ,..., ,..., 1 1 будемо також писати R v x . Предметне ім'я x неiстотне для V-квазіарнoго предикату Р, якщо для довільних d∈VA та для довільних a, b∈A маємо Р(d∇xaa) ≅ Р(d∇xab). V-квазіарний предикат Р на A 1-еквітонний, якщо для довільних d, d'∈VA із умов Р(d)↓, d'⊃d та | d' \ d|=1 випливає Р(d')↓=Р(d). V-квазіарний предикат Р на A локально-еквітонний, якщо для довільних d, d'∈VA із умов Р(d)↓, d'⊇d та d' \ d скінченна, випливає Р(d')↓=Р(d). Той факт, що d'⊇d та d' \ d скінченна, будемо позначати d' ⊃F d. Відомо [6], що предикат Р 1-еквітонний ⇔ Р локально-еквітонний. V-квазіарний предикат Р на A еквітонний, якщо для довільних d, d' ∈VA із умови Р(d)↓ та d'⊇d випливає Р(d')↓=Р(d). V-квазіарний предикат Р еквісумісний, якщо для довільних d, d'∈VA із d≈d', Р(d)↓ та Р(d')↓ випливає Р(d)=Р(d'). V-квазіарний предикат Р локально-еквісумісний, якщо для довільних d, d'∈VA таких, що (d' \ d)∪(d \ d') скінченна, із d≈d', Р(d)↓ та Р(d')↓ випливає Р(d)=Р(d'). Кожний еквітонний предикат є локально-еквітонним, але існують [6] нееквітонні локально-еквітонні предикати. Неважко навести приклади еквісумісних нееквітонних предикатів та локально-еквісумісних предикатів, які не є локально-еквітонними. Приклад 1. Зафіксуємо х, у∈V. Предикат Р : VA→{T, F} задамо так. Покладемо Р(d)=Т, якщо x∈im(d) та y∉im(d), або y∈im(d) та x∉im(d); покладемо Р(d)↑, якщо х, у∈im(d) або х, у∉im(d). Такий предикат Р нееквітонний, але еквісумісний. Приклад 2. Зафіксуємо х, у∈V. Предикат Q : VA→{T, F} задамо так. Для всіх скінченних d∈VA покладемо Q(d)=Т, якщо x∈im(d) та y∉im(d), або y∈im(d) та x∉im(d); для всіх нескінченних d∈VA покладемо Q(d)=F, якщо x∈im(d) та y∉im(d), або y∈im(d) та x∉im(d); покладемо Q(d)↑, якщо х, у∈im(d) або х, у∉im(d). Такий предикат Q не є локально-еквітонним та еквісумісним, але Q локально-еквісумісний. Теорема 1. Кожний еквісумісний предикат можна розширити до еквітонного. 4 Нехай предикат Р : VA→{T, F} еквісумісний. Розширення Р можна робити як на більші (розширення вгору), так і на менші дані (розширення вниз). Розглянемо розширення вгору. Якщо Р(d)↑, але для деякого d1⊂F d маємо P(d1)↓, то покладемо Р(d)↓=P(d1). Таке розширення однозначне, тому коректне. Справді, нехай d1⊂F d, d2⊂F d, Р(d1)↓, Р(d2)↓ та Р(d1) ≠ Р(d2). Але з того, що d1⊂F d, d2⊂F d, випливає d1≈d2, при цьому (d1\ d2)∪(d2\ d1) скінченна. Тому за локально-еквісумісністю Р необхідно Р(d1) = Р(d2) Розширення вгору приводить до еквітонного предикату Р'. Проведемо тепер розширення вниз, побудувавши за Р' новий предикат Р''. Для цього візьмемо довільне d, для якого Р'(d)↑, і розглянемо значення Р'(d') для таких d′, що d⊂d′. Якщо всі Р'(d') не визначені, або є два різних значення Р', то покладемо Р''(d) невизначеним. Якщо є лише одне значення серед усіх Р'(d'), то покладемо Р''(d) рівним цьому значенню. Отриманий предикат буде також еквітонним. Він є найкращим релевантним розширенням Р у тому сенсі, що це найбільше еквітонне розширення, значення якого однозначно визначаються значеннями Р ▄ Теорема 2. Кожний локально-еквісумісний предикат можна розширити до локально-еквітонного. Доведення теореми 2 подібне до доведення теореми 1, для прикладу розглянемо випадок розширення вгору. Нехай предикат Р : VA→{T, F} локально-еквісумісний. Якщо Р(d)↑, але для деякого d1⊂F d маємо P(d1)↓, то покладемо Р(d)↓=P(d1). Таке розширення однозначне, тому коректне. Справді, нехай d1⊂F d, d2⊂F d, Р(d1)↓, Р(d2)↓ та Р(d1) ≠ Р(d2). Але з того, що d1⊂F d, d2⊂F d, випливає d1≈d2, при цьому (d1\ d2)∪(d2\ d1) скінченна. Тому за локально-еквісумісністю Р необхідно Р(d1) = Р(d2) ▄ Будемо розглядати композиційно-номінативні логіки еквісумісних та локально- еквісумісних предикатів на реномінативному та кванторному рівнях. Семантичною основою ЕС-логік є композиційні алгебри еквісумісних квазіарних предикатів (ESРrА, C). Семантичною основою ЛЕС-логік є композиційні алгебри локально-еквісумісних квазіарних предикатів (LESРrА, C). Тут ESРrА − множина еквісумісних V-квазіарних предикатів на A, LESРrА − множина локально-еквісумісних V-квазіарних предикатів на A, множина C задається базовими композиціями першого порядку ∨∨∨∨, ¬¬¬¬, R v x для логік реномінативного рівня та ∨∨∨∨, ¬¬¬¬, R v x , ∃∃∃∃x для логік кванторного рівня. Відомо [5, 6], що композиції ∨∨∨∨, ¬¬¬¬, R v x , ∃∃∃∃x зберігають властивості еквітонності та локально-еквітонності. Теорема 3. Композиції ¬¬¬¬, ∨∨∨∨, R v x , ∃∃∃∃x зберігають еквісумісність V-квазіарних предикатів. Нехай d1≈d2, предикати Р та Q еквісумісні. Зрозуміло, що Р еквісумісний ⇔ ¬¬¬¬(Р) еквісумісний. Нехай ∨∨∨∨(Р, Q)(d1)↓ та ∨∨∨∨(Р, Q)(d2)↓. Якщо ∨∨∨∨(Р, Q)(d1) ≠ ∨∨∨∨(Р, Q)(d2), то можливі два випадки: 1) ∨∨∨∨(Р, Q)(d1) = Т і ∨∨∨∨(Р, Q)(d2) = F; 2) ∨∨∨∨(Р, Q)(d2) = Т і ∨∨∨∨(Р, Q)(d1) = F. У першому випадку маємо два підвипадки: Р(d1) = Т, Р(d2) = F, Q(d2) = F, або Q(d1) = Т, Р(d2) = F, Q(d2) = F. В силу d1≈d2 перший підвипадок суперечить еквісумісності Р, другий підвипадок суперечить еквісумісності Q. Випадок 2) розглядається аналогічно. Таким чином, предикат ∨∨∨∨(Р, Q) еквісумісний. 5 Нехай R v x (Р)(d1)↓ та R v x (Р)(d2)↓. Це означає Р(r v x (d1))↓ та Р(r v x (d2))↓. Згідно твердження 1 із d1≈d2 випливає r v x (d1) ≈ r v x (d2). За еквісумісністю Р маємо Р(r v x (d1)) = Р(r v x (d2)), тобто R v x (Р)(d1) = R v x (Р)(d2). Отже, предикат R v x (Р) еквісумісний. Нехай ∃∃∃∃x(Р)(d1)↓ та ∃∃∃∃x(Р)(d2)↓. Припустимо, що ∃∃∃∃x(Р)(d1) ≠ ∃∃∃∃x(Р)(d2). Можливі два випадки: 1) ∃∃∃∃x(Р)(d1) = T та ∃∃∃∃x(Р)(d2) = F; 2) ∃∃∃∃x(Р)(d2) = T та ∃∃∃∃x(Р)(d1) = F. Розглянемо випадок 1), випадок 2) розглядається аналогічно. Маємо Р(d1∇xab)=T для деякого b∈A та Р(d2∇xaa)=F для всіх a∈A. Звідси Р(d2∇xab)=F. Але із d1≈d2 маємо d1∇xab ≈ d2∇xab, звідки Р(d1∇xab) = Р(d2∇xab) = F за еквісумісністю Р. Отримали суперечність. Отже, ∃∃∃∃x(Р)(d1) = ∃∃∃∃x(Р)(d2), звідки предикат ∃∃∃∃x(Р) еквісумісний ▄ Наслідок 1. Клас ESРrА замкнений відносно композицій ¬¬¬¬, ∨∨∨∨, R v x , ∃∃∃∃x. Беручи до уваги похідні композиції →→→→, &, ↔↔↔↔ та ∀∀∀∀x, дістаємо: Наслідок 2. Клас ESРrА замкнений відносно композицій ¬¬¬¬, ∨∨∨∨, →→→→, &, ↔↔↔↔, R v x , ∃∃∃∃x, ∀∀∀∀x. Теорема 4. Композиції ¬¬¬¬, ∨∨∨∨, R v x , ∃∃∃∃x зберігають локально-еквісумісність V-квазі- арних предикатів. Нехай d1≈d2, (d1 \ d2)∪(d2 \ d1) скінченна, предикати Р та Q локально-еквісумісні. Доведення того, що ¬¬¬¬(Р) локально-еквісумісний та ∨∨∨∨(Р, Q) локально-еквісумісний, є дослівним повтореннямд доведення еквісумісності таких предикатів в теоремі 3. Нехай R v x (Р)(d1)↓ та R v x (Р)(d2)↓. Це означає Р(r v x (d1))↓ та Р(r v x (d2))↓. Згідно твердження 1 із d1≈d2 випливає r v x (d1) ≈ r v x (d2). Крім того, якщо (d1 \ d2)∪(d2 \ d1) скінченна, то (r v x (d1) \ r v x (d2))∪(r v x (d2) \ r v x (d1)) теж скінченна. За локально-еквісумісністю Р маємо Р(r v x (d1)) = Р(r v x (d2)), тобто R v x (Р)(d1) = R v x (Р)(d2). Отже, предикат R v x (Р) локально-еквісумісний. Нехай ∃∃∃∃x(Р)(d1)↓ та ∃∃∃∃x(Р)(d2)↓. Припустимо, що ∃∃∃∃x(Р)(d1) ≠ ∃∃∃∃x(Р)(d2). Можливі два випадки: 1) ∃∃∃∃x(Р)(d1) = T та ∃∃∃∃x(Р)(d2) = F; 2) ∃∃∃∃x(Р)(d2) = T та ∃∃∃∃x(Р)(d1) = F. Розглянемо випадок 1), випадок 2) розглядається аналогічно. Маємо Р(d1∇xab)=T для деякого b∈A та Р(d2∇xaa)=F для всіх a∈A. Звідси Р(d2∇xab)=F. Але із d1≈d2 маємо d1∇xab ≈ d2∇xab. Крім того, якщо множина (d1 \ d2)∪(d2 \ d1) скінченна, то множина (d1∇xab \ d2∇xab)∪(d2∇xab \ d1∇xab) теж скінченна. За локально-еквісумісністю Р маємо Р(d1∇xab) = Р(d2∇xab) = F. Отримали суперечність. Отже, ∃∃∃∃x(Р)(d1) = ∃∃∃∃x(Р)(d2), звідки предикат ∃∃∃∃x(Р) локально-еквісумісний ▄ Наслідок 1. Клаc LESРrА замкнений відносно композицій ¬¬¬¬, ∨∨∨∨, R v x , ∃∃∃∃x. Беручи до уваги похідні композиції →→→→, &, ↔↔↔↔ та ∀∀∀∀x, дістаємо: Наслідок 2. Клас LESРrА замкнений відносно композицій ¬¬¬¬, ∨∨∨∨, →→→→, &, ↔↔↔↔, R v x , ∃∃∃∃x, ∀∀∀∀x. Побудова композиційних алгебр еквісумісних та локально-еквісумісних предикатів дає змогу визначити мови ЕС-логік та ЛЕС-логік. З синтаксичної точки зору такі мови не відрізняються від мови НКЛ. Алфавіт мови складається з множини V предметних імен, множини Ps предикатних символiв, символів базових композицій ¬, ∨, Rv x , ∃x. Множина Fr формул мови визначається індуктивно: 1) Кожний предикатний символ є формулою. Такi формули – атомарні. 2) Нехай Φ та Ψ – формули. Тодi ¬Φ, ∨ΦΨ, Rv x Φ, ∃xΦ – формули. 6 При фіксуванні множини базових композицій композиційні алгебри (ESРrА, C) та (LESРrА, C) визначаються алгебраїчними системами (АС) (А, ЕSРrА) та (А, LЕSРrА) відповідно. Значення формул мови ЕС-логіки задамо за допомогою відображення I : Рs→ЕSРrА. Таке відображення природним чином, аналогічно випадку НКЛ та ЛЕ-логік [5, 6], продовжується до відображення J : Fr→ЕSРrА. Пару ((А, ЕSРrА), I) назвемо неокласичною АС еквісумісних предикатів з доданою сигнатурою або ЕС-АС. Значення формул мови ЛЕС-логіки задамо за допомогою відображення I : Рs→LЕSРrА. Таке відображення природним чином продовжується до відображення J : Fr→LЕSРrА. Пару ((А, LЕSРrА), I) назвемо неокласичною АС локально-еквісумісних предикатів з доданою сигнатурою, або ЛЕС-АС. Надалі АС з доданою сигнатурою будемо позначати у вигляді A=(А, I). Предикат J(Φ), який є значенням формули Φ при інтерпретації на A=(А, I), позначаємо ΦA. Таким чином, різниця між мовами ЛЕС-логік, ЕС-логік, ЛЕ-логік та НКЛ – в семантичних моделях. Для ЛЕС-логіки клас таких моделей найширший. Основні закони класичної логіки справджуються і для ЛЕС-логік та ЕС-логік. Для таких логік природним чином, аналогічно випадку НКЛ та ЛЕ-логік [5, 6], вводяться поняття A-істинної (позначаємо A|=Φ) та всюди істинної (позначаємо |=Φ) формули, поняття логiчного наслiдку та логiчної еквiвалентності. Семантичні властивості ЕС-логік та ЛЕС-логік в основному аналогічні відповідним властивостям НКЛ та ЛЕ-логік [5–8, 10]. Важливе місце серед таких властивостей займає теорема семантичної еквiвалентностi та критерії неістотності предметних імен. Як і для випадку НКЛ та ЛЕ-логік, додатковою вимогою до семантичних моделей ЕС-логік та ЛЕС-логік є наявність нескінченної множини тотально неістотних імен. Це дає змогу виконувати еквівалентні перетворення довільних формул. Для ЕС-логік та ЛЕС-логік справджуються теореми [5–8] про зведення формул до різнокванторної форми та нормальної форми. Визначення логічного наслідку для множин формул у випадку ЕС-логік та ЛЕС- логік цілком аналогічне відповідному визначенню для НКЛ та ЛЕ-логік [6, 7]. Те, що множина формул ∆∆∆∆ є логічним наслідком множини формул ΓΓΓΓ, позначаємо ΓΓΓΓ |=|=|=|=∆∆∆∆. Індукцією за побудовою формули для випадку ЕС-логік та ЛЕС-логік доводиться Теорема 5. Нехай АС однієї сигнатури A=(А, IА) і В=(А, IВ) та формула Φ такі, що для всіх р∈σ(Φ) для всіх d∈VA із умови рA(d)↓ випливає рВ(d)↓=рA(d). Тоді для довільного d∈VA із умови ΦA(d)↓ випливає ΦВ(d)↓ = ΦA(d). Для випадку НКЛ та ЛЕ-логік відповідне твердження – це теорема 3 [7] для НКЛ та наслідок теореми 7 [6] для ЛЕ-логік. Нехай A=(А, IА) і В=(А, IВ) – неокласичні АС однiєї сигнатури. АС В назвемо системою розширень для АС A, якщо для всіх р∈Ps для всіх d∈VA із умови рA(d)↓ випливає рВ(d)↓=рA(d). Використовуючи введене визначення, як наслідок теореми 5 отримуємо, що для НКЛ, ЛЕ-логік, ЕС-логік та ЛЕС-логік справджується Теорема 6. Нехай В=(А, IВ) – система розширень для АС A=(А, IА). Тоді для довільної формули Φ та довільної d∈VA із умови ΦA(d)↓ випливає ΦВ(d)↓=ΦA(d). Нехай АС A=(А, IА) така, що для кожного р∈Ps предикат рA еквісумісний. Із теореми 3 отримуємо, що тоді для кожної формули Φ предикат ΦA еквісумісний. Нехай АС A=(А, IА) така, що для кожного р∈Ps предикат рA локально-еквісумісний. Тоді із теореми 4 маємо, що для кожної формули Φ предикат ΦA локально-еквісумісний. 7 Систему розширень В для АС A назвемо системою еквітонних розширень, якщо для кожного р∈Ps предикат рВ еквітонний. Систему розширень В для АС A назвемо системою локально-еквітонних розширень, якщо для кожного р∈Ps предикат рВ локально-еквітонний. Базові композиції зберігають властивості еквітонності та локально-еквітонності. Тому в системі еквітонних розширень В для АС A для кожної формули Φ предикат ΦВ еквітонний, причому для всіх d∈VA із ΦA(d)↓ випливає ΦВ(d)↓=ΦA(d). Аналогічно, в системі локально-еквітонних розширень В для АС A для кожної формули Φ предикат ΦВ локально-еквітонний, причому для всіх d∈VA із ΦA(d)↓ випливає ΦВ(d)↓=ΦA(d). Таким чином, враховуючи теореми 1 та 2, отримуємо: Теорема 7. 1) Для кожної ЕС-АС A=(А, IА) можна збудувати систему еквітонних розширень В=(А, IВ). При цьому для кожної формули Φ предикат ΦВ є еквітонним розширенням відповідного ΦA. 2) Для кожної ЛЕС-АС A=(А, IА) можна збудувати систему локально-еквітонних розширень В=(А, IВ). При цьому для кожної формули Φ предикат ΦВ є локально- еквітонним розширенням відповідного ΦA. На випадок ЕС-логік та ЛЕС-логік переносяться твердження, які справджуються (див. [6, 7]) для НКЛ та ЛЕ-логік: Теорема 8. Нехай ΣΣΣΣ − множина формул, у тотально неістотне та у∉пт(ΣΣΣΣ), нехай A = (А, IА) − АС. Тоді існує АС В = (А, IВ) така, що для довільної Φ∈ΣΣΣΣ з умови ΦA(d)↓ випливає ΦВ(d║-у)↓ = ΦВ(d)↓ = ΦA(d). Теорема 9. Нехай ΣΣΣΣ − множина формул, Ψ ∼ Φ, нехай АС A = (А, IА) та d∈VA такі, що для всіх Ξ∈ΣΣΣΣ маємо ΞA(d)↓, ΨA(d)↓ та ΦA(d)↑. Тоді існують АС В = (А, IВ) та δ∈AV такі, що для всіх Ξ∈ΣΣΣΣ маємо ΞB(δ)↓=ΞA(d), ΨB(δ)↓=ΨA(d) та ΦB(δ)↓=ΨB(δ). Cпочатку для АС A = (А, IА) будуємо систему еквітонних (локально-еквітонних) розширень A' = (А, IА'), потім, використовуючи аналогічні теоремам 8 та 9 твердження для НКЛ та ЛЕ-логік, для A' = (А, IА') будуємо АС В = (А, IВ) із потрібними властивостями ▄ На випадок ЕС-логік і ЛЕС-логік дослівно переноситься доведення [6] теореми про заміну еквівалентних: Теорема 10. Нехай Φ ∼ Ψ. Тоді Φ, ΓΓΓΓ |= |= |= |= ∆∆∆∆ ⇔ Ψ, ΓΓΓΓ |=|=|=|= ∆∆∆∆ та ΓΓΓΓ |= |= |= |= ∆∆∆∆, Φ ⇔ ΓΓΓΓ |= |= |= |= ∆∆∆∆,Ψ. На основі розглянутих теорем можна стверджувати, що властивості відношення логічного наслідку |= |= |= |= для множин формул ЕС-логік і ЛЕС-логік цілком аналогічні відповідним властивостям відношення |=|=|=|= для множин формул НКЛ та ЛЕ-логік [6, 7]. Вони безпосередньо відтворюють cемантичні властивості формул, пов'язані з пропозиційними композиціями i композиціями реномінації та квантифікації. 2. Секвенційні числення ЕС-логік та ЛЕС-логік Побудуємо тепер формально-аксіоматичні системи секвенційного типу, які формалізують відношення логічного наслідку між множинами формул ЕС-логік і ЛЕС-логік реномінативного рівня та кванторного рівня. Як було зазначено вище, властивості відношення |=|=|=|= для ЕС-логік та ЛЕС-логік аналогічні, тому такі системи назвемо реномінативними та кванторними секвенційними ЕС-численнями. Секвенційне числення традиційно будуємо так, що секвенція |− |− |− |− ΓΓΓΓ−| −| −| −| ∆∆∆∆ вивідна ⇔ ΓΓΓΓ |= |= |= |= ∆∆∆∆. Тому базовими властивостями відношення |=|=|=|= співставимо їх синтаксичні аналоги − секвенційні форми. Секвенційні форми є правилами виведення секвенційних числень. Секвенції |− |− |− |− ΓΓΓΓ−| −| −| −| ∆∆∆∆ такі, що ΓΓΓΓ∩∆∆∆∆ ≠ ∅, називають замкненими. Якщо секвенція |− |− |− |− ΓΓΓΓ−| −| −| −| ∆∆∆∆ замкнена, то ΓΓΓΓ |= |= |= |= ∆∆∆∆. Замкнені секвенції грають роль аксіом секвенційних числень. 8 Згідно до базових властивостей [6, 7] відношення |=|=|=|= вводимо відповідні базові секвенційні форми. На реномінативному рівні – це пропозиційні секвенційні форми ||||−−−−¬¬¬¬, −−−−||||¬¬¬¬, ||||−−−−∨∨∨∨, −−−−||||∨∨∨∨ та реномінативні секвенційні форми ||||−−−−RT, −−−−||||RT, ||||−−−−RR, −−−−||||RR, ||||−−−−R¬¬¬¬, −−−−||||R¬¬¬¬, ||||−−−−R∨∨∨∨, −−−−||||R∨∨∨∨, ||||−−−−PsN, −−−−||||PsN. На кванторному рівні до них додаються секвенційні форми ||||−−−−R∃∃∃∃, −−−−||||R∃∃∃∃, |−|−|−|−∃∃∃∃, −|−|−|−|∃∃∃∃. Зазначені секвенційні форми наведені в [6, 7], обмежимось тут для прикладу тільки формами |−|−|−|−∃∃∃∃ та −|−|−|−|∃∃∃∃: |−|−|−|−∃∃∃∃ ΣΣΣΣ ΣΣΣΣ , ),( | | xA ARx y ∃− − −|−|−|−|∃∃∃∃ ΣΣΣΣ ΣΣΣΣ , ,),(),...,( | ||| 1 xA xAARAR x z x z m ∃ ∃ − −−− Для ||||−−−−∃∃∃∃ ім'я у тотально неістотне та не входить до складу формул секвенції |−∃xА, ΣΣΣΣ. Для −|−|−|−|∃∃∃∃ {z1,…, zт} – множина квазівільних імен доступних формул [6, 7] секвенції −|∃xА, ΣΣΣΣ. Секвенційні числення ЕС-логік із зазначеними базовими секвенційними формами кванторного рівня назвемо кванторними ЕС-численнями. Обмежуючись секвенційними формами реномінативного рівня, отримуємо реномінативні ЕС-числення. Секвенція різнокванторна, якщо всі її формули різнокванторні, причому множини кванторних та квазівільних імен формул секвенції не перетинаються. Для кожної формули можна збудувати [6, 7] еквівалентну їй різнокванторну формулу. Неважко довести, що застосування базових секвенційних форм зберігає різнокванторність секвенцій. Тому, не обмежуючи загальність, можна розглядати тільки різнокванторні секвенції. Поняття виведення для секвенційних ЕС-числень вводимо традиційним чином, аналогічно класичним секвенційним численням [12, 13]. Таке виведення має вигляд дерева, вершинами якого є секвенції. Секвенційне дерево замкнене, якщо кожний його лист − замкнена секвенція. Секвенція ΣΣΣΣ вивідна, якщо існує замкнене секвенційне дерево з коренем ΣΣΣΣ. Таке дерево назвемо виведенням секвенції ΣΣΣΣ. Для ЕС-числень справджуються теореми коректності та повноти. Формулювання цих теорем однакове для числень реномінативного та кванторного рівня. Теорема 11 (теорема коректності). Нехай секвенція |−|−|−|− ΓΓΓΓ−| −| −| −| ∆∆∆∆ вивідна. Тоді ΓΓΓΓ |= |= |= |= ∆∆∆∆. Теорема доводиться індукцією за побудовою замкненого секвенційного дерева для секвенції |− |− |− |− ΓΓΓΓ−| −| −| −| ∆∆∆∆. Для доведення повноти секвенційних ЕС-числень природно використати метод модельних (Хінтікківських) множин. Доведення теореми повноти з використанням модельних множин для неокласичних секвенційних числень реномінативного та кванторного рівня наведені в [7, 11]. Враховуючи розглянуті вище семантичні властивості та той факт, що з синтаксичної точки зору мови ЛЕС-логік, ЕС-логік, ЛЕ-логік та НКЛ не відрізняються, такі доведення переносяться на випадок реномінативних та кванторних ЕС- числень. Теорема 12 (теорема повноти). Нехай ΓΓΓΓ |= |= |= |= ∆∆∆∆. Тоді секвенція |−|−|−|− ΓΓΓΓ−| −| −| −| ∆∆∆∆ вивідна. Для випадку ЛЕС-логік та ЕС-логік, як і для НКЛ, справджуються важливі властивості, що випливають з теореми повноти, зокрема, принцип компактності та його наслідки: теореми про суперечливість та несуперечливість множин формул, теореми про існування моделі, теореми про взаємну суперечливість та взаємну несуперечливість. Доведення цих властивостей, проведені [7] для НКЛ, переносяться на випадок ЛЕС-логік та ЕС-логік. 9 Висновки. В роботі побудовані логіки часткових предикатів над даними з неповною інформацією – логіки еквісумісних та локально-еквісумісних предикатів. Вони зберігають основні закони класичної логіки при істотному розширенні класу семантичних моделей. Розглянуті семантичні властивості таких логік, для них побудовані аксіоматичні системи секвенційного типу − секвенційні ЕС-числення. Пропоновані логіки можна розглядати як потужні формалізми для опису та моделювання різноманітних предметних областей з урахуванням частковості та неповноти інформації. 1 Андон Ф.И., Яшунин А.Е., Резниченко В.А. Логические модели интеллектуальных информационных систем.– Киев: Наукова думка, 1999. - 396 с. 2. A. Nait Abdallah. The logic of partial information.– Berlin: Springer.– 1996.– 715 p. 3. S.P Demri, E.S. Orlowska. Incomplete information: structure, inference, complexity.– Berlin: Springer.– 2002.– 405 p. 4. Никитченко Н.С., Шкильняк С.С. Неоклассические логики предикатов. – Проблемы программирования, 2000, № 3–4, c. 3–17. 5. Нікітченко М.С., Шкільняк С.С. Композиційно-номінативні логіки еквітонних предикатів. – Вісник Київського університету. Серія: фіз.-мат. науки. Вип 2. – Київ, 2000. – С. 300–314. 6. Нікітченко М.С., Шкільняк С.С. Логіки локально-еквітонних предикатів: семантичні властивості та секвенційні числення. – Проблемы программирования, 2003, № 2, c. 28–41. 7. Шкільняк С.С. Неокласичні секвенційні числення. – Вісник Київського ун-ту. Серія: фіз.-мат. науки. Вип.4. – Київ, 2002. – С. 261–274. 8. Шкільняк С.С. Нормальні форми в неокласичній логіці // Проблемы программирования. – 2001, № 3–4. – С. 14–22. 9. Басараб И.А., Никитченко Н.С., Редько В.Н. Композиционные базы данных. – К.: Либідь, 1992. – 192 с. 10. Нікітченко М.С., Шкільняк С.С. Семантичні аспекти посткласичних логік // Проблемы программирования. – 2001. – № 1-2. – С. 3–12. 11. Нікітченко М.С., Шкільняк С.С. Неокласичні логіки та секвенційні числення // Деп в ДНТБ України 22.07.2002, № 114-Ук2002. – 46 с. 12. Клини С. Математическая логика. – М.: Наука. – 1973. – 480 с. 13. Непейвода Н.Н. Прикладная логика. – Новосибирск: НГУ, 2000. – 521 с. Композиционно-номинативные логики предикатов над данными с неполной информацией / Н.С.Никитченко, С.С.Шкильняк Предикаты над данными с неполной информацией уточняются как эквисовместимые и локально-эквисовместимые предикаты. Предложены композиционно-номинативные логики эквисовместимых и локально-эквисовместимых предикатов, являющиеся естественными расширениями логик эквитонных и локально-эквитонных предикатов. Такие логики сохраняют основные дедуктивные свойства классических логик, но имеют существенно более богатый класс семантических моделей. Рассматриваются семантические свойства этих логик, строятся соответствующие секвенциальные исчисления. Построенные логики можно рассматривать как формализмы описания и моделирования различных предметных областей, учитывающие частичность и неполноту информации. Composition nominative predicate logics over data with incomplete information / M.S.Nikitchenko, S.S.Shkilniak Predicates over data with incomplete information are specified as equicompatible and local equicompatible predicates. Composition nominative logics of such predicates, which are natural extensions of logics of equitone and local equitone predicates, are proposed. These logics preserve the main deductive properties of classical logic, but have a more rich class of models. Semantic properties and consequence relation for sets of formulas of such logics are studied and corresponding sequential calculi are constructed. The constructed logics can be considered as formalisms for description and modelling of various subject domains with partial and incomplete information. 10 Про авторів: Нікітченко Микола Степанович, доктор фіз.-мат. наук, зав. кафедри теорії програмування Київського національного університету ім. Тараса Шевченка; м. Київ, тел. (044) 259-05-19 Шкільняк Степан Степанович, кандидат фіз.-мат. наук, доцент кафедри теорії програмування Київського національного університету ім. Тараса Шевченка; м. Київ, тел. (044) 259-05-19 Надійшла до редколегії 24.12.2003