Composition nominative modal logics of partial non-monotone predicates and their calculi

We consider new program-oriented logical formalisms of modal type – pure first-order composition nominative modal logics of partial predicates without monotonicity restriction. For such logics we specify semantic models and languages and investigate interactions of modal compositions with renominati...

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2018
Автори:	Shkilniak, O.S., Kasianiuk, V.S., Malutenko, L.M.
Формат:	Стаття
Мова:	Ukrainian
Опубліковано:	Інститут програмних систем НАН України 2018
Теми:	modal logic partial predicate logical consequence sequent calculus UDC 004.42:510.69
Онлайн доступ:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/317
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Problems in programming
Завантажити файл:

Репозитарії

Problems in programming

id	pp_isofts_kiev_ua-article-317
record_format	ojs
resource_txt_mv	ppisoftskievua/9f/4716b01bb7a07c408ef9ae20f33e409f.pdf
spelling	pp_isofts_kiev_ua-article-3172024-04-28T11:52:03Z Composition nominative modal logics of partial non-monotone predicates and their calculi Композиционно-номинативные модальные логики немонотонных частичных предикатов и их исчисления Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення Shkilniak, O.S. Kasianiuk, V.S. Malutenko, L.M. modal logic; partial predicate; logical consequence sequent calculus UDC 004.42:510.69 модальная логика; частичный предикат; логическое следствие; секвенциальное исчисление УДК 004.42:510.69 модальна логіка; частковий предикат; логічний наслідок; секвенційне числення УДК 004.42:510.69 We consider new program-oriented logical formalisms of modal type – pure first-order composition nominative modal logics of partial predicates without monotonicity restriction. For such logics we specify semantic models and languages and investigate interactions of modal compositions with renominations and quantifiers. A consequence relation for two formulas in a given state is introduced and generalized to a logical consequence relation for two sets of formulas specified with states. We describe properties of a logical consequence relation for sets of formulas specified with states and properties of modalities elimination for various reachability relations. Sequent type calculi are proposed for general transitional and temporal modal logics of non-monotone predicates. We define various types of the calculi for different reachability relations and specify their basic sequent forms and sequent closure conditions. We give a step-by-step description of a deriving process (building of a sequent tree) by the introduced calculi. For these calculi we prove the soundness theorem and the theorem about existence of a counter-model for a non-closed path in a sequent tree. The counter-model is obtained using the Hintikka sets method. The proof of the completeness theorem is based on the theorem about existence of a counter-model.Problems in programming 2017; 2: 24-39 Исследованы новые программно-ориентированные логические формализмы модального типа – композиционно-номинативные модальные логики немонотонных частичных предикатов. Описаны семантические модели и языки этих логик, рассмотрено взаимодействие модальных композиций с реноминациями и кванторами. Введено отношение следствия для формул в данном состоянии, оно обобщено до отношения логического следствия для множеств специфицированных состояниями формул. Для общих и темпоральных модальных логик немонотонных предикатов построены исчисления секвенциального типа. Описаны разновидности этих исчислений, для них доказаны теорема корректности и теорема о существовании контрмодели для незамкнутого пути в секвенциальном дереве. На основе теоремы о контрмодели доказана теорема полноты.Problems in programming 2017; 2: 24-39 Досліджено нові програмно-орієнтовані логічні формалізми модального типу – композиційно-номінативні модальні логіки немонотонних часткових предикатів. Описано семантичні моделі та мови цих логік, розглянуто основні семантичні властивості. Введено відношення наслідку для формул у стані, описано властивості відношення логічного наслідку для множин специфікованих станами формул. На цій основі для загальних i темпоральних модальних логік немонотонних предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них доведено теореми коректності й повноти.Problems in programming 2017; 2: 24-39 Інститут програмних систем НАН України 2018-11-19 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/317 10.15407/pp2017.02.024 PROBLEMS IN PROGRAMMING; No 2 (2017); 24-39 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2017); 24-39 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2017); 24-39 1727-4907 10.15407/pp2017.02 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/317/312 Copyright (c) 2018 PROBLEMS OF PROGRAMMING
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2024-04-28T11:52:03Z
collection	OJS
language	Ukrainian
topic	modal logic partial predicate logical consequence sequent calculus UDC 004.42:510.69
spellingShingle	modal logic partial predicate logical consequence sequent calculus UDC 004.42:510.69 Shkilniak, O.S. Kasianiuk, V.S. Malutenko, L.M. Composition nominative modal logics of partial non-monotone predicates and their calculi
topic_facet	modal logic partial predicate logical consequence sequent calculus UDC 004.42:510.69 модальная логика частичный предикат логическое следствие секвенциальное исчисление УДК 004.42:510.69 модальна логіка частковий предикат логічний наслідок секвенційне числення УДК 004.42:510.69
format	Article
author	Shkilniak, O.S. Kasianiuk, V.S. Malutenko, L.M.
author_facet	Shkilniak, O.S. Kasianiuk, V.S. Malutenko, L.M.
author_sort	Shkilniak, O.S.
title	Composition nominative modal logics of partial non-monotone predicates and their calculi
title_short	Composition nominative modal logics of partial non-monotone predicates and their calculi
title_full	Composition nominative modal logics of partial non-monotone predicates and their calculi
title_fullStr	Composition nominative modal logics of partial non-monotone predicates and their calculi
title_full_unstemmed	Composition nominative modal logics of partial non-monotone predicates and their calculi
title_sort	composition nominative modal logics of partial non-monotone predicates and their calculi
title_alt	Композиционно-номинативные модальные логики немонотонных частичных предикатов и их исчисления Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення
description	We consider new program-oriented logical formalisms of modal type – pure first-order composition nominative modal logics of partial predicates without monotonicity restriction. For such logics we specify semantic models and languages and investigate interactions of modal compositions with renominations and quantifiers. A consequence relation for two formulas in a given state is introduced and generalized to a logical consequence relation for two sets of formulas specified with states. We describe properties of a logical consequence relation for sets of formulas specified with states and properties of modalities elimination for various reachability relations. Sequent type calculi are proposed for general transitional and temporal modal logics of non-monotone predicates. We define various types of the calculi for different reachability relations and specify their basic sequent forms and sequent closure conditions. We give a step-by-step description of a deriving process (building of a sequent tree) by the introduced calculi. For these calculi we prove the soundness theorem and the theorem about existence of a counter-model for a non-closed path in a sequent tree. The counter-model is obtained using the Hintikka sets method. The proof of the completeness theorem is based on the theorem about existence of a counter-model.Problems in programming 2017; 2: 24-39
publisher	Інститут програмних систем НАН України
publishDate	2018
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/317
work_keys_str_mv	AT shkilniakos compositionnominativemodallogicsofpartialnonmonotonepredicatesandtheircalculi AT kasianiukvs compositionnominativemodallogicsofpartialnonmonotonepredicatesandtheircalculi AT malutenkolm compositionnominativemodallogicsofpartialnonmonotonepredicatesandtheircalculi AT shkilniakos kompozicionnonominativnyemodalʹnyelogikinemonotonnyhčastičnyhpredikatoviihisčisleniâ AT kasianiukvs kompozicionnonominativnyemodalʹnyelogikinemonotonnyhčastičnyhpredikatoviihisčisleniâ AT malutenkolm kompozicionnonominativnyemodalʹnyelogikinemonotonnyhčastičnyhpredikatoviihisčisleniâ AT shkilniakos kompozicíjnonomínativnímodalʹnílogíkinemonotonnihčastkovihpredikatívtaíhčislennâ AT kasianiukvs kompozicíjnonomínativnímodalʹnílogíkinemonotonnihčastkovihpredikatívtaíhčislennâ AT malutenkolm kompozicíjnonomínativnímodalʹnílogíkinemonotonnihčastkovihpredikatívtaíhčislennâ
first_indexed	2024-09-16T04:08:32Z
last_indexed	2024-09-16T04:08:32Z
_version_	1818568448990511104
fulltext	Теоретичні та методологічні основи програмування © О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко, 2017 24 ISSN 1727-4907. Проблеми програмування. 2017. № 2 УДК 004.42:510.69 О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко КОМПОЗИЦІЙНО-НОМІНАТИВНІ МОДАЛЬНІ ЛОГІКИ НЕМОНОТОННИХ ЧАСТКОВИХ ПРЕДИКАТІВ ТА ЇХ ЧИСЛЕННЯ Досліджено нові програмно-орієнтовані логічні формалізми модального типу – композиційно- номінативні модальні логіки немонотонних часткових предикатів. Описано семантичні моделі та мо- ви цих логік, розглянуто основні семантичні властивості. Введено відношення наслідку для формул у стані, описано властивості відношення логічного наслідку для множин специфікованих станами фо- рмул. На цій основі для загальних i темпоральних модальних логік немонотонних предикатів побу- довано числення секвенційного типу. Описано різновиди цих числень, для них доведено теореми ко- ректності й повноти. Ключові слова: модальна логіка, частковий предикат, логічний наслідок, секвенційне числення. Вступ Для моделювання предметних об- ластей та опису інформаційних і програ- мних систем успішно використовуються модальні логіки, в першу чергу темпора- льні та епістемічні. Апарат темпоральних логік застосовується для моделювання динамічних систем, специфікації та вери- фікації програм. Для опису експертних систем, баз даних і баз знань використо- вуються епістемічні логіки. Традиційні модальні логіки базуються на класичній логіці предикатів. Проте класична логіка має [1] принципові обмеження, вона не- достатньо враховує частковість та непов- ноту інформації про предметну область. Тому набуває актуальності проблема по- будови нових, програмно-орієнтованих логічних формалізмів модального типу. Такими є композиційно-номінативні мо- дальні логіки (КНМЛ), які поєднують мо- жливості традиційних модальних логік [2] і композиційно-номінативних логік [1, 3] часткових квазіарних предикатів. Низку класів КНМЛ побудовано і досліджено, зокрема, в [4–6]. Транзиційні модальні логіки (ТМЛ) відбивають аспект зміни й розвитку предметних областей, описуючи переходи від одного стану світу до іншо- го, вони є найважливішим класом КНМЛ. В межах ТМЛ природним чином розгля- даються традиційні модальні логіки. Під- класами ТМЛ є темпоральні (ТмМЛ) та мультимодальні (ММЛ) логіки, в межах ММЛ далі виділено ТМЛ епістемічного типу та загальні ТМЛ (ЗМЛ). Метою даної роботи є дослідження чистих першопорядкових ТМЛ часткових квазіарних предикатів без обмеження мо- нотонності. ТМЛ немонотонних предика- тів запропоновано в [7], вони вивчались в [8, 9]. В даній статті розглянуто семан- тичні й синтаксичні аспекти ТМЛ немо- нотонних предикатів. Описано відношен- ня логічного наслідку для множин специ- фікованих станами формул, на цій основі для ЗМЛ та ТмМЛ немонотонних преди- катів побудовано числення секвенційного типу. Отримано різновиди цих числень залежно від властивостей відношень пе- реходу на станах світу, для таких числень доведено теореми коректності й повноти. Поняття, які в цій роботі не визна- чаються, тлумачимо в сенсі [1, 3, 8]. 1. Транзиційні модальні системи та їх різновиди Центральним для КНМЛ є поняття композиційно-номінативної модальної си- стеми (КНМС). КНМС – це об’єкт вигляду M = (Cms, Fт, Iт), де Cms = (S, R, Pr, C) – композиційна модальна система, вона за- дає семантичні аспекти світу, Fm – мно- жина формул мови КНМЛ, Iт – відобра- ження інтерпретації формул, S – множина станів світу, R – множина відношень на S, Теоретичні та методологічні основи програмування 25 Pr – множина предикатів на станах, C – множина композицій на Pr. Найважливішим класом КНМС є транзиційні модальні системи (ТМС). У випадку ТМС R складається з відношень вигляду R  S  S, трактуємо їх як відно- шення переходу на станах. Для чистих першопорядкових ТМС S – це множина алгебраїчних систем вигляду  = (A, Pr), C задається базовими загальнологічними композиціями і базовими модальними композиціями, A – множина базових да- них стану , Pr – множина квазіарних предикатів вигляду VA  {T, F}, це преди- кати стану . Предикати вигляду VA {T, F}, де S A A   , назвемо глоба- льними. Базовими загальнологічними ком- позиціями вважаємо логічні зв’язки  та , композиції реномінації R v x та квантифіка- ції x. Логічні зв’язки , &,  є похідни- ми, вони виражаються  та ; композиції квантифікації x виражаються  та x (див. [1, 3]). Мультимодальні ТМС (ММС) – це ТМС із { \| }iR i I  та базовими модаль ними композиціями Кi, iI, де кожному i R зіставлено відповідну Кi. Загальні ТМС (ЗМС) є окремим ви- падком ММС, у них }{R та єдина ба- зова модальна композиція  (необхідно). ТМС, у яких }{R , а базовими модальними композиціями є  (завжди буде) та  (завжди було), називають те- мпоральними (ТмМС). Для загальних ТМС задають похід- ну композицію  (можливо): Р означає Р. Для ТмМС задають похідні ком- позиції  (колись буде) і  (колись бу- ло): Р означає Р, Р означає Р. Далі обмежимось розглядом ЗМС та ТмМС, в першу чергу зосереджуючись на ЗМС. Отримані результати природним чи- ном переносяться на випадок ММС. Опишемо мови чистих першопоря- дкових ТМС. Алфавіт мови: множини V предметних імен (змінних) та Ps предика- тних символiв (сигнатура мови); символи базових загальнологічних композицій , , , v xR x; множина Ms символів базо- вих модальних композицій (модальна си- гнатура). У випадку ЗМС Ms = , у випад- ку ТмМС Ms = , . В мовах ЗМС множина Fт формул визначається так. Маємо Ps  Fт, такі фо- рмули атомарні; далі задаємо: , Fт   , Ф, , v xR  x,   Fт. В мовах ТмМС множину Fт задає- мо так. Маємо Ps  Fт, а далі: , Fт   , Ф, , v xR  x, ,   Fт. При запису формул будемо вживати (див. [1]) символи похідних композицій , &, , x. Наприклад, x означає x. Тип ТМС визначається сигнатурою мови та сигнатурою неістотності. Таку си- гнатуру задаємо за допомогою тотальної функції  : Ps2V, яку (див. [1]) продовжу- ємо до  : Fr2V. Атомарні формули та формули ви- гляду , v xR p де pPs та (p) { } ,v  на- звемо примітивними. Формули вигляду ( ) x yR  назвемо R-формулами. Визначимо відображення інтерпре- тації формул на станах. Спочатку задаємо Iт : Рs  S Pr, при цьому має бути Iт(p, )  Pr (базові предикати є предика- тами станів). Продовжимо Iт до відобра- ження Iт : Fт  S Pr так: Iт(, ) = (Iт(, )); Iт(, ) = (Iт(, ), Iт(, )); ( , ) R ( ( , )); v v x xIm R Im     Iт(x, )(d) = , якщо існує : ( , )( ) , , якщо ( , )( ) для всіх , невизначене в усіх інших випадках. T a A Im d x a T F Im d x a F a A               Iт(, )(d) = Теоретичні та методологічні основи програмування 26 , якщо ( , )( ) для всіх : , , якщо існує : та ( , )( ) , невизначене в усіх інших випадках. T Im d T S F S Im d F               Якщо для S не існує :   , то Iт(, )(d) для кожного dVA. У випадку ТмМС для формул ви- гляду  та  маємо: Iт(, )(d) = , якщо ( , )( ) для всіх : , , якщо існує : та ( , )( ) , невизначене в усіх інших випадках. T Im d T S F S Im d F               Якщо для S не існує :   , то Iт(, )(d) для кожного dV. Iт(, )(d) = , якщо ( , )( ) для всіх : , , якщо існує : та ( , )( ) , невизначене в усіх інших випадках. T Im d T S F S Im d F               Якщо для S не існує :   , то Iт(, )(d) для кожного d VA. Предикати, які є значеннями не- модалізованих формул (при їх побудові не використовуємо символи модадьних композицій ), належать до предикатів станів. Предикат Iт(, ), який є значен- ням формули  у стані , позначаємо . Формула  неспростовна (частково істинна) в ТМС M (позн. M \|= ), якщо  неспростовний для всіх S. Формула  неспростовна, або час- тково істинна (позн. M \|= ), якщо M \|=  для всіх ТМС M одного типу. ТМС будемо також подавати у ви- гляді M = (S, R, А, Iт). Залежно від умов, накладених на відношення переходу , можна визначати різні класи ТМС. Традиційними є випадки, коли  рефлексивне, симетричне чи тран- зитивне. Якщо  рефлексивне, то до назви ТМС додаємо R; якщо транзитивне, то до- даємо T; якщо симетричне, то додаємо S. Отримуємо такі типи ЗМС та ТмМС: R-ЗМС, T-ЗМС, S-ЗМС, RT-ЗМС, RS-ЗМС, TS-ЗМС, RTS-ЗМС; R-ТмМС, T-ТмМС, S-ТмМС, RT- ТмМС, RS-ТмМС, TS-ТмМС, RTS-ТмМС. Якщо симетричне, завжди маємо Iт(, )(d) = Iт(, )(d). Це означає, що дія композицій  та  ідентична, це фактично композиція . Отже, якщо  симетричне, то типи S-ТмМС, RS- ТмМС, TS-ТмМС, RTS-ТмМС цілком іден- тичні типам S-ЗМС, RS-ЗМС, TS-ЗМС, RTS-ЗМС. 2. Семантичні властивості ТМЛ Стисло опишемо основні семантич- ні властивості ТМЛ. Теорема 1. Композиції ,  та  зберігають еквітонність (монотонність). Наведемо доведення для , для  та  доведення аналогічне. Нехай  еквітонний і для кожного  такого, що ,  предикат  екві- тонний. Нехай d, d’VA, d  d’, (d). Нехай (d) = F. Тоді для деякого  такого, що ,  маємо (d) = F. Однак d  d’, тому за еквітонністю  маємо (d’) = F, звідки ()(d’) = F. Нехай (d) = T. Тоді для кожно- го  такого, що ,  маємо (d) = T. Згі- дно d  d’ для кожного такого  за екві- тонністю  тоді (d’) = T, тому (d’) = T. Таким чином,  еквітонний. Композиції , , R , v x x зберігають [1] еквітонність. Звідси такий наслідок. Наслідок 1. Базові композиції ЗМС та ТмМС зберігають еквітонність. Властивості композицій реномінації R, RI, RU, RR, R, R, RR (див. [3]), в яких мовиться про рівність предикатів, справджуються для предикатів ТМС. На формули ТМЛ переноситься відоме [3] поняття Rs-Un-еквівалентності. Для визначення цього поняття, а також для елімінації кванторів використовують [3] спеціальні предикати-індикатори Ez, які визначають наявність в даних компоненти з іменем zV. Предикати Ez задаємо так: E(z) = T, якщо d(z); E(z) = F, якщо d(z). Теоретичні та методологічні основи програмування 27 Rs-формою R-формули ),(,, ,, vux zyxR де { } ( ),  u назвемо R-формулу ( ),v zR утворену із , , , , ( ) x u v x y zR  всеможливими спрощеннями реномінації на основі влас- тивостей R, RI, RU, RR (застосування R дає Rs-форму , яка може не бути R- формулою). Нехай Un  V – множина імен, тра- ктованих як неозначені (Un задаємо за допомогою предикатів-індикаторів Ez), а символ V позначає відсутність зна- чення. Нехай R-формула uxr vysR ,, ,, така:  UnvxUnysr },{ ,},,{ . Un-форма формули uxr vysR ,, ,, – це вираз ux vR , , . R-формули  та  назвемо Rs-Un- еквівалентними (позн  Un ), якщо  та  мають однакові Rs-форми або ці Rs- форми мають однакові Un-форми. Якщо R-формули  та  – Rs-Un- еквівалентні, то  та  теж будемо на- зивати Rs-Un-еквівалентними. Вважаємо, що для формули , яка не є R-формулою чи запереченням R-формули, її Un-форма збігається із . Таким чином, кожна фор- мула Rs-Un-еквівалентна сама собі. Нехай M = (St, R, A, Im) – ТМС. Не- хай Un  V – множина імен, трактованих як неозначені в стані St. Теорема 2. Якщо  Un , то для всіх Ad UnV \  маємо (d) = (d). Зауважимо, що Ad UnV \  означає: Eu(d) = F для всіх uUn. Розглянемо взаємодію в ТМС мода- льних композицій із реномінаціями і кван- торами. Обмежимось випадком ЗМС. Символи модальних композицій можна проносити [7] через реномінації. Теорема 3. v xR (d) =  v xR (d) для довільних , St, dVA. Звідси випливає: кожна формула вигляду )(v xR )(v xR неспростов- на. Розглянемо взаємодію модальних композицій та кванторів. Для ЗМЛ еквітонних предикатів формули xx та xx є неспростовними (див. [1, 7]). Це не так для загального випадку нееквітонних (не- монотонних) предикатів, для цих формул в [7] побудовані контрмоделі – ЗМС, в яких ці формули спростовні. Приклад 1. xx та xx – спростовні формули. Побудуємо ЗМС, в якій спростову- ється xx. Нехай St = {, }, R = {  }, A = {a}, A = {b}. Нехай для рPs неістотні усі імена, окрім x. Задамо р() = F, р() = F, р( ][ bx ) = T. Тоді xр() = T, звідки xр() = T. Маємо р( ][ ax ) = р([ ]x a  ) = = р() = F, адже [ ]x a    , звідки р( ][ ax ) = F, тому xр() = F. Отримали (xрxр)() = F, що дає  \| xрxр. Побудуємо ЗМС, в якій спростову- ється xx. Нехай St = {, }, R = {  }, A = {a, b}, A = {b}. Нехай для рPs неістотні усі імена, окрім x, y. Задамо р( ][ by ) = T, р( ],[ bybx  ) = F. Згі- дно A = {b} із р( ],[ bybx  ) = F маємо xр( ][ by ) = F, звідки випливає, що xр( ][ by ) = F. Із р( ][ by ) = T ма- ємо р( ],[ byax  ) = T, звідки отри- муємо xр( ][ by ) = T. Отже, (xрxр)([ ]y b ) = F, звідки  \| xрxр. Зауважимо, що в цих ЗМС предикат р нееквітонний. Отже, для загального випадку ЗМЛ немонотонних (нееквітонних) пре- дикатів xx та xx – спростовні формули, тобто вони не є істинними. Приклад 2 (див.[1, 7]). Формули xx та xx спрос- товні для ЗМС еквітонних предикатів. Теоретичні та методологічні основи програмування 28 Побудуємо ЗМС еквітонних преди- катів, у якій спростовуються такі формули. Нехай St = {, }, R = {  }, A = {a}, A = {a, b}, а для рPs неістотні усі імена, окрім x. Задамо р([ ]x a ) = F, р( ][ ax ) = F, р([ ]x b ) = T. Тоді маємо (р)( ][ ax ) = F, а згідно A = {a} звідси (xр)( ][ ax ) = F. Згідно р([xb]) = T маємо (x р)( ][ ax ) = T, звідки отриму- ємо (x р)( ][ ax ) = T. Таким чином, (x рxр)( ][ ax ) = F, звідки ви- пливає  \| x рxр. Нехай для qPs неістотні усі імена, окрім x. Задамо q( ][ ax ) = T, q( ][ ax ) = T, q( ][ bx ]) = F. Тоді має- мо (x q)([ ]x a ) = F, звідки отримуємо (x q)([ ]x a ) = F. Маємо R = {  }, тому q([ ]x a ) = T  (q)( ][ ax ) = T. Згідно A = {a} тоді (xq)( ][ ax ) = T. Отже, (xqx q)( ][ ax ) = F, звід- ки  \|xqx q. Наслідок 2. В загальному випадку ЗМЛ формули xx та xx спростовні. Аналогічні твердження формулює- мо для ТмМС. Розглянемо відношення логічного наслідку на множині специфікованих ста- нами формул. Специфікована станом формула – це об’єкт вигляду , де  – формула мо- ви,  – її специфікація (відмітка). Тут S, де S – певна множина імен станів світу. Отже, специфікація вказує на стан світу, в якому розглядається предикат, що є зна- ченням цієї формули. Oпишемо відношення наслідку M\|= для двох формул в стані  (специфікова- них станом ) ТМС M. Це робимо аналогі- чно визначенню відношення неспростовні- сного наслідку при фіксованій інтерпрета- ції в логіках часткових однозначних квазі- арних предикатів (див. [1, 3]).  M\|= , якщо для кожного dVA маємо: (d) = T  неможливо (d) = F. Для відношення M\|= отримуємо:  M\|=   M\|= ()   \|= ;  M\|   M\| ()   \|   існує dVA таке, що (d) = T та (d) = F. Зокрема: M\|    \|   існує dVA таке, що (d) = F. Звідси: M\|=    \|=   (d)  F для всіх dVA   неспростовний. Відношення M\|= наслідку для двох формул в стані  індукує відношення екві- валентності M двох формул в стані . Відношення M задаємо так:  M    M\|=  та  M\|= . Для відношення M отримуємо:  M   M\|= ()   \|= . Узагальнимо відношення наслідку для двох формул в стані  ТМС M до від- ношення наслідку для двох множин спе- цифікованих станами формул в узгодженій із ними ТМС M. Нехай  – множина специфікованих станами формул, причому ці специфікації утворюють множину S. Множина  узго- джена із ТМС M = (St, R, A, Im), якщо за- дана ін’єкція S у St. Нехай  та  – множини специфіко- ваних станами формул.  є наслідком  в узгодженій із ними ТМС M (позн.  M\|= ), якщо для всіх dVA маємо: (d) = T для всіх   Ψ(d)  F для деякого Ψ. Надалі запис  M\|=  за умовчанням означатиме узгодженість  та  із ТМС M. Із визначення випливає:  M\|   існує dVA таке, що для всіх  маємо (d) = T та для всіх Ψ маємо Ψ(d) = F.  є логічним наслідком  (відносно ТМС певного типу), якщо  M\|=  для всіх ТМС M (які належать до цього типу). Цей факт позначаємо  \|= . Введене відношення логічного нас- лідку \|= відповідає відношенню \|=IR [3] не- Теоретичні та методологічні основи програмування 29 спростовнісного логічного наслідку в логі- ках часткових квазіарних предикатів. Сформулюємо умову відсутності відношення логічного наслідку для двох множин специфікованих станами формул.  \|   існують узгоджена із  та  ТМС M = (St, R, A, Im) та dVA такі: (d) = T для всіх  та Ψ(d) = F для всіх Ψ. 3. Властивості відношення логічного наслідку Розглянемо властивості відношення логічного наслідку для множин специфіко- ваних станами формул. Немодальні властивості відношення \|= повторюють відповідні властивості від- ношення \|=IR (див. [3]). Найперше це на- ступні властивості: M) якщо  \|= ,    та   , то  \|=  (монотонність відношення \|=); СB) ,  \|= ,  (базова умова га- рантованої наявності відношення \|=). Нехай  та  – множини специфіко- ваних формул, Un = {x \| Ex}. Загальну умову гарантованої наяв- ності \|= отримуємо на основі теореми 2: С)  Un   ,  \|= , . Властивості еквівалентних перетво- рень отримуються на основі наведених в [3] властивостей R, RI, RU, RR, R, R, RR. Кожна така властивість R продукує дві властивості RL та RR для відношення \|=, коли виділена формула знаходиться у лівій чи правій його частині: RL) R(),  \|=   ,  \|= ; RR)  \|= R(),    \|= , ; RIL) , , ( ) ,z v z xR   \|=   ( ) ,v xR   \|= ; RIR)  \|= , , ( ) ,z v z xR     \|= ( ) ,v xR   . За умови z() маємо: RUL) , , ( ) ,z v y xR   \|=   ( ) , v xR \|= ; RUR)  \|= , , , ( )z v y xR    \|= , ( )v xR  . RRL) ( ( )) ,v w x yR R   \|=    ( ) ,v w x yR   \|= ; RRR)  \|= , ( ( ))v w x yR R     \|= , ( )v w x yR  ; RL) ( ) ,v xR   \|=   ( ) ,v xR    \|= ; RR)  \|= , ( )v xR    \|= , ( )v xR   ; RL) ( ) ,v xR   \|=    ( ) ( ) ,v v x xR R     \|= ; RR)  \|= , ( )v xR     \|= , ( ) ( )v v x xR R    ; RRL) , ,R ( ) , \|u x v y x =      R ( ) , \|u v x =    ; RRR) , ,\| ,R ( )u x v y= x       \| ,R ( )u v= x     . Подібно до RL та RR формулює- мо властивості для похідних логічних зв'я- зок  та , подібно до RRL та RRR – властивості RRL та RRR. До властивостей еквівалентних пе- ретворень відносяться також властивості пронесення модальностей через реноміна- цію. У випадку ЗМС маємо: RL) , ( ) \|v xR      , ( ) \|v xR     ; RR) \| , ( )v xR      \| , ( )v xR     . У випадку ТмМС маємо: RL) , ( ) \|v xR      , ( ) \|v xR     ; RR) \| , ( )v xR      \| , ( )v xR     ; RL) , ( ) \|v xR      , ( ) \|v xR     ; RR) \| , ( )v xR      \| , ( )v xR     . Властивості декомпозиції формул: L) ,  \|=    \|= , ; R)  \|= ,   ,  \|= ; L) ,  \|=   ,  \|=  та ,  \|= ; R)  \|= ,    \|= , , . Теоретичні та методологічні основи програмування 30 Наведемо властивості елімінації кванторів; для їх опису використаємо спе- ціальні предикати-індикатори Ez: L) за умови zfu(, , х) маємо х,  M \|=   ( ) , , \|x z MR Ez     ; RL) за умови z ))(,,(  xRfu u v маємо ( ) , \|u v MR x        , , ( ) , , \|u x v z MR Ez     ; vR) Ey,  M \|= х,    , \| , ( ) ,x M yEy x R        ; RvR) , \| , ( )u M vEy R x        , ,, \| , ( ) , ( )u u x M v v yEy R x R        . Подібним чином формулюємо влас- тивості декомпозиції для  та  та влас- тивості елімінації кванторів x. Bластивості E-розподілу та первіс- ного означення: Ed)  \|=   Ey,  \|=  та  \|= , Ey; Ev)  \|=   Ez,  \|=  за умови zfu(, ). Наведемо властивості елімінації модальностей. У випадку ЗМС маємо: L) ,  \|=   { \|  } \|= ; R)  \|= ,    \|= ,  для всіх S таких, що   . У випадку ТмМС маємо: L) ,  \|=   { \|  } \|= ; R)  \|= ,    \|= ,  для всіх S таких, що   . L) ,  \|=   { \|  } \|= ; R)  \|= ,    \|= ,  для всіх S таких, що   . Зауважимо, що властивості для  записуємо аналогічно властивостям для . Для властивостей відношення \|= до- цільно вказати відповідні дуальні власти- вості відношення \|, за якими безпосеред- ньо виписуємо секвенційні форми. Для на- ведених властивостей відношення \|=, окрім L та R (R та R у випадку ТмМС) від- повідні властивості відношення \| отриму- ємо заміною символа \|= на символ \|. Наприклад, для L та R маємо: L) ,  \|   ,  \|  або ,  \| ; R)  \| ,    \| ,  для деякого S такого, що   . При наявності додаткових умов, на- кладених на  , властивості елімінації мо- дальностей відповідним чином модифіку- ються. Розглянемо випадки, коли  може бути транзитивними, рефлексивними чи симетричними. Запишемо дуальні власти- вості для \| у випадку ЗМС. 1.  рефлексивне. Маємо L та R;   для L дає умову { \|  }. 2.  симетричне. L та R запису- ємо так (маємо     ): LS) ,  \|    { \| чи     } \| . RS)  \| ,    \| ,  для деякого S такого: чи     . 3.  рефлексивне й симетричне. Маємо RS та LS, при цьому в силу   для LS умова { \| чи     }. 4.  транзитивне. Маємо R та LТ) ,  \|    { \|  }{ \|  } \| . Наявність { \|  } необхід- на через транзитивність відношення  . 5.  транзитивне й рефлексивне. Маємо R та LТ, причому в силу   для LТ умова { \|  }. 6.  транзитивне й симетричне. Тоді маємо RS та LТS) ,  \|    { \| чи     } { \| чи     } \| . Теоретичні та методологічні основи програмування 31 7.  транзитивне, рефлексивне й симетричне. Маємо RS та LТS, причому для LТS умова { \| чи     }. Подібним чином дуальні властивос- ті елімінації модальностей формулюємо для ТмМС. При цьому властивості для  записуються аналогічно відповідним влас- тивостям для . Якщо симетричне, то властивості для  та  ідентичні, це фа- ктично властивості для . 4. Секвенційні числення чистих першопорядкових ТМЛ В цій роботі зосередимося на чис- леннях ЗМЛ. Подібним чином можна розг- лядати числення ММЛ. Числення ТмМЛ отримуємо з числень ЗМЛ розщепленням секвенційних форм із модальностями. Секвенції ми трактуємо як множини специфікованих станами формул. Специ- фікації мають вигляд \|– чи –\|, де  – ім'я стану. Виділяючи \|–-формули та –\|-форму- ли, секвенції позначаємо \|––\|. Специфіковані формули вигляду \| ( ),u vR x    \|–x назвемо T-формулами, а вигляду \| ( ),u vR x   –\|x – F-форму- лами. Прикладами формул  xxRu v ),( назвемо формули вигляду )( ),(, ,  x y xu yv RR . Для секвенції  та стану  задамо секвенцію  = { \|  = \|– чи  = –\|} формул стану . При побудові виведення збагачуємо секвенції збудованими на да- ний момент виведення множинами відно- шень на станах. Збагачені секвенції запи- суємо як  // M, де M – схема моделі світу, тобто збудоване на цей момент відношен- ня досяжності, записане для імен станів. Множини означених, неозначених і нерозподілених імен стану  секвенції  задамо так: val() = {u \| \|–Eu}; unv() = {u \| –\|Eu}; ud() = nm() \ (val()  unv()). Виведення в секвенційних числен- нях має вигляд дерева, вершинами якого є секвенції. Правилами виведення секвен- ційних числень є секвенційні форми, вони безпосередньо виписуються за дуальними властивостями відношення \|. Аксіомами секвенційних числень є замкнені секвенції. Для замкненої секвенції \|––\| має викону- ватись умова  \|= . Секвенційне дерево замкнене, якщо всі його листи – замкнені секвенції. Секвенція  вивідна, якщо існує за- мкнене секвенційне дерево з коренем . Опишемо числення чистих першо- порядкових ЗМЛ та ТмМЛ. Секвенційне числення визначається умовами замкненості секвенції та базовими секвенційними формами. На основі умови С гарантованої на- явності відношення \|= отримуємо загальну умову замкненості секвенції : С) існують  та Rs-Un-еквівалентні  та  такі: \|– та –\|; зокрема, існують  та формула  така: \|– та –\|. Тут Un = {uV \| –\|Eu}. Базові секвенційні форми індукова- ні відповідними властивостями відношен- ня \|= логічного наслідку, а виписуються за дуальними властивостями відношення \|. Основні форми еквівалентних пере- творень: \|RR \| \| ( ), // ( ( )), // v w x y v w x y R M R R M         ; \|RR \| \| ( ), // ( ( )), // v w x y v w x y R M R R M       ; \|R \| \| ( ), // ( ), // v x v x R M R M        ; \|R \| \| ( ), // ( ), // v x v x R M R M        ; \|R \| \| ( ) ( ), // ( ), // v v x x v x R R M R M           ; \|R \| \| ( ) ( ), // ( ), // v v x x v x R R M R M         ; Теоретичні та методологічні основи програмування 32 \|R \| \| ( ), // ( ), // v x v x R M R M          ; \|R \| \| ( ), // ( ), // v x v x R M R M        . У випадку ТмМС замість \|R та \|R маємо: \|R \| \| ( ), // ( ), // v x v x R M R M          ; \|R \| \| ( ), // ( ), // v x v x R M R M        ; \|R \| \| ( ), // ( ), // v x v x R M R M          ; \|R \| \| ( ), // ( ), // v x v x R M R M        . Окрім основних форм еквівалент- них перетворень, використовуємо допомі- жні форми спрощення. Ці форми індуку- ються властивостями RL, RR, RIL, RIR, RUL, RUR, RRL, RRR відношення \|=. Перетво- рення на основі форм спрощення закладені в умови замкненості секвенції: для встано- влення Rs-Un-еквівалентності формул не- обхідна побудова їх Rs-форм, що робиться на основі властивостей R, RI, RU, RR. Форми спрощення такі: \|–R \| \| , // ( ), // M R M         ; –\|R \| \| , // ( ), // M R M       ; \|–RI \| , \| , ( ), // ( ), // v u y v y u R M R M         ; –\|RI \| , \| , ( ), // ( ), // v u y v y u R M R M       ; \|–RU )( , // ),( // ),( , ,\| \|      vy MR MR vy uz v u   ; –\|RU \| , \| , ( ), // , ( ) ( ), // v u y v z u R M y v R M         ; \|–RR \| , \| , ( ), // ( ), // u v u x v y R x M R x M           ; –\|RR \| , \| , ( ), // ( ), // u v u x v y R x M R x M         . Форми декомпозиції формул: \|–  \| \| , // , // M M        ; \|  \| \| , // , // M M        ; \| \| \| \| , // , // , // M M M             ; \| \| \| \| , , // , // M M         . Форми елімінації кванторів: \|– \| \| \| ( ), , // , , // x zR Ez M x M            zfu(, x); \|–R , \| , \| \| ( ), , // , ( ), // u x v z u v R Ez M R x M           zfu(, ( )) u vR x ; –\|v \| \| \| \| \| , ( ), , // , , // x yx R Ey M x Ey M               ; –\|Rv , \| \| , \| \| \| ( ), ( ), , // ( ), , // u u x v v y u v R x R Ey M R x Ey M             . \|– та \|–R назвемо T-формами, –\|v та –\|Rv назвемо F-формами. Форми E-розподілу та первісного означення: Ed \| \|, // , // Ex M Ex M     , xnm(); Ev \| , // // Ez M M     , zfu(). Теоретичні та методологічні основи програмування 33 Форми елімінації модальних опера- торів залежать від властивостей відношен- ня  . Розглянемо традиційні випадки, ко- ли  може бути рефлексивним, транзити- вним чи симетричним. Це дає (див. також [8]) наступні різновиди чистих першопо- рядкових числень ЗМЛ. 1. На  не накладені додаткові умови. Маємо GMQC-числення. Якщо в момент застосування форми до \| маємо стани 1, …, n такі, що 1,...,   n , то до \| застосовуємо \| 1\| \| \| \| , ,..., , // , // n M M               . Якщо ж таких , що   , немає, то до \| застосовуємо форму \|f \| \| \| , , // { } , // M M              ,  – новий стан. Форма, яка застосовується до \|: \| \| \| , // { } , // M M          ,  – новий стан. 2. рефлексивне. Маємо GMQC_R- числення. До \| застосовуємо форму \| для всіх станів 1, …, n таких, що в мо- мент її застосування 1,...,   n . За ре- флективністю маємо   . Форма, яка застосовується до \|: \|R \| \| , // { , } , //            M M ,  – новий стан. 3. симетричне. Маємо GMQC_S- числення. Тоді     зa симетри- чністю Якщо в момент застосування фо- рми до \| маємо 1, …, n такі, що 1,...,   n , то застосовуємо \|. Якщо таких , що   , немає, то застосовуємо \|fS \| \| \| , , // { , } , //                 M M ,  – новий стан. До \| застосовується форма: \|S \| \| , // { , } , //            M M ,  – новий стан. 4.  рефлексивне та симетричне. Отримуємо GMQC_RS-числення. До \| застосовуємо форму \| для всіх станів 1, …, n таких, що в момент її застосуван- ня 1,...,   n . Зауважимо, що завжди маємо   та завжди     . До \| застосовується форма: \|RS \| \| , // { , , } , //              M M ,  – новий стан. 5.  транзитивне. Тоді маємо GMQC_T-числення. Якщо в момент засто- сування форми до \| маємо 1, …, n такі, що 1,...,   n , то застосовуємо: \|T 1 1\| \| \| \| \| \| , ,..., , ,..., , // , // n n M M                     . Через транзитивність  тут необ- хідні 1\| \|,..., n     . Якщо ж таких , що   , немає, то застосовуємо \|fT \| \| \| \| , , , // { } , // M M                ,  – новий стан. До \| застосовуємо форму \|. 6. транзитивне й рефлексивне. Отримуємо GMQC_RT-числення. До \| застосовуємо форму \|T для всіх станів 1, …, n таких, що в момент її застосування 1,...,   n (тут завжди маємо   ). До \| застосовуємо форму \|R. 7. транзитивне й симетричне. Отримуємо GMQC_TS-числення. Якщо в момент застосування форми до \| має- мо 1, …, n такі, що 1,..., n    , то застосовуємо \|T (завжди     ). Якщо немає :   , то застосовуємо Теоретичні та методологічні основи програмування 34 \|fTS \| \| \| \| , , , // { , } , // M M                  ,  – новий стан. До \| застосовуємо форму \|S. 8.  транзитивне, рефлексивне й симетричне. Маємо GMQC_RTS-числення. До \| застосовуємо форму \|T для всіх станів 1, …, n таких, що в мо- мент її застосування 1,..., n    (зав- жди маємо   та     ). До \| застосовуємо \|RS. Подібним чином розглядаємо випа- дки, коли може бути рефлексивним, транзитивним чи симетричним, для ТмМС. Це дає такі різновиди чистих першопоряд- кових числень ТмМЛ: TmMQC, TmMQC_R, TmMQC_S, TmMQC_RS, TmMQC_T, TmMQC_RT, TmMQC_TS, TmMQC_RTS. Форми елімінації для  записуємо аналогічно відповідним формам для . Якщо симетричне, то форми елімінації  та  ідентичні, це фактично форми елімінації . Тому числення TmMQC_S, TmMQC_RS, TmMQC_TS, TmMQC_RTS ці- лком ідентичні численням GMQC_S, GMQC_GRS, GMQC_GTS, GMQC_GRTS. Основну властивість введених сек- венційних форм описує Теорема 4. Нехай M // M // \|\| \|\|     та M // M // M // \|\| \|\|\|\|     – секвенційні форми. Тоді: 1)  \|=    \|= ;  \|=  та  \|=    \|= ; 2)  \|    \| ;  \|    \|  або  \| . Поетапна побудова виведення – секвенційного дерева – для заданої злічен- ної чи скінченної секвенції  в численнях ТМЛ немонотонних предикатів подібна до відповідних побудов у численнях логік немонотонних квазіарних предикатів та числень ТМЛ еквітонних предикатів. По- будову дерева ведемо паралельно із побу- довою схеми моделі світу, ця схема онов- люється при застосуванні форм елімінації модальностей, які додають нові стани. Побудова дерева починається з його кореня – секвенції . Кожне застосування секвенційної форми проводимо до скін- ченної множини доступних на даний мо- мент формул. На початку кожного етапу в усіх незамкнених секвенціях виконуємо крок доступу: до списку доступних додає- мо по одній зі списків \|-формул та \|- формул. На початку побудови доступна пара перших формул списків (єдина \|- формула чи \|-формула, якщо один зі спис- ків порожній). Після виконання кожної форми перевіряємо, чи буде вершина- секвенція замкненою. При появі замкненої секвенції побудова дерева на цьому шляху обривається. Секвенції  це множини специфіко- ваних формул, тому якщо при виконанні форми отримуємо специфіковану форму- лу, яка вже є в секвенції, то формулу- копію до секвенції не заносимо. Якщо всі листи будованого дерева замкнені, то отримано замкнене секвен- ційне дерево, побудова завершена позити- вно. Якщо ні, то у випадку виведення скін- ченної секвенції  додатково перевіряємо незамкнені листи на фінальність. Незамкнена вершина-секвенція  фінальна, якщо до неї незастосовна жодна форма, або кожне застосування форми до  не вводить формул, відмінних від фор- мул секвенцій на шляху від  до . Поява фінальної секвенції означає ситуацію по- вторення незамкненої секвенції на шляху, тому всі вершини цього шляху незамкнені, такий шлях назвемо незамкненим. Опишемо етап виведення для неза- мкненої листа-секвенції. Нехай на початку етапу після додавання до неї пари нових доступних формул отримана секвенція . Активізуємо всі доступні (окрім примітив- них) формули , до кожної активної фор- мули застосовуємо відповідну форму. Піс- ля застосування основної форми утворені нею формули на даному етапі пасивні, до них на цьому етапі основні форми незасто- совні. В процесі застосування основних форм виконуємо спрощення, застосовуючи допоміжні форми типів R, RI, RU, RR. Застосування на етапі основних секвенційних форм проводимо так. Теоретичні та методологічні основи програмування 35 Спочатку для кожного наявного в  стану виконуємо 1-засновкові форми типу RR, R, R, R, , T. При застосу- ванні T-форми кожен раз беремо нове тотально неістотне zV. Множину нових z, використаних для активних T-формул стану  секвенції , позначимо vt. Нехай після застосування цих 1-засновкових форм маємо секвенцію 0. Нехай в 0 є l активних формул, до яких застосовна 2-засновкова \|. Ці застосування ведуть до побудови для 0 піддерева, що має n = 2l листів-наступників секвенції 0, нехай це 1,…, n. Нехай , 0, 1,…, n – множини доступних формул секвенцій на шляхах від  до , 0, 1,…, n. Для цих k та наявних у них станів (фігуру- ють в специфікаціях доступних формул) маємо nm(k) = nm()vt, val(k) = = val()vt, ud(k) = ud(). Позначи- мо val()vt як val, ud() як ud. Нехай для наявного стану  секвен- ції  маємо ud  . Це означає, що в сек- венціях 1,…, n маємо нерозподілені імена стану . За допомогою Еd однаковим чи- ном робимо для кожного 1,…, n всемож- ливі розподіли імен ud на означені та не- означені. Це дає побудову однакових під- дерев висоти \|ud\| з вершинами 1,…, n, що дає \| \| 2 ud m    наступників 1,...,j jm    кожної з секвенцій j{1,…, n} з множи- нами Vnk  ud, дe k{1,…, m}, нових означених імен стану . Будемо вважати Vn1 = . Якщо val = , то для всіх 1,j  дe j{1,…, n} (для них немає означених імен стану ), робимо первісне означення – додаємо \|–Ez для нового тотально неіс- тотно го z, що дає Vn1 = {z}. Тоді в jk  маємо множину означених імен valVnk. Розподіли імен на означені й не- означені робимо для кожного наявного стану  секвенції , для якого ud  . При цьому розподіл для наступного стану з не- розподіленими іменами робимо для кожної секвенції, отриманої в результаті розподі- лу для попереднього такого стану. Після завершення розподілів у кож- ній з так отриманих секвенцій-наступників секвенції 0 застосовуємо F-форму для кожного означеного імені кожного наявно- го стану. Далі в цих секвенціях- наступниках виконуємо форми –\| (форми –\| та –\| для числень ТмМС), після них – форми \| (форми \|– та \|– для чис- лень ТмМС). Побудова секвенційного дерева може завершуватися або не завершувати- ся. Якщо побудова завершена позитив- но, то маємо замкнене дерево. Якщо побудова завершена негатив- но (можливо лише при виведенні скінчен- ної секвенції), то маємо скінченне незамк- нене дерево. Якщо побудова не завершу- ється, то маємо нескінченне незамкнене дерево; таке дерево має хоча б один не- скінченний шлях (лема Кеніга). Отже, як- що побудова завершена негативно або не завершується, то в дереві існує незамкне- ний шлях. Кожна з формул початкової секвенції  зустрінеться на цьому шляху і стане доступною. Теорема 5 (коректності). Якщо сек- венція \|––\| вивідна, то  \|= . Нехай \|––\| вивідна, тоді для неї побудоване замкнене секвенційне дерево. Усі його листи – замкнені секвенції, тому для кожного такого листа \|––\| маємо  \|= . Рух від листів дерева до його коре- ня здійснюється за допомогою секвенцій- них форм. За теоремою 4 при переході від засновків форм до висновків зберігається відношення \|=. Тому для кожної вершини секвенційного дерева \|––\| маємо \|= . Зокрема, для секвенції \|––\| – кореня де- рева – теж маємо  \|= . 5. Теорема про контрмодель. Теорема повноти Для доведення повноти секвенцій- них числень модальних логік використає- мо метод систем модельних множин. Система модельних множин – це пара ({Н \| S}, M), де кожна Н – моде- льна множина стану , M – схема моделей Теоретичні та методологічні основи програмування 36 світу, яка задається R. Для множин Н за- даємо Un = unv(Н) та W = nm(Н) \ Un. Модельна множина стану Н визна- чається умовою коректності та умовами переходу. Умова коректності індукується умовою замкненості секвенції: MС) не існує Rs-Un-еквівалентних формул  та : \|–Н та –\|Н. Умови переходу індуковані вико- нанням відповідних форм. Вони форму- люються однотипно для форм еквівалент- них перетворень та форм спрощення. Наведемо для прикладу умови MRU, MRR та MR. MRU) за умови y() маємо: , \| , ( )y v z uR H     \| ( )v uR H    ; , \| , ( )y v z uR H    \| ( )v uR H   ; MRR) , \| , ( )u x v yR x H       \| ( )u vR x H     ; , \| , ( )u x v yR x H     \| ( )u vR x H    ; MR) \| ( )v xR H     \| ( )v xR H     ; \| ( )v xR H    \| ( )v xR H    . Для форм декомпозиції формул та елімінації кванторів маємо: M) \|–Н  –\|Н; –\|Н  \|–Н; M) \|–Н  \|–Н або \|–Н; –\|Н  –\|Н і –\|Н; M) \|–хН   існує уW: \| ( )   x yR H ; –\|хН   \| ( )  x yR H для всіх уW; MR) \| ( )u vR x H       існує уW : , \| , ( )u x v yR H    ; \| ( )u vR x H      , \| , ( )u x v yR H   для всіх уW ; Для форм елімінації  маємо: M) \|–Н  \|–Н для всіх S таких, що   ; –\|Н  –\|Н для деякого S такого, що   . У випадку ТмМС маємо: M) \|–Н  \|–Н для всіх S таких, що   ; –\|Н  –\|Н для деякого S такого, що   ; M) \|–Н  \|–Н для всіх S таких, що   ; –\|Н  –\|Н для деякого S такого, що   . Теорема 6 (про контрмодель). Не- хай  – незамкнений шлях в секвенційно- му дереві, Н – множина всіх специфіко- ваних формул стану  на шляху , M – об’єднання усіх схем моделей світу секве- нцій шляху , НM = ({Н \| S}, M), S W W   , де кожна W – множина озна- чених предметних імен формул Н. Тоді існують TМС M = (S, R, А, Iт) та VA з asn() = W: \|–Н  () = Т; –\|Н  () = F. Для переходу від нижчої вершини шляху  до вищої використовується одна з базових секвенційних форм. Переходи згідно таких форм відповідають пунктам визначення системи модельних множин. Кожна непримітивна формула на шляху  рано чи пізно буде розкладена згідно від- повідної форми. Всі секвенції шляху  незамкнені, тому для них не виконуються умови замкненості C, звідки для всіх  ви- конується умова коректності MС визна- чення системи модельних множин. Візьмемо деяку множину А таку, що \|А\| = \|W\|, та ін'єктивну VA з asn() = W. Така  є бієкцією W на A, яка розпадається на бієкції  : WA. Кожна А продуб- льовує W. Теоретичні та методологічні основи програмування 37 Задамо значення базових предика- тів на  та на даних вигляду r ( )v x  : \|–EyН  Ey() = Т ; –\|EyН  Ey() = F ; \|– рН  р() = Т ; –\| рН  р() = F ; \| ( ) (r ( )) ( ) ( ) ;v v v x x xR p H p R p T          \| ( ) (r ( )) ( ) ( ) .v v v x x xR p H p R p F         Для інших W d A   значення р(d) задаємо довільним чином, враховуючи (р). Для примітивних формул твер- дження теореми випливає з визначення значень базових предикатів. Далі доводи- мо традиційно: індукцією за складністю формули згідно побудови системи моде- льних множин. Наведемо для прикладу доведення для пп. MRR, M, MR, M. MRR) нехай , \| , ( )u x v yR x H     . Тоді \| ( )u vR x H     за визначенням НM. За припущенням індукції ( ) ( ) ,u vR x T    звідки , , ( ) ( )u x v yR x T    . Нехай , \| , ( )u x v yR x H    . Тоді має- мо \| ( )u vR x H    за визначенням НM. За припущенням індукції маємо ( ) ( ) ,u vR x F    тому , , ( ) ( )u x v yR x F    . M) нехай \|–хН. За визначен- ням НM існує уW таке: \| ( )x yR H    . За припущенням індукції ( ) ( )x yR T   . Звідси (х(у)) = Т. Але (у)А згі- дно уW, тому для а = (у)А маємо (ха) = Т, звідки (х)() = Т. Нехай –\|хН. За визначенням НM тоді \| ( )x yR H   для всіх уW. За припущенням індукції ( ) ( )x yR F   для всіх уW. Звідси (х(у)) = F для всіх уW. Кожне bА має вигляд b = (у) для деякого уW, адже  визначає бієкцію  : WA. Звідси (хb) = F для всіх bА, тому (х)() = F. MR) нехай \| ( )u vR x H     . За ви- значенням НM існує уW: , \| , ( )u x v yR H    . За припущенням індукції , , ( ) ( )u x v yR T   . Звідси отримуємо ( ( ) ( ))u v x y T      . Згідно уW маємо (у)А, тому отримуємо ( ( ) )u v x a T     для а = (у), звідки TxRu v  )()(  . Нехай \| ( )u vR x H    . За визна- ченням НM тоді , \| , ( )u x v yR H   для всіх уW. За припущенням індукції для всіх уW маємо , , ( ) ( )u x v yR F   , звідси для всіх уW ( ( ) ( ))u v x y F      Кожне bА має вигляд b = (у) для деяко- го уW, адже  задає бієкцію  : WA. Звідси ( ( ) )u v x a F     для всіх bА, тому ( ) ( )u vR x F    . M) нехай \|–Н. За визначен- ням НM маємо \|–Н для всіх S таких, що   . За припущенням індукції () = Т для всіх  таких, що   . Звід- си за визначенням  отримуємо ()() = T. Нехай –\|Н. За визначенням НM тоді –\|Н для деякого S:   . За припущенням індукції () = F, тому ()() = F за визначенням . Із теореми про контрмодель отри- муємо теорему повноти. Теорема 7. Нехай  \|= . Тоді сек- венція \|––\| вивідна. Припустимо супротивне:  \|= , тобто  M\|=  для кожної узгодженої ТМС M, проте секвенція  = \|––\| невивідна. Тоді в дереві для  існує незамкнений шлях. За теоремою 6 НM = ({Н \| S}, M) – Теоретичні та методологічні основи програмування 38 система модельних множин, тому існують ТМС M = (S, R, А, Jт) та VA такі: \|–Н  () = Т та –\|Н  () = F. Зокрема, це правильно для формул секвенції \|––\|. Тому для всіх  має- мо () = Т та для всіх Ψ маємо Ψ() = F. Це заперечує  M\|= , тому  \| . Отримали суперечність. Отже, припущення про невивідність \|––\| невір- не, що й доводить теорему. Висновки Досліджено нові програмно-орієн- товані логічні формалізми модального ти- пу – чисті першопорядкові композиційно- номінативні модальні логіки часткових предикатів без обмеження монотонності. Описано семантичні моделі та мови таких логік, розглянуто взаємодію модальних композицій із реномінаціями та кванто- рами, введено відношення наслідку для формул в даному стані. Наведено власти- вості відношення логічного наслідку для множин специфікованих станами формул, описано властивості елімінації модально- стей для різних відношень досяжності. Для загальних транзиційних та темпора- льних модальних логік немонотонних предикатів запропоновано числення сек- венційного типу. Описано різновиди та- ких числень для різних відношень досяж- ності, для цих числень наведено базові секвенційні форми та умови замкненості секвенцій. Детально описано поетапну процедуру побудови виведення (секвен- ційного дерева) в цих численнях, для них доведено теорему коректності та теорему про існування контрмоделі для незамкне- ного шляху в секвенційному дереві. На основі теореми про існування контрмоде- лі доведено теорему повноти. 1. Нікітченко М.С., Шкільняк С.С. Приклад- на логіка. К.: ВПЦ Київський університет, 2013. 278 с. 2. Cocchiarella N.B., Freund M.A. Modal logic. Oxford University Press, 2008. 267 p. 3. Нікітченко М.С., Шкільняк О.С., Шкільняк С.С. Чисті першопорядкові логіки квазіа- рних предикатів. Проблеми програмування. 2016. № 2–3. C. 73–86. 4. Шкільняк О.С. Семантичні властивості композиційно-номінативних модальних логік. Проблеми програмування. 2009. № 4. C. 11–23. 5. Шкільняк О.С. Композиційно-номінативні модальні логіки функціонально-еквацій- ного рівня. Проблеми програмування. 2010. № 2–3. C. 42–47. 6. Шкільняк О.С. Транзиційні композиційно- номінативні модальні логіки та їх числен- ня. Наук. записки НаУКМА. Серія: Комп’ютерні науки. 2013. Т. 151. C. 48–54. 7. Шкільняк О.С. Транзиційні модальні логі- ки немонотонних квазіарних предикатів. Компьютерная математика. 2014. В. 2. C. 99–110. 8. Шкільняк О.С. Mодальні логіки немоно- тонних часткових предикатів. Вісник Київ- ського ун-ту. Серія: фіз.-мат. науки. 2015. Вип. 3. C. 141–147. 9. Shkilniak O. Modal Logics of Partial Predicates without Monotonicity Restriction. Workshop on Foundations of Informatics: Proceedings FOI-2015. – Chisinau, Moldova. P. 198–211. References 1. NIKITCHENKO M. and SHKILNIAK S. (2013). Applied logic. Кyiv: VPC Кyivskyi Universytet (in ukr). 2. COCCHIARELLA N. and FREUND M. (2008). Modal logic. Oxford University Press. 3. NIKITCHENKO M., SHKILNIAK O. and SHKILNIAK, S. (2016). Pure first-order logics of quasiary predicates. In Problems in Progamming. N 2–3, P. 73–86 (in ukr). 4. SHKILNIAK O. (2009). Semantic properties of composition nominative modal logics. In Problems in Progamming. N 4, P. 11–23 (in ukr). 5. SHKILNIAK, O. (2010). Composition nominative modal logics of functional- equational level. Problems in Progamming. N 2–3, P. 42–47 (in ukr). 6. SHKILNIAK O. (2013). Transitional composition-nominative modal logics and their calculi. In Scientific Notes of NaUKMA. Series: Computer sciences. 151, P. 99–110 (in ukr). Теоретичні та методологічні основи програмування 39 7. SHKILNIAK O. (2014). Transitional modal logics of non-monotone quasiary predicates. In Computer mathematics. 2, P. 99–110 (in ukr). 8. SHKILNIAK O. (2015). Modal logics of non- monotone partial predicates. In Bulletin of Taras Shevchenko National University of Kyiv. Series: Physics & Mathematics. 3, P. 141–147 (in ukr). 9. SHKILNIAK O. (2015). Modal Logics of Partial Predicates without Monotonicity Restriction. In Workshop on Foundations of Informatics: Proceedings FOI-2015. Chisinau, Moldova. P. 198–211. Одержано 20.04.2017 Про авторів: Шкільняк Оксана Степанівна, кандидат фізико-математичних наук, доцент, доцент кафедри інформаційних систем. Кількість наукових публікацій в українських виданнях – 84, у тому числі у фахових виданнях – 32. Кількість наукових публікацій в зарубіжних виданнях – 9. http://orcid.org/0000-0003-4139-2525. Касьянюк Веда Станіславівна, кандидат фізико-математичних наук, завідувач науково-дослідного сектору теоретичної кібернетики. Кількість наукових публікацій в українських виданнях – 129, у тому числі у фахових виданнях – 51. Кількість наукових публікацій в зарубіжних виданнях – 7. http://orcid.org/0000-0003-3268- 303Х. Малютенко Людмила Миколаївна, провідний інженер науково-дослідного сектору теоретичної кібернетики. Кількість наукових публікацій в українських виданнях – 15, у тому числі у фахових виданнях – 7. Кількість наукових публікацій в зарубіжних виданнях – 1. http://orcid.org/0000-0002-3513-5533. Місце роботи авторів: Київський національний університет імені Тараса Шевченка, 01601, Київ, вул. Володимирська, 60. Тел.: (044) 259 0511, (050) 356 4875. E-mail: me.oksana@gmail.com mailto:me.oksana@gmail.com

Composition nominative modal logics of partial non-monotone predicates and their calculi

Репозитарії

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