Construction of sequent calculi of composition-nominative multimodal logics

Construction of sequent calculi of composition-nominative multimodal logics

In this paper first-order composition-nominative multimodal logics of quantifier-equational level are studied. For these logics sequent calculi are constructed. Soundness and completeness theorems are proved for the defined calculi. Problems in programming 2013; 1: 3-13

Збережено в:
Бібліографічні деталі
Дата:2025
Автор: Shkilniak, O.S.
Формат: Стаття
Мова:Ukrainian
Опубліковано: PROBLEMS IN PROGRAMMING 2025
Теми:
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/783
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-783
record_format ojs
resource_txt_mv ppisoftskievua/c7/270c484dfd9288ae6d5217d3f9987ac7.pdf
spelling pp_isofts_kiev_ua-article-7832025-08-27T13:30:47Z Construction of sequent calculi of composition-nominative multimodal logics Побудова секвенційних числень мультимодальних композиційно-номінативних логік Shkilniak, O.S. УДК 004.42:510.69 In this paper first-order composition-nominative multimodal logics of quantifier-equational level are studied. For these logics sequent calculi are constructed. Soundness and completeness theorems are proved for the defined calculi. Problems in programming 2013; 1: 3-13 Досліджено першопорядкові композиційно-номінативні мультимодальні логіки кванторно-екваційного рівня. Для цих логік побудовано числення секвенційного типу. Для таких числень доведено теореми коректності та повноти.Problems in programming 2013; 1: 3-13 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-08-27 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/783 PROBLEMS IN PROGRAMMING; No 1 (2013); 1-13 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2013); 1-13 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2013); 1-13 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/783/835 Copyright (c) 2025 PROBLEMS IN PROGRAMMING
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2025-08-27T13:30:47Z
collection OJS
language Ukrainian
topic

spellingShingle

Shkilniak, O.S.
Construction of sequent calculi of composition-nominative multimodal logics
topic_facet


УДК 004.42:510.69
format Article
author Shkilniak, O.S.
author_facet Shkilniak, O.S.
author_sort Shkilniak, O.S.
title Construction of sequent calculi of composition-nominative multimodal logics
title_short Construction of sequent calculi of composition-nominative multimodal logics
title_full Construction of sequent calculi of composition-nominative multimodal logics
title_fullStr Construction of sequent calculi of composition-nominative multimodal logics
title_full_unstemmed Construction of sequent calculi of composition-nominative multimodal logics
title_sort construction of sequent calculi of composition-nominative multimodal logics
title_alt Побудова секвенційних числень мультимодальних композиційно-номінативних логік
description In this paper first-order composition-nominative multimodal logics of quantifier-equational level are studied. For these logics sequent calculi are constructed. Soundness and completeness theorems are proved for the defined calculi. Problems in programming 2013; 1: 3-13
publisher PROBLEMS IN PROGRAMMING
publishDate 2025
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/783
work_keys_str_mv AT shkilniakos constructionofsequentcalculiofcompositionnominativemultimodallogics
AT shkilniakos pobudovasekvencíjnihčislenʹmulʹtimodalʹnihkompozicíjnonomínativnihlogík
first_indexed 2025-09-17T09:22:27Z
last_indexed 2025-09-17T09:22:27Z
_version_ 1843502458619297792
fulltext Теоретичні та методологічні основи програмування © O.С. Шкільняк, 2013 ISSN 1727-4907. Проблеми програмування. 2013. № 1 3 УДК 004.42:510.69 О.С. Шкільняк ПОБУДОВА СЕКВЕНЦІЙНИХ ЧИСЛЕНЬ МУЛЬТИМОДАЛЬНИХ КОМПОЗИЦІЙНО-НОМІНАТИВНИХ ЛОГІК Досліджено першопорядкові композиційно-номінативні мультимодальні логіки кванторно-екваційного рівня. Для цих логік побудовано числення секвенційного типу. Для таких числень доведено теореми коректності та повноти. Вступ Розвиток програмування та пов'я- зана з цим поява нових задач і проблем характеризуються виникненням нових ро- зділів математичної логіки, які мають ве- лике практичне значення. Важливе місце серед них посідають модальні логіки. Осо- бливого значення такі логіки набувають у зв'язку зі створенням та розвитком су- часних інформаційних та програмних сис- тем. Апарат темпоральних логік успішно застосовується для моделювання динаміч- них систем, специфікації та верифікації програм. Для опису сучасних інтелектуа- льних систем, баз даних і баз знань вико- ристовуються епістемічні логіки (див., на- пр., [1]). Можливості традиційних мода- льних логік і композиційно-номінативних логік квазіарних часткових предикатів [2] поєднують композиційно-номінативні модальні логіки (КНМЛ). Центральним поняттям КНМЛ є поняття композиційно- номінативної модальної системи (КНМС). На основі спеціального уточнення цього поняття збудовано та досліджено [3–5] нові класи КНМЛ реномінативного та першопорядкових рівнів. Важливим кла- сом КНМС є транзиційні модальні системи (ТМС), які відбивають аспект зміни й роз- витку предметних областей, описуючи пе- реходи від одного стану світу до іншого. Традиційні модальні логіки (алетичні, те- мпоральні, епістемічні) можуть природним чином розглядатися в межах транзиційних КНМЛ. Під ТМС розумітимемо об'єкти ви- гляду ((S, R, Pr, C), Fт, Jт). Тут S – мно- жина станів світу; R – множина відношень на станах вигляду R  S  S, Pr – множина предикатів на даних станів світу; C – мно- жина композицій на Pr , C визначається базовими загальнологічними композиція- ми відповідного рівня та базовими мода- льними композиціями; Fm – множина фо- рмул мови; Jт – відображення інтерпрета- ції формул у станах світу. Нові класи ТМС – мультимодальні транзиційні системи (ММС) – запропоно- вано в [6, 7]. ММС – це ТМС із множиною відношень R = {i | iI} та базовими мода- льними композиціями Кi , i I , у яких ко- жному i зіставлено відповідну Кi . Для КНМЛ номінативних рівнів S конкретизуємо як множину неокласичних алгебраїчних систем вигляду  α αα ,A Pr , де αPr – множина еквітонних предикатів вигляду V A   ,T F . Тоді S Pr Pr   – множина пре- дикатів усіх станів, S A A   – множина усіх базових даних світу. Окремим випадком ММС є загальні ТМС, для них R = {} та маємо єдину базо- ву модальну композицію . Мета даної роботи – дослідження мультимодальних логік (ММЛ) еквітонних предикатів кванторного-екваційного рівня та побудова для них числень секвенційно- го типу. Для таких числень доведено тео- реми коректності та повноти. Невизначені тут поняття тлумачимо в сенсі робіт [2, 4, 8]. Теоретичні та методологічні основи програмування 4 1. Семантичні властивості мультимодальних логік На кванторному-екваційному рівні базовими загальнологічними композиція- ми є , , v xR , x та спеціальні 0-арні ком- позиції – параметризовані за іменами пре- дикати рівності =ху , вони задають слабку (з точністю до визначеності) рівність ком- понентів даного з іменами x та y . Опишемо мову ММС кванторного- екваційного рівня. Алфавіт мови: множини V предметних імен та Ps предикатних сим- волiв; символи базових композицій  ,  , v xR , x , =xy ; множина     |iMs К i I  си- мволів базових модальних композицій (модальна сигнатура). Множина Fт формул мови визна- чається індуктивно: FA) кожний p Ps та кожний ху є формулою; такi формули – атомарні; FP) нехай  та  – формули; тодi  та  – формула; FR) нехай  – формулa; тодi v xR () – формула; F) нехай  – формулa; тодi x  – формула; FM) нехай  – формула,  iК Ms ; тодi  iК  – формула. Задамо відображення інтерпретації атомарних формул на станах світу :Im Рs S Pr  , при цьому  ,Im p Pr  та  хуIm   =ху для всіх х, уV. Продов- жимо Im до відображення інтерпретації формул на станах :Jm Fm S Pr  . При цьому маємо  ,Jm Pr   . IA)    , ,Jm p Im p   для кожно- го pPs;    , ,ху хуJm Im     для всіх х, уV; IP)  ,Jm      ,Jm   ;  ,Jm        , , ,Jm Jm    ; IR)     , ,v v x xJm R Jm    R ; I)   ,Jm x d          α α , якщо існує : ,α , , якщо , для всіх невизначене в усіх інших випадках. T a A Jm d x a T F Jm d x a T a A                IM)     ,iJm К d         , якщо ,δ для всіх всіх δ : α δ, , якщо існує δ та ,δ , невизначене в усіх інших випадках. i T Jm d T S F S Jm d F              Якщо для стану  не існує такого , що  βi , то вважаємо   ,iJm K d   для кожного d V A. Предикат  ,Jm   , який є значен- ням формули  у стані  , позначаємо .  істинна в ММС M якщо преди- кат  є істинним для кожного S. Це позначаємо M |= .  всюди істинна (позначаємо |= ), якщо M |=  для всіх ММС M одного типу. ММС номінативних рівнів скороче- но позначаємо також як M = (S, R, А, Іт). Замість ху будемо в традиційному вигляді писати x y . Залежно від того, як задати  d при умові d  V A, можна виділити [5] ММС із сильною умовою визначеності на станах, названі St-ММС, та ММС із загальною умовою визначеності на станах, названі Gn-ММС. Для St-ММС при умові d V A вважаємо  δ d  . Для Gn-ММС при умові d V A вважаємо    d d    , де d – скорочене поз- начення даного (іменної множини)  δ|a d a A   . Така умова видається більш природною. У випадку Gn-ММС ма- ємо    δ δ δd d  для всіх d V A. Базові композиції Gn-ММС зберіга- ють еквітонність предикатів, водночас ба- зові модальні композиції St-ММС зберіга- ють лише слабку еквітонність, а еквітон- ність вони не зберігають (див. [3, 4]). Тому Теоретичні та методологічні основи програмування 5 в даній роботі основну увагу приділимо дослідженню Gn-ММС. Властивості відношень i індуку- ють різні класи ММС. Найчастіше розгля- дають випадки, коли ці відношення мо- жуть бути рефлексивними, симетричними чи транзитивними. Якщо всі i рефле- ксивні, то в назві ММС пишемо R; якщо всі i транзитивні, то пишемо T; якщо всі i симетричні, то пишемо S. Таким чином, маємо наступні чисті типи ММС: R-ММС, T-ММС, S-ММС, RT- ММС, RS-ММС, TS-ММС, RTS-ММС. Можна розглядати складніші, змі- шані типи ММС, коли різні відношення i мають різні властивості. ММС із скінченними множинами однотипних відношень i названо [6–8] епістемічними, або ММС епістемічного типу. Такі ММС тісно пов'язані з базовими системами традиційної епістемічної логіки знання. Зокрема, R-ММС, RT-ММС, RTS- ММС є узагальненнями відомих [1] епі- стемічних Т(n), S4(n), S5(n)-систем. Теорема 1. Для довільних iK Ms маємо такі властивості: 1)  | v v x i i xR K K R   ; 2)  | i ix K K x     та  | i iK x x K    ; 3)  | Kix y x y    . Отже, модальні композиції можна проносити через реномінації, водночас взаємодія модальних композицій та кван- торів істотно складніша: формули вигляду K Ki ix x    та K Ki ix x   не є [6 – 8] всюди істинними. Властивість п. 3 зумовлена тим, що трактування рівності базових даних як їх тотожності веде до того, що для одного і того ж даного d неможлива ситуація, коли в одному стані    d x d y  , а в іншому стані    d x d y  . Поняття логічного наслідку для множин специфікованих станами формул вводимо так.  є логічним наслідком  в ММС M (позначаємо  |=M ), якщо для всіх d V A із того, що (d) = T для всіх   , випли- ває: неможливо Ψ(d) = F для всіх Ψ  .  є логічним наслідком  (познача- ємо  |= ), якщо  |=M  для всіх ММС M відповідного типу. Розглянемо властивості відношення |= на кванторно-екваційному рівнi. Споча- тку наведемо немодалізовані властивості (вони фактично успадковані від компози- ційно-номінативних логік квазіарних пре- дикатів [2]): C) якщо   , то  |= ; U) нехай    та   , тоді  |=M    |=M ; )   ,  |=M    |=M ,  ;  |=M ,    ,  |=M ; )   ,  |=M     ,  |=M  та  ,  |=M ;  |=M ,     |=M ,  ,  ; N) , , y v z xR ( )  |=M   ( ) ,v xR   |=M ;  |=M , , , ( )y v z xR    |=M , ( )v xR  (тут  μy  ); RT) , , ( ) ,z v z xR   |=M   ( ) ,v xR   |=M ;  |=M , , , ( )z v z xR    |=M , ( )v xR  ; R) ( ) ,v xR   |=M     ( ) ,v xR   |=M ;  |=M , ( )v xR    |=M ,  ( )v xR  ; R) ( ) ,v xR   |=M    ( ) ( ) ,v v x xR R     |=M ;  |=M , ( )v xR     |=M , ( ) ( )v v x xR R    ; RR) ( ( )) ,v w x yR R   |=M    ( ) ,v w x yR   |=M ; Теоретичні та методологічні основи програмування 6  |=M , ( ( ))v w x yR R     |=M , ( )v w x yR  ; R) ( ) ,v xR y    |=M    ( ) ,v xy R    |=M ;  |=M , ( )v xR y     |=M , ( )v xyR   ; R) ( ) ,v xR y    |=M    ( ) ,v y x zzR    |=M ;  |=M , ( )v xR y      |=M , ( ) .v y x zzR   Для R умова  ,y x , для R – умова  ,y x . ) x   ,  |=   ( ) ,x yR   |= , де y nm (,, x  ) та y тотально неісто- тне;  |=M , ( )x yR  , x     |=M , x   . Із рівністю пов'язані властивості: SmE) x y ,  |=M    x y , y x ,  |=M ; TrE) x y , y z ,  |=M    x y , y z , s r , x z ,  |=M ; Е) y x , , , ( )z u y vR  ,  |=M    y x , , , ( )z u y vR  , , , ( )z u x vR  ,  |=M ; y x ,  |=M , , , ( )z u y vR    y x ,  |=M , , , ( )z u y vR  , , , ( )z u x vR  ; ER) x y ,  ,  |=M    x y ,  , x yR  , ,y xR   |=M ; x y ,  |=M ,    x y ,  |=M ,  , x yR  , y xR  . Наведемо властивості, пов'язані з модальними композиціями: RКi ) , (K )v x iR  |=M    , K ( )v i xR  |=M ;  |=M , (K )v x iR    |=M , K ( )v i xR  ; Кi ) Ki  ,  |=M     β  | i  и |=M ;  |=M , Ki    |=M ,  для всіх : i  . 2. Секвенційні числення мультимодальних логік еквітонних предикатів Пропоновані числення композицій- но-номінативних ММЛ індуковані реля- ційною семантикою цих логік. Специфікацією стану називають [3] слово вигляду |– чи –|, де  – префікс стану світу. В такому префіксі вказується стан світу, в якому розглядається специфі- кована формула. Спеціальний символ  вказує на довільний стан, пов’язаний із да- ним станом відношенням досяжності. Ви- користання  уточнюється [3, 4] залежно від виду модальної логіки. Стани світу бу- демо іменувати натуральними числами. Секвенції збагачуємо збудованими на даний момент виведення множиною S станів світу та множиною R відношень на S. Секвенційні форми повинні враховувати можливість зміни носіїв станів світу (фор- ма |–, в окремих випадках форми |R та |R), тому для кожного із станів S треба вказувати збудовану на даний мо- мент множину його базових даних A . То- му збагачені секвенції будемо записувати як  //  A , {A}, … // M, скорочено як  // St // M. Тут  – множина специфікова- них формул; St – збудована на даний мо- мент множина імен станів;  A , {A}, … – побудовані на даний момент стани із множинами їх базових даних; M – схема моделі світу, тобто побудоване на даний момент відношення досяжності, за- писане для імен станів. Опишемо базові секвенційні форми числень ММЛ еквітонних предикатів кван- торних рівнів. Спочатку наведемо форми, анало- гічні відповідним формам числень логі- ки еквітонних квазіарних предикатів [2]. Теоретичні та методологічні основи програмування 7 Вони не змінюють схему моделі світу, але форми |– (в окремих випадках також |R і |R) змінюють стани. Спочатку наведемо форми, анало- гічні відповідним формам числень логіки еквітонних квазіарних предикатів [2]. Во- ни не змінюють схему моделі світу, але форми |– (в окремих випадках |R і |R) змінюють стани. |–  | | , / / / / , / / / / A St M A St M       ; |  | | , / / / / , / / / / A St M A St M       ; | | | | , / / / / , / / / / , / / / / A St M B St M A B St M         ; | | | | , , / / / / , / / / / A B St M A B St M       ; |RT | , | , ( ), / / / / ( ), / / / / v x z v z x R A St M R A St M     ; |RT | , | , ( ), / / / / ( ), / / / / v x z v z x R A St M R A St M     ; |RR | | ( ), / / / / ( ( )), / / / / v w x y v w x y R A St M R R A St M       ; |RR | | ( ), / / / / ( ( )), / / / / v w x y v w x y R A St M R R A St M     ; |R |- |- ( ), / / / / ( ), / / / / v x v x R A St M R A St M       ; |R | | ( ), / / / / ( ), / / / / v x v x R A St M R A St M       ; |R | | ( ) ( ), / / / / ( ), / / / / v v x x v x R A R B St M R A B St M       ; |R | | ( ) ( ), / / / / ( ), / / / / v v x x v x R A R B St M R A B St M       ; |N | , | , ( ), / / / / ( ), / / / / v u y v z u R A St M R A St M     при у(A); |N | , | , ( ), / / / / ( ), / / / / v u y v z u R A St M R A St M     при у(A); |R | | ( ), / / / / ( ), / / / / v x v x yR A St M R yA St M       при у{ ,v x }; |R | | ( ), / / / / ( ), / / / / v x v x yR A St M R yA St M       при у{ ,v x }; |R | | ( ), / / '/ / ( ), / / / / v y x z v x zR A St M R yA St M         ; |R | | ( ), / / '/ / ( ), / / / / v y x z v x zR A St M R yA St M       . Для |R та |R умови:  ,y v x , z тотально неістотне та znm   v xR A . При умові  ,y v x використовує- мо |R та |R; якщо  ,y v x , то викори- стовуємо |R та |R. Форми елімінації кванторів: |–  | | , / / '/ / , / / / / x yR A St M xA St M      ; –|  | | | , , / / / / , / / / / x zxA R A St M xA St M        . Для |– ім'я у тотально неістотне та уnт(, А). При цьому до носія A стану  додається новий елемент у. До вищенаведених форм додаємо базові форми для модальних операторів |RКi , |RКi , | Кi , | Кi , де iI: |RКi     | | , / / / / , / / / / v i x v x i K R A St M R K A St M     , де iI; |RКi     | | , / / / / , / / / / v i x v x i K R A St M R K A St M     , де iI. Секвенційні форми елімінації мода- льних операторів | Кi та | Кi записуються по-різному залежно від властивостей від- ношень досяжності i , iI. При цьому фо- рми | Кi зазвичай не змінюють (див. далі) множини базових даних станів і схему мо- делі світу, форма | Кi для стану  вводить Теоретичні та методологічні основи програмування 8 новий стан  такий, що i  та A A  . Розглянемо як приклад три випадки. Загальний випадок. Якщо на i не накладені умови, то маємо такі форми. | Кi 1| | | | , ,..., , // // K , // // n i A A A St M A St M         . Тут | A – допоміжна специфікова- на формула, яка конкретизується в даній секвенції через специфіковані 1| ,A  … ..., |n A  для всіх наявних в даний момент станів 1β ,...,βn таких, що 1,i  , i n  . Якщо таких станів немає, то вводимо новий стан β , додаємо i  до схеми моделі світу М та записуємо специ- фіковану формулу | A . | Кi | , // ' // { } K , // // i i St M A St M       , де  – це | | 1 |, ,..., mA B B   . Тут  – новий стан, 1, , mB B – усі формули, що фігурують в допоміжних спе- цифікованих формулах вигляду | jB , по- роджених формулами | i jK B  (якщо  міс- тить такі формули). Це означає, що при поя- ві нового стану , досяжного із , для до- поміжних формул вигляду | jB треба за- писати нові специфіковані формули β| jB . До схеми моделі світу М додаємо i  , для введеного нового стану  задаємо A A  . Відношення i транзитивне та ре- флексивне. Тоді маємо такі форми. | Кi | , // // K , // // i St M A St M    , де  – це 1| | | |, , , , , n A A A A      1 | |K , , K ni iA A    . Допоміжна | A конкретизується через 1| |, , n A A    та 1 | |K , , K ni iA A    для всіх наявних в даний момент станів 1, …, n таких, що 1, ,i i n    . Специфіковані формули 1| K ,i A  |, K n i A  тут необхідні через транзитив- ність відношення i . Явне виділення | A необхідне через рефлексивність відношен- ня i. | Кi | , // ' // { } K , // // i i St M A St M       , де  – це | | 1 | | 1 |, ,..., , K ,..., Km i i mA B B B B     . Тут  – новий стан, B1, …, Bm – усі формули, що фігурують в допоміжних спе- цифікованих формулах вигляду | jB , по- роджених формулами | Ki jB (якщо  їх містить). Специфіковані | Ki jB необхідні через транзитивність i. До схеми моделі світу М додаємо i  , для введеного но- вого стану  задаємо A A  (зауважимо, що нові елементи даних стану можуть далі з’являтися, наприклад, за рахунок |–-форм, як в A , так і в A ). Відношення i транзитивне, рефле- ксивне та симетричне. Маємо такі форми. | Кi | , // // K , // // i St M A St M    , де  – це 1| | |, , ,A A A    1| | |, , K , , K n ni iA A A      . Допоміжна | A конкретизується через специфіковані формули 1| ,A  |, n A  та 1 | |K , , K ni iA A    для всіх на- явних в даний момент станів 1, , n  та- ких, що 1, ,i i n    чи 1 ,i  , n i  . | Кi | , // ' // { , } K , // // i i i St M A St M         , де  – це | | 1 | | 1, , , , K ,m iA B B B    |, Ki mB . Тут симетричність i врахована додаванням i  та i  до М. Вищенаведені форми задають чис- лення кванторного рівня. Числення ММЛ кванторно-екваційного рівня можна роз- глядати як прикладні секвенційні числення Теоретичні та методологічні основи програмування 9 ММЛ кванторного рівня. Виведення в цих численнях – це виведення секвенцій з до- даними аксіомами для рівності (рефлексив- ності, симетричності, транзитивності, замі- ни рівних). Це означає: для кожного наяв- ного в секвенції стану  в ній мусять бути: |–   ,x x x  |–  x y x y y x     , |–  x y z x y y z x z        (тут x, y, z – тотально неістотні); |–      , , , , z u z u x v y vx y x y R p R p     для всіх pPs, , ,z u  (тут x, y – тотально неістотні, відмінні від z, ,u v ). Поява нового стану  веде до випи- сування усіх таких формул. Проте можна явно не вносити ці аксіоми до секвенції, а враховувати їх за потребою, подібно випа- дку загальних ТМС функціонально-еква- ційного рівня (див. [5]). Це означає моди- фікацію процедури побудови дерева. Для врахування аксіом симетрично- сті, транзитивності та заміни рівних вво- димо допоміжні форми: ЕSm | | | , , / / / / , / / / / x y y x St M x y St M         ; ЕTr | | | | | , , , / / / / , , / / / / x y y z x z St M x y y z St M             ; |–ЕPs , , | | , | , , | | , , ( ), ( ), / / / / ; , ( ), / / / / z u z u x v y v z u x v x y R p R p St M x y R p St M          –|ЕPs , , | | , | , , | | , , ( ), ( ), / / / / . , ( ), / / / / z u z u x v y v z u x v x y R p R p St M x y R p St M          Замкненість секвенції  визначаєть- ся виконанням однієї з наступних умов: С) існують формула  та префікс стану  такі, що |–  та –| ; СRf) –| x x   для деяких x V та префіксу стану  ; CE) |– x y  , –|Kix y   або –| x y  , |– Kix y   для деяких ,x y V , Ki Ms та префіксу стану . Умова СRf індукована аксіомою ре- флексивності, умова CE індукована влас- тивістю | Kix y x y    . Процедура побудови секвенційного дерева для числень ММЛ кванторно-еква- ційного рівня в основних рисах аналогічна відповідній процедурі для секвенційних числень логік квазіарних предикатів [2], але побудова дерева ведеться паралельно із по- будовою схем моделей світу. При застосу- ванні секвенційних форм схема моделі сві- ту залишається незмінною, окрім випадку | Кi-форм (інколи |Кi-форм), які додають нові стани, що дає розширення моделі сві- ту. Побудова дерева розбита на етапи. Кожне застосування секвенційної форми проводиться до скінченної множини до- ступних на даний момент формул. Спочатку виконуємо | Кi-форми, які додають нові стани, далі | Кi-форми. Потім виконуємо всі |–-форми, після цього – всі R-форми, далі – усі інші форми. При цьому –|-форма до –| xA  застосовується багатократно – для усіх імен доступних формул секвенції –| xA  ,  та її наступни- ків. За необхідності також робимо додат- кові кроки для продукування нових фор- мул-рівностей і додавання відповідних "копій" формул вигляду  , | , z u y vR p  чи  , | , z u y vR p . Це робимо так. Нехай на попередньому кроці була отримана (або стала доступною на початку етапу) формула | s t  . Тоді, згідно ЕSm, додаємо | t s  . Далі, згідно |–ЕPs та –|ЕPs, для кожної з наявних доступних формул вигляду  , |– , z u s vR p чи  , | , z u s vR p додає- мо відповідно  , | , z u t vR p  чи  , | , z u t vR p . Нехай після попереднього кроку ма- ємо (або доступні на початку етапу) | s t  та | t s  . Згідно ЕTr, додаємо | s r  . Враховуючи ЕSm, далі отриму- ємо | s t  , | t s  , | t r  , | r t  , | s r  , | r s  . Нехай на попередньому кроці була отримана (або стала доступною на початку Теоретичні та методологічні основи програмування 10 етапу) формула вигляду  , | , z u s vR p чи ви- гляду  , | , z u s vR p , причому серед доступ- них формул секвенції маємо | s t  та | t s  . Згідно |–ЕPs і –|ЕPs, для кожної з наявних доступних формул вигляду  , | , z u s vR p та  , | , z u s vR p додаємо відпо- відно  , | , z u t vR p та  , | , z u t vR p . Таких до- даткових кроків може бути декілька, згід- но наявності різних доступних формул ви- гляду | s t  . Враховуючи вищенаведені властиво- сті відношення |=, отримуємо: Теорема 2. Нехай | | | | // '// ' // // St M St M         та | | | | | | // // // // // // St M St M St M             – секвенційні форми. Тоді: – з умови  |=  випливає  |= ; – з умови  |=  та  |=  випливає  |= . 3. Теореми коректності та повноти Теорема коректності для секвенцій- них числень ММЛ формулюється тради- ційним чином. Теорема 3. Нехай секвенція |––| вивідна. Тоді  |= . Доведення проводиться індукцією за побудовою замкненого секвенційного дерева для секвенції |––|, воно аналогічне доведенню відповідної теореми для сек- венційних числень загальних ТМЛ [3]. Для доведення повноти секвенцій- них числень ММЛ кванторно-екваційного рівня використаємо метод систем модель- них множин [9, 3]. Розглядаємо тут більш загальний випадок Gn-ММС. Система модельних множин – це пара ({Н | S}, R), де S – множина ста- нів світу, R – множина відношень на S. Системи модельних множин записуємо також як ({Н | S}, M) де M – схема мо- делей світу, яка задається множиною R. Множина Н специфікованих фор- мул із W nm  (Н) – модельна множина стану  , якщо виконуються такі умови: MС) для кожної формули  лише одна з специфікованих формул | чи | може належати до Н; RfС) жодна специфікована формула ви- гляду | x x  , де xnm(Н), не може на- лежати до Н; EC) для кожної пари специфікованих формул вигляду | x y  , |Kix y  чи вигляду | x y  , | Kix y  , де x, ynm(Н), лише одна з формул пари може належати до Н; MSm) якщо | x y  Н, то | y x  Н; HTr) якщо | x y  Н тa | y z  Н, то | x z  Н; ЕPs) якщо | x y  Н тa  , | , z u y vR p Н, то  , | , z u x vR p Н ; якщо | x y  Н та  , | , z u y vR p Н, то  , | , z u x vR p Н ; MN) якщо  , | , y v z xR  Н та у(), то  | v xR  Н ; якщо  , | , y v z xR  Н та у   , то  | v xR  Н ; MT) якщо  , | , z v z xR  Н, то  | v xR   Н ; якщо  , | , z v z xR  Н, то  | v xR  Н ; M) якщо |Н, то |Н; якщо |Н, то |Н ; M) якщо |Н, то |Н або |Н ; якщо |Н, то |Н та |Н ; MRR) якщо   | v w x yR R  Н, то | ( )v w x yR  Н ; якщо   | v w x yR R  Н, то  | v w x yR  Н ; Теоретичні та методологічні основи програмування 11 MR) якщо  | v xR  Н, то  | v xR  Н ; якщо  | v xR  Н, то  | v xR  Н ; MR) якщо  | v xR  Н, то    | v v x xR R    Н ; якщо  | v xR  Н, то    | v v x xR R     H . MR) якщо  | v xR y    H та y ,v x , то  | v xyR   H ; якщо  | v xR y    H та y ,v x , то  | v xyR    H ; MRS) нехай z   x ynm R  та z тотально неістотне, тоді: якщо  | v xR y    H та y{ ,v x }, то  | v y x zzR   H ; якщо  | v xR y    H та y{ ,v x }, то  | v y x zzR    H ; MRК) якщо  | Kv x iR   H , то  | K v i xR   H ; якщо  | Kv x iR  Н, то  |K v i xR   H (тут iI); M) якщо | x  H , то існує y W таке:  | x yR    H ; якщо | x   H , то | ( )x yR   H для всіх y W ; MК) якщо | Ki Н, то |Н для всіх S таких, що i ; якщо |Ki Н, то |Н для деякого S такого, що i  (тут iI). MС, RfС та ЕС – це умови корект- ності модельної множини стану. Вони ін- дуковані відповідними умовами замкнено- сті секвенції. Процедура побудови секвенційного дерева може завершуватися або не завер- шуватися. Якщо процедура завершена по- зитивно, то маємо замкнене дерево. Якщо процедура завершена негативно або не за- вершується, то маємо скінченне чи нескін- ченне незамкнене дерево. Тоді в дереві іс- нує скінченний або нескінченний незамк- нений шлях. Кожна з формул початкової секвенції зустрінеться на цьому шляху і стане доступною. Теорема 4. Нехай  – незамкнений шлях в секвенційному дереві, Н – множи- на всіх специфікованих формул секвенцій шляху  із специфікацією стану |– чи –|, M – об'єднання усіх схем моделей світу секвенцій шляху. Тоді НM =({Н |  S},M) – система модельних множин. Для переходу від нижчої вершини шляху до вищої використовується одна з базових секвенційних форм. Переходи згі- дно таких форм відповідають пунктам ви- значення системи модельних множин. До- поміжні специфіковані формули (їхній префікс містить ) для модельних множин не беремо до уваги. Кожна непримітивна формула на шляху  рано чи пізно буде розкладена згідно відповідної секвенційної форми. Всі секвенції шляху  незамкнені, тому виконуються пункти MС, RfС, ЕС визначення системи модельних множин. Теорема 5. Нехай НM – система мо- дельних множин, побудована за незамкне- ним шляхом в секвенційному дереві, нехай НM = ({Н | S}, M) та W = nт(НM). Тоді існують ММС M = (S, R, А, Іт) та  V A з im() = W такі: 1) | H    T   ; 2) | H    F   . Зауважимо, що          для всіх S (ми розглядаємо Gn-ММС). Теорема 5 доводиться індукцією за складністю формули згідно побудови сис- теми модельних множин. Позначимо W nm  ( H ). Рівність індукує на W відношення еквівалентнос- ті: x  y | x y   H . Позначимо     {u | |– v = u H }=  |u   u . Тепер задамо     S v v   = = {u | |– v = u H для деякого S}. Теоретичні та методологічні основи програмування 12 Таке визначення коректне. Справді, для системи модельних множин НM, по- будованої за незамкненим шляхом  сек- венційного дерева, неможливо | x y   H та | x y  H для деяких  , S. Це зумовлене трактуванням рів- ності базових даних як їх тотожності: для одного і того ж даного d неможливо    d x d y  в одному стані та    d x d y  в іншому стані Задамо A = {[v] | vW ]. Тоді має- мо S A A   {[v] | vW ]. Тепер визначимо  = [v[v] | vW] та  = [v[v] | vW ]. Таке  – сюр'єкція WА, кожне  – сюр'єкція W А  . Задамо значення базових предика- тів на  та на іменних множинах вигля- ду  v xr  . Якщо | x y  H , то x  y, тому маємо    x y T     за побудовою  . Якщо | p  H , то візьмемо  p T   ; якщо | p  H , то візьмемо  p F   . Якщо  | v xR p  H , то візьмемо   v xp r T   ; якщо  | v xR p  H , то візьмемо   r v xp F   . В усіх інших випадках значення  p d задаємо довільним чином (достат- ньо розглядати d W A   ). При цьому врахо- вуємо еквітонність і обмеження стосовно неістотності імен: для всіх d, h W A   таких, що    || – || –d p h p   , необхідно    p d p h  . Задані таким чином значення базо- вих предикатів продовжимо за еквітонніс- тю, враховуючи умови неістотності імен, на відповідні h W A. Зрозуміло, що значен- ня базових предикатів задані однозначно, причому враховано неістотність для p імен у  p . Отже, значення базових пре- дикатів визначені коректно. Для атомарних формул чи вигляду  v xR p твердження 1) та 2) теореми випли- вають з визначення значень базових пре- дикатів. При цьому предикати вигляду p та  v xR p  еквітонні та тотальні на відпо- відних W A   . Із побудови НM випливає: якщо предикат (предикати), який є значенням простішої формули (права частина відпо- відних пунктів визначення H ), еквітон- ний і тотальний на W A   , то предикат, який є значенням формули, утвореної відповід- ною композицією (ліва частина пунктів визначення H ), теж еквітонний і тоталь- ний на W A   . Це гарантує еквітонність усіх предикатів  , якщо такими є базові пре- дикати на станах. Крок індукції для тверджень 1) та 2) доводиться стандартним чином (доведення аналогічних теорем для загальних ТМС див. [3, 5]). Наведемо для прикладу дове- дення для пунктів M та MК. Нехай | x  H . За визначенням НM існує y W таке, що  | ( )x yR   H . За припущенням індук- ції ( ( ))x yR    T   . Звідси  x   y T  . Але  y A  згідно y W , тому для а =  y A  маємо  x a T   , звідки    x T      . Нехай | x   H . За визначенням НM тоді |( ( ))x yR   H для всіх y W . За припущенням індукції ( ( ))x yR      F для всіх y W . Звідси   x y F    для всіх y W . Кожне b A має вигляд b =  y для де- якого y W , адже  визначає сюр'єкцію  : W A . Звідси  x b F   для всіх b A , тому    x F      . Теоретичні та методологічні основи програмування 13 Нехай | Ki  H , де Ki Ms. За визначенням НM тоді | H для всіх  таких, що i  . За припущенням індук- ції маємо   T   для всіх  таких, що i  . За визначенням Кi отримуємо    Ki    = T. Нехай |Ki  H , де Ki Ms. За визначенням НM тоді | H для деяко- го  такого, що i  . За припущенням індукції   F   . За визначенням Ki отримуємо    Ki    = F. Теорема 6. Нехай  |= . Тоді сек- венція |––| вивідна. Припустимо супротивне:  |=  (тоб- то  |=M  для кожної узгодженої ММС M), проте  = |––| невивідна. Тоді в сек- венційному дереві для  існує незамкне- ний шлях. Згідно теореми 4, НM = = ({ H | S}, M) – система модельних множин. Згідно теореми 5, існують ММС M = (S, R, А, Im) та  V A: | Н    T   та –| H    F   . Зо- крема, це вірно для формул секвенції |––|. Тому для всіх    маємо   T   та для всіх    маємо   F   . Це запе- речує  |=M , тому  | . Отримали супере- чність. Висновки У роботі досліджено першопорядкові композиційно-номінативні мультимодаль- ні логіки кванторно-екваційного рівня. На- ведено основні семантичні властивості та- ких логік, зокрема, властивості відношен- ня логічного наслідку для множин формул. На базі цих властивостей для мультимода- льних логік еквітонних предикатів кванто- рно-екваційного рівня запропоновано чис- лення секвенційного типу. Для побудова- них числень доведено теореми коректності та повноти. Дослідження семантичних і синтак- сичних властивостей першопорядкових композиційно-номінативних мультимода- льних та епістемічних логік будуть про- довжені для логік функціональних рівнів. 1. Андон Ф.И., Яшунин А.Е., Резниченко В.А. Логические модели интеллектуальных ин- формационных систем.– К.: 1999. – 396 с. 2. Нікітченко М.С., Шкільняк С.С. Математи- чна логіка та теорія алгоритмів. – К.: ВПЦ Київський університет, 2008. – 528 с. 3. Шкільняк О.С. Композиційно-номінативні модальні та темпоральні логіки: семантичні властивості, секвенційні числення // Наукові записки НаУКМА. Сер.: Комп’ютерні на- уки. – 2008. – Т. 86. – C. 25–34. 4. Шкільняк О.С. Семантичні властивості ком- позиційно-номінативних модальних логік // Проблеми програмування. – 2009. – № 4. – C. 11–23. 5. Шкільняк О.С. Секвенційні числення ком- позиційно-номінативних модальних логік функціонально-екваційного рівня // Про- блеми програмування. – 2011. – № 1. – C. 17–28. 6. Шкільняк О.С., Шкільняк C.С. Композицій- но-номінативні логіки епістемічного типу // Наукові записки НаУКМА. Сер.: Комп’ю- терні науки. – 2011. – Т. 125. – C. 4–7. 7. Шкільняк О.С., Шкільняк С.С. Kомпозиційно-номінативні мультимодаль- ні логіки // Штучний інтелект. – 2011. – № 4. – C. 126 –133. 8. Нікітченко М.С., Шкільняк О.С., Шкіль- няк С.С. Побудова модальних логік темпо- рального та епістемічного типу на основі композиційно-номінативного підходу // Ві- сник Київського ун-ту. Серія: фіз.-мат. на- уки. – 2011. – Вип. 3. – С. 204–211. 9. Семантика модальных и интенсиональных логик. – M.: Прогресс, 1981. – 494 с. Одержано 10.02.2012 Про автора: Шкільняк Оксана Степанівна, кандидат фізико-математичних наук, асистент кафедри інформаційних систем. Місце роботи автора: Київський національний університет імені Тараса Шевченка, 01601, м. Київ, вул. Володимирська, 60. Тел.: (044) 259 0511, (044) 522 0640 (д) e-mail: me.oksana@gmail.com mailto:me.oksana@gmail.com

Схожі ресурси