Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics

The aim of the work is to study new classes of program-oriented logical formalisms of the modal type – pure first-order modal logics of partial quasiary predicates without monotonicity condition and enriched with equality predicates. Modal logics can be used to describe and model various subject are...

Повний опис

Збережено в:

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

Репозитарії

Problems in programming

id	pp_isofts_kiev_ua-article-615
record_format	ojs
resource_txt_mv	ppisoftskievua/c4/eb567ca6e7a85edf0c1edc5e370c1dc4.pdf
spelling	pp_isofts_kiev_ua-article-6152025-02-14T10:28:12Z Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics Модальні логіки часткових квазіарних предикатів з рівністю та cеквенційні числення цих логік Shkilniak, О.S. Shkilniak, S.S. modal logic; predicate; logical consequence; sequent calculus UDC 510.64 модальна логіка; предикат; логічний наслідок; секвенційне числення УДК 510.64 The aim of the work is to study new classes of program-oriented logical formalisms of the modal type – pure first-order modal logics of partial quasiary predicates without monotonicity condition and enriched with equality predicates. Modal logics can be used to describe and model various subject areas, artificial intelligence systems, information and software systems. The limitations of the classical predicate logic on which traditional modal logics are based determine the relevance of the problem of introducing new program-oriented logical formalisms. Such are composition-nominative modal logics, which synthesize facilities of traditional modal logics and logics of partial quasiary predicates. One of their important classes are transitional modal logics (TML), they reflect the aspect of change and evolution of subject areas. We denote pure first-order TML by TMLQ. In this paper two types of TMLQ with equality are considered: TMLQ (with strong equality predicates xy), and TMLQ= (with weak equality predicates =xy). For quantifier elimination in logics of non-monotonic predicates special predicates which indicate whether a component with a corresponding name has a value in the input data are required. The use of these predicates is a characteristic feature of both TMLQ and TMLQ=. Total indicator predicates determine the presence or absence of a component with a certain name, while partial indicator predicates signalize only the presence of such a component. Thus, total indicator predicates are introduced as special parametric 0-ary compositions Ez in TMLQ, and partial indicator predicates are represented in TMLQ= as predicates =xx. Another feature of TMLQ and TMLQ= is the use of the extended renomination compositions. In this paper we describe semantic models and languages of TMLQ and TMLQ=. Particular attention is paid to the properties related to equality predicates, substitution of equals in TMLQ and TMLQ= is described. A number of logical consequence relations for these logics are defined on sets of formulas specified with states. On this semantic basis, the corresponding sequent type calculi are proposed for the investigated logics.Prombles in programming 2024; 2-3: 19-27 Робота присвячена дослідженню нових класів програмно-орієнтованих логічних формалізмів модального типу – чистих першопорядкових модальних логік часткових квазіарних предикатів зі знятою умовою монотонності та збагачених предикатами рівності. Апарат модальних логік використовується для опису й моделювання різноманітних предметних областей, cистем штучного інтелекту, інформаційних та програмних систем. Обмеження класичної логіки предикатів, на якій базуються традиційні модальні логіки, зумовлюють актуальність проблеми побудови нових, програмно-орієнтованих логічних формалізмів. Такими є композиційно-номінативні модальні логіки, які синтезують можливості традиційних модальних логік і логік часткових квазіарних предикатів. Важливим їх класом є транзиційні модальні логіки (TMЛ), які відбивають аспект зміни й розвитку предметних областей. Чисті першопорядкові ТМЛ названо TMLQ. В роботі запропоновано два різновиди TMLQ з рівністю: з предикатами строгої рівності xy, їх названо TMLQ, та слабкої рівності =xy, їх названо TMLQ=. Для елімінації кванторів в логіках немонотонних предикатів потрібні спеціальні предикати-індикатори наявності у вхідних даних компоненти з відповідним предметним іменем. Використання цих предикатів є характерною особливістю TMLQ та TMLQ=. Тотальні предикати-індикатори визначають наявність чи відсутність компоненти з певним іменем, а часткові предикати-індикатори визначають лише наявність такої компоненти. Тотальні предикати-індикатори Ez фігурують в TMLQ як спеціальні 0- арні композиції, часткові предикати-індикатори вже присутні в TMLQ= як предикати =xx. Ще одна особливість TMLQ та TMLQ= – використання композицій розширеної реномінації. В роботі описано семантичні моделі та мови TMLQ та TMLQ=. Увагу акцентовано на властивостях, пов’язаних з предикатами рівності, описано особливості заміни рівних в TMLQ та в TMLQ=. Для цих логік визначено низку відношень логічного наслідку для множин специфікованих станами формул. На цій семантичній основі для досліджених логік запропоновано відповідні числення секвенційного типу. Prombles in programming 2024; 2-3: 19-27 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2024-12-17 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/615 10.15407/pp2024.02-03.019 PROBLEMS IN PROGRAMMING; No 2-3 (2024); 19-27 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2024); 19-27 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2024); 19-27 1727-4907 10.15407/pp2024.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/615/667 Copyright (c) 2024 PROBLEMS IN PROGRAMMING
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2025-02-14T10:28:12Z
collection	OJS
language	Ukrainian
topic	modal logic predicate logical consequence sequent calculus UDC 510.64
spellingShingle	modal logic predicate logical consequence sequent calculus UDC 510.64 Shkilniak, О.S. Shkilniak, S.S. Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics
topic_facet	modal logic predicate logical consequence sequent calculus UDC 510.64 модальна логіка предикат логічний наслідок секвенційне числення УДК 510.64
format	Article
author	Shkilniak, О.S. Shkilniak, S.S.
author_facet	Shkilniak, О.S. Shkilniak, S.S.
author_sort	Shkilniak, О.S.
title	Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics
title_short	Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics
title_full	Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics
title_fullStr	Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics
title_full_unstemmed	Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics
title_sort	modal logics of partial quasiary pradicates with equality and sequent calculi of this logics
title_alt	Модальні логіки часткових квазіарних предикатів з рівністю та cеквенційні числення цих логік
description	The aim of the work is to study new classes of program-oriented logical formalisms of the modal type – pure first-order modal logics of partial quasiary predicates without monotonicity condition and enriched with equality predicates. Modal logics can be used to describe and model various subject areas, artificial intelligence systems, information and software systems. The limitations of the classical predicate logic on which traditional modal logics are based determine the relevance of the problem of introducing new program-oriented logical formalisms. Such are composition-nominative modal logics, which synthesize facilities of traditional modal logics and logics of partial quasiary predicates. One of their important classes are transitional modal logics (TML), they reflect the aspect of change and evolution of subject areas. We denote pure first-order TML by TMLQ. In this paper two types of TMLQ with equality are considered: TMLQ (with strong equality predicates xy), and TMLQ= (with weak equality predicates =xy). For quantifier elimination in logics of non-monotonic predicates special predicates which indicate whether a component with a corresponding name has a value in the input data are required. The use of these predicates is a characteristic feature of both TMLQ and TMLQ=. Total indicator predicates determine the presence or absence of a component with a certain name, while partial indicator predicates signalize only the presence of such a component. Thus, total indicator predicates are introduced as special parametric 0-ary compositions Ez in TMLQ, and partial indicator predicates are represented in TMLQ= as predicates =xx. Another feature of TMLQ and TMLQ= is the use of the extended renomination compositions. In this paper we describe semantic models and languages of TMLQ and TMLQ=. Particular attention is paid to the properties related to equality predicates, substitution of equals in TMLQ and TMLQ= is described. A number of logical consequence relations for these logics are defined on sets of formulas specified with states. On this semantic basis, the corresponding sequent type calculi are proposed for the investigated logics.Prombles in programming 2024; 2-3: 19-27
publisher	PROBLEMS IN PROGRAMMING
publishDate	2024
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/615
work_keys_str_mv	AT shkilniakos modallogicsofpartialquasiarypradicateswithequalityandsequentcalculiofthislogics AT shkilniakss modallogicsofpartialquasiarypradicateswithequalityandsequentcalculiofthislogics AT shkilniakos modalʹnílogíkičastkovihkvazíarnihpredikatívzrívnístûtacekvencíjníčislennâcihlogík AT shkilniakss modalʹnílogíkičastkovihkvazíarnihpredikatívzrívnístûtacekvencíjníčislennâcihlogík
first_indexed	2025-07-17T09:41:58Z
last_indexed	2025-07-17T09:41:58Z
_version_	1850412917980135424
fulltext	Теоретичні і методологічні основи програмування 19 УДК 510.64 http://doi.org/10.15407/pp2024.02-03.019 О.С. Шкільняк, С.С. Шкільняк МОДАЛЬНІ ЛОГІКИ ЧАСТКОВИХ КВАЗІАРНИХ ПРЕДИКАТІВ З РІВНІСТЮ ТА CЕКВЕНЦІЙНІ ЧИСЛЕННЯ ЦИХ ЛОГІК Робота присвячена дослідженню нових класів програмно-орієнтованих логічних формалізмів мода- льного типу – чистих першопорядкових модальних логік часткових квазіарних предикатів зі знятою умовою монотонності та збагачених предикатами рівності. Апарат модальних логік використовуєть- ся для опису й моделювання різноманітних предметних областей, cистем штучного інтелекту, інфор- маційних та програмних систем. Обмеження класичної логіки предикатів, на якій базуються тради- ційні модальні логіки, зумовлюють актуальність проблеми побудови нових, програмно-орієнтованих логічних формалізмів. Такими є композиційно-номінативні модальні логіки, які синтезують можли- вості традиційних модальних логік і логік часткових квазіарних предикатів. Важливим їх класом є транзиційні модальні логіки (TMЛ), які відбивають аспект зміни й розвитку предметних областей. Чисті першопорядкові ТМЛ названо TMLQ. В роботі запропоновано два різновиди TMLQ з рівністю: з предикатами строгої рівності xy, їх названо TMLQ, та слабкої рівності =xy, їх названо TMLQ=. Для елімінації кванторів в логіках немонотонних предикатів потрібні спеціальні предикати-індикатори наявності у вхідних даних компоненти з відповідним предметним іменем. Використання цих преди- катів є характерною особливістю TMLQ та TMLQ=. Тотальні предикати-індикатори визначають наяв- ність чи відсутність компоненти з певним іменем, а часткові предикати-індикатори визначають лише наявність такої компоненти. Тотальні предикати-індикатори Ez фігурують в TMLQ як спеціальні 0- арні композиції, часткові предикати-індикатори вже присутні в TMLQ= як предикати =xx. Ще одна особливість TMLQ та TMLQ= – використання композицій розширеної реномінації. В роботі описано семантичні моделі та мови TMLQ та TMLQ=. Увагу акцентовано на властивостях, пов’язаних з пре- дикатами рівності, описано особливості заміни рівних в TMLQ та в TMLQ=. Для цих логік визначено низку відношень логічного наслідку для множин специфікованих станами формул. На цій семантич- ній основі для досліджених логік запропоновано відповідні числення секвенційного типу. Ключові слова: модальна логіка, предикат, логічний наслідок, секвенційне числення О.S. Shkilniak, S.S. Shkilniak MODAL LOGICS OF PARTIAL QUASIARY PREDICATES WITH EQUALITY AND SEQUENT CALCULI OF THESE LOGICS The aim of the work is to study new classes of program-oriented logical formalisms of the modal type – pure first-order modal logics of partial quasiary predicates without monotonicity condition and enriched with equali- ty predicates. Modal logics can be used to describe and model various subject areas, artificial intelligence sys- tems, information and software systems. The limitations of the classical predicate logic on which traditional modal logics are based determine the relevance of the problem of introducing new program-oriented logical formalisms. Such are composition-nominative modal logics, which synthesize facilities of traditional modal logics and logics of partial quasiary predicates. One of their important classes are transitional modal logics (TML), they reflect the aspect of change and evolution of subject areas. We denote pure first-order TML by TMLQ. In this paper two types of TMLQ with equality are considered: TMLQ (with strong equality predicates xy), and TMLQ= (with weak equality predicates =xy). For quantifier elimination in logics of non-monotonic predicates special predicates which indicate whether a component with a corresponding name has a value in the input data are required. The use of these predicates is a characteristic feature of both TMLQ and TMLQ=. Total indicator predicates determine the presence or absence of a component with a certain name, while partial indicator predicates signalize only the presence of such a component. Thus, total indicator predicates are intro- duced as special parametric 0-ary compositions Ez in TMLQ, and partial indicator predicates are represented in TMLQ= as predicates =xx. Another feature of TMLQ and TMLQ= is the use of the extended renomination com- positions. In this paper we describe semantic models and languages of TMLQ and TMLQ=. Particular attention is paid to the properties related to equality predicates, substitution of equals in TMLQ and TMLQ= is described. A number of logical consequence relations for these logics are defined on sets of formulas specified with states. On this semantic basis, the corresponding sequent type calculi are proposed for the investigated logics. Key words: modal logic, predicate, logical consequence, sequent calculus © О.С.Шкільняк, С.С.Шкільняк, 2024 ISSN 1727-4907. Проблеми програмування. 2024. №2-3 Теоретичні і методологічні основи програмування 20 Вступ Апарат модальних логік успішно використовується для опису й моделю- вання різноманітних предметних облас- тей, cистем штучного інтелекту, інформа- ційних та програмних систем (див., напр., [1, 2]). Темпоральні логіки застосовують- ся для моделювання динамічних систем, специфікації та верифікації програм [2–4], на базі цих логік розроблено низку систем і мов специфікацій. Епістемічні логіки з великим успіхом використовуються для опису систем штучного інтелекту, інфор- маційних та експертних систем. Водночас обмеження класичної логіки предикатів, яка лежить в основі традиційних модаль- них логік, роблять вельми актуальною за- дачу побудови нових, програмно- орієнтованих логічних формалізмів мода- льного типу. Такими є композиційно- номінативні модальні логіки (КНМЛ), які поєднують можливості традиційних мо- дальних логік [3] і композиційно- номінативних логік часткових квазіарних предикатів [5–8]. Найважливішим класом КНМЛ є транзиційні модальні логіки (TMЛ), які відбивають аспект зміни й ро- звитку предметних областей. Такі логіки вивчались, зокрема, в [9, 10]. Традиційні модальні логіки природним чином розг- лядаються в межах TMЛ. Метою пропонованої роботи є дос- лідження нових класів програмно- орієнтованих модальних логік – чистих першопорядкових TMЛ часткових квазіа- рних предикатів зі знятою умовою моно- тонності (еквітонності) та збагачені пре- дикатами рівності. Виділено [8] два різно- види таких предикатів: слабкої рівності =ху та строгої рівності ху. Чисті першо- порядкові TMЛ зі знятою умовою моно- тонності назвемо TMLQ. TMLQ з предика- тами строгої рівності назвемо TMLQ, а TMLQ з предикатами слабкої рівності на- звемо TMLQ=. TMLQ без предикатів рівно- сті досліджено в [9, 10]. TMLQ та TMLQ= вивчаються в цій роботі. Для елімінації кванторів в логіках немонотонних предикатів потрібні спеціа- льні предикати-індикатори наявності у вхідних даних компоненти з відповідним предметним іменем. Використання преди- катів-індикаторів є характерною особливі- стю TMLQ. Тотальні предикати-індикатори визначають наявність чи відсутність ком- поненти з певним іменем, а часткові пре- дикати-індикатори визначають лише наяв- ність компоненти з певним іменем. Тота- льні предикати-індикатори Ez фігурують, зокрема, в [5–7, 9]. Предикати Ez можна виразити як y xy, проте доцільніше зада- ти їх явно як спеціальні 0-арні композиції, як зроблено в TMLQ Водночас часткові предикати-індикатори вже присутні в TMLQ=, такими є предикати =xx. В роботі описано семантичні моделі та мови TMLQ, описано особливості заміни рівних в TMLQ та TMLQ=, визначено низ- ку відношень логічного наслідку для мно- жин специфікованих станами формул та наведено їх властивості, На цій семантич- ній основі для TMLQ з рівністю запропо- новано низку числень секвенційного типу. Поняття, які в цій роботі не визна- чаються, тлумачитимо в сенсі [5–9]. 1. Транзиційні модальні системи Центральним для КНМЛ є поняття композиційно-номінативної модальної си- стеми (КНMС). Такі системи є моделями світів розгляду модальних логік. КНMС – це об'єкт вигляду M = (Cms, Ds, Iт). Тут: – Cms – композиційна модальна си- стема, задає семантичні аспекти світу; – Ds – дескриптивна система, вона визначає стандартні дескрипції; зазвичай це множина Fт формул мови КНМЛ; – Dns – денотаційна система, вона визначає значення стандартних дескрипцій на семантичних моделях; зазвичай для цього використовується відображення Iт інтерпретації формул на станах світу. Композиційна модальна система – це об’єкт вигляду Cms = (St, R, Pr, C), де: – St – множина станів світу; – R – множина відношень на St ви- гляду R  St  Stn; – Pr – множина предикатів на St; – C – множина композицій на Pr. КНMС далі будемо трактувати як об'єкти вигляду M = ((St, R, Pr, C), Fт, Iт). Теоретичні і методологічні основи програмування 21 Для чистих першопорядкових КНMС множину St конкретизуємо як множину алгебраїчних систем (структур) вигляду  = (A, Pr), де A – множина ба- зових даних стану , Pr – множина квазі- арних предикатів VA→{T, F}, названих предикатами стану . Предикати вигляду VA→{T, F}, де α α , S A A  = назвемо глобальними. Важливим класом КНMЛ є транзи- ційні модальні логіки (TMЛ), вони відби- вають аспект зміни й розвитку предметних областей, описуючи переходи від одного стану світу до іншого. В основі TMЛ ле- жить поняття транзиційної модальної сис- теми (TMС), такі системи є найважливі- шим класом КНMC. Чисті першопорядкові TMС назвемо TMSQ. TMС – це КНМC, у яких множина R складається з відношень вигляду R  St  St. Ці відношення трактуємо як ві- дношення переходу на станах. Окремими випадками TMС є зага- льні транзиційні, темпоральні, мультимо- дальні системи (див. [9, 10]). TMС, в яких R складається з єдино- го бінарного відношення , а базовою мо- дальною композицією є  ("необхідно"), названо загальними (GMS). TMС, в яких R складається з єдино- го бінарного відношення , а базовими модальними композиціями є  ("завжди буде") і  ("завжди було"), названо тем- поральними (TmMS). TMС із множиною відношень R = { i \| iI} і базовими модальними ком- позиціями Mi, iI, в яких кожному i R зіставлено відповідну композицію Mi, на- звано мультимодальними (MМS). В MМS дія кожної Mi аналогічна дії , але тільки щодо свого відношення ,i iI. Для GMS традиційно задають похі- дну композицію  ("можливо"): Р озна- чає Р. Для TmMS задають похідні композиції  ("колись буде") та  ("ко- лись було"): Р означає Р, а Р означає Р. Базовими загальнологічними ком- позиціями для TMSQ вважаємо логічні зв’язки  та , композиції реномінації , ,R ⊥ v u x та квантифікації x. Для TMSQ з рів- ністю до них додаємо спеціальні 0-арні композиції – предикати рівності. TMSQ з предикатами строгої рівності xy назвемо TMSQ, а TMSQ з предикатами слабкої строгої рівності =xy назвемо TMSQ=. Нагадаємо, що V-A-квазіарним пре- дикатом називаємо [5] часткову функцію вигляду Q : VA→{T, F}. Тут VA – множина всіх V-A-іменних множин {T, F} – множи- на істиннісних значень. V і A трактуємо як множини предметних імен (змінних) і пре- дметних значень. V-A-іменну множину (V-A-ІМ) ви- значають [5] як однозначну функцію ви- гляду VA. Подаємо V-A-ІМ у вигляді [ ] ,i i i Iv a де vіV, aіA, vі  vj при і  j. Для V-A-ІМ вводимо операції \|\|–Z, де Z  V, накладення , реномінації та ро- зширеної реномінації (див. [5, 7, 8]). Кожний V-A-квазіарний предикат Q задаємо двома множинами: область істин- ності T(Q) = {d \| Q(d) = T} та область хиб- ності F(Q) = {d \| Q(d) = F}. Предикат Q однозначний, або P-пре- дикат, якщо T(Q)F(Q) =; Q неспростовний, якщо F(Q) = ; Q виконуваний, якщо T(Q)  . Далі розглядаємо саме однозначні V-A-квазіарні предикати. В класі P-предикатів маємо 3 конс- тантних: – Q тотожно істинний (позн. T), якщо F(Q) =  та T(Q) = VА; – Q тотожно хибний (позн F), як- що T(Q) =  та F(Q) = VА; – Q тотально невизначений (позн. ⊥, якщо T(Q) = F(Q) = . P-предикат Q еквітонний, якщо (Q(d) та d  d')Q(d')= Q(d). хV неістотне для предиката Q, якщо d1 \|\|–х = d2 \|\|–хQ(d1) = Q(d2). Визначення базових загальнологіч- них композицій , , x, , ,R ⊥ v u x квазіарних предикатів наведено в [7] Предикати рівності трактуємо як спеціальні 0-арні композиції, беручи до уваги їх загальнологічний статус. Виділено Теоретичні і методологічні основи програмування 22 [6] два різновиди цих предикатів: слабкої (з точністю до визначеності) рівності ={x,y} та строгої (точної) рівності {x,y}. Задаємо ={x,y} та {x,y} так: T(={x,y}) = {d \| d(x), d(y) та d(x) = d(y)}, F(={x,y}) = {d \| d(x), d(y) та d(x)  d(y)}; T({x,y}) = {d \| d(x), d(y) та d(x) = d(y)} {d \| d(x) та d(y)}, F({x,y}) = {d \| d(x), d(y), d(x)  d(y)} {d \| d(x), d(y) або d(x), d(y)}. Окремим випадком ={x,y} та {x,y}, якщо x та y збігаються, є ={x} та {x}. Предикати ={x,y}, ={x} та {x,y}, {x} більш звично позначаємо =xy, =xx та xy,  xx. Отже, =xy та =yx – це один і той же пре- дикат, xy та yx – теж один і той же пре- дикат. Предикати xy та xx тотальні не- монотонні; =xy та =xx часткові еквітонні. Спеціальні 0-арні композиції – пре- дикати-індикатори – визначають наявність у вхідних даних компоненти зі вказаним іменем. Тотальні предикати-індикатори встановлюють наявність чи відсутність такої компоненти, часткові предикати- індикатори встановлюють лише наявність цієї компоненти. Тотальні предикати-індикатори Ez немонотонні, їх задаємо (див. [7]) так: T(Ez) = {d \| d(z)}; F(Ez) = {d \| d(z)}. Частковими предикатами-індикато- рами в TMSQ= є еквітонні предикати =zz. Справді, маємо T(=zz) = {d \| d(z)} = T(Ez) та F(=zz) = {d \| d(z) та d(z)  d(z)} = . Таким чином, маємо такі різновиди TMSQ з рівністю: GMSQ, TmMS Q, MМS Q для TMSQ та GMSQ=, TmMS Q=, MМS Q= для TMSQ=. Опишемо мову GMSQ. Алфавіт мови: множина V предметних імен (змін- них); множина Ps предикатних символiв; множина , ,{ , , , , , }v u x xyR x Ex⊥    символів базових загальнологічних композицій; множина Ms = {} символів базових мо- дальних композицій. Множина Fr формул мови визначається так: Fa) Ps  Fr; F) {Ex \| xV}  Fr та {ху \| x, уV}  Fr; Fp) ,FrFr та Fr; FR) Fr , , Φ ;v u xR Fr⊥  F) Fr xFr; F) Fr  Fr. Формули вигляду рPs, Ex, ху на- звемо атомарними. Множини гарантовано неістотних для формул імен задаємо функцією  : Fr→2V (див. [7, 9]). Тип GMSQ визначається розшире- ною сигнатурою  = (Ps, ) та властивос- тями відношення . Задамо відображення інтерпретації Im формул на станах світу. Спочатку зада- ємо Im : Рs  St→Pr, водночас має бути Iт(p, )  Pr (базові предикати є преди- катами станів). Символи композицій (зок- рема, символи Ex та  xy) інтерпретуються як відповідні композиції (зокрема, відпові- дні предикати-індикатори та предикати рі- вності). Продовжимо таке Im до відобра- ження Fт  St→Pr наступним чином: Ip) Iт(, ) = (Iт(,)); Iт(, ) = (Iт(, ), Iт(, )); IR) , , , ,( (Φ),α) R ( (Φ,α));⊥ ⊥=v u v u x xIm R Im I) Iт(x, )(d) = , якщо існує : ( , )( ) , , якщо ( , )( ) для всіх , невизначене в усіх інших випадках. T a A Im d x a T F Im d x a F a A       ==    =   I) Iт(, )(d) = , якщо ( , )( ) для всіх : , , якщо існує : та ( , )( ) , невизначене в усіх інших випадках. T Im d T S F S Im d F   =   =      =  Якщо для S не існує :   , то Iт(, )(d) для кожного dVA. Предикати, які є значеннями немо- далізованих формул (при їх побудові не використовуються символи MS), належать до предикатів станів. Предикати, які є значеннями модалі- зованих формул, належать до глобальних. TMS записуємо як M = (St, R, A, Im). Наступні визначення даються одна- ково для всіх описаних різновидів TMSQ. Предикат Iт(, ) – значення фор- мули  у стані  – позначаємо . Теоретичні і методологічні основи програмування 23 Формула  неспростовна в стані  (позначаємо  \|=), якщо  – неспрос- товний предикат. Формула  неспростовна в TMS M (позн.M \|=), якщо для всіх St преди- кат  є неспростовним. Нехай ℳ – клас TMS певного типу. Формула  ℳ-неспростовна (позн. ℳ \|=), якщо M \|= для всіх TMS Mℳ. Залежно від умов, накладених на відношення , можна визначати різні кла- си GMS Q. Традиційними є випадки, коли може бути рефлексивним, симетричним чи транзитивним. Тоді в назві GMSQ пи- шемо символ R, T чи S. Отримуємо такі класи: R-GMSQ, T-GMSQ, S-GMSQ, RT- GMSQ, RS-GMSQ, TS-GMSQ, RTS- GMSQ. Мова GMSQ= визначається аналогі- чно мові GMSQ з такими відмінностями. Множина символів базових загальнологіч- них композицій – це , ,{ , , , , }.v u x xyR x⊥   = У визначенні множини формул замість п. F маємо {=ху \| x, уV}  Fr. Відповідно ви- значається відображення інтерпретації. Опишемо мову TmMSQ. Алфавіт мови – це алфавіт мови GMSQ із тією від- мінністю, що множина символів базових модальних композицій Ms = {, }. Множину Fт формул мови задаємо за пп. Fa, F, Fp, FR, F для мови GMSQ, а замість п. F маємо: F) FrFr та Fr. Визначаючи відображення Iт за- мість I записуємо I (див. [9, 10]). Мова TmMSQ= визначається подіб- но до мови TmMSQ з такими відміннос- тями, які має мова GMSQ= щодо мови GMSQ. Залежно від умов, накладених на , визначаємо різні класи GMSQ=, TmMSQ, TmMSQ= так, як це зроблено для GMSQ. У такий спосіб визначаємо і мови MMSQ та MMSQ=. Залежно від того, як задається зна- чення (d) за умови dVA, виділено [10]) два різновиди TMS: із сильною умо- вою визначеності на станах та із загальною умовою визначеності на станах. Сильна умова є занадто обмежувальною, вона та- кож порушує [10] еквітонність предикатів при дії модальної композиції. Загальна умова набагато природніша, вона задаєть- ся так: (d) =(d ) для всіх dVA та St Тут d – це позначення для ІМ [ v a d \| aA ]. За умови dVA маємо (d) =(d ). Це означає,що предикати стану  "відчувають" лише компоненти v a з базовими даними aA. Взаємодія модальних композицій із реномінаціями та кванторами досліджена в [10]. Стисло опишемо її для GMSQ. Теорема 1. Для всіх Fr, dVA маємо , , , ,R ( Φ)( ) (R (Φ))( )v u v u x xd d⊥ ⊥= . Отже, символи Ms можна проноси- ти через символи реномінації. Теорема 2. Формули вигляду x→x, x→x, x→x, x→x спросто- вуються в GMSQ, водночас вони неспрос- товні в GMSQ еквітонних предикатів; 2) формули вигляду x→ x, x→x, x→x, x→x спрос- товні в GMSQ еквітонних предикатів. Теореми 1 та 2 відповідним чином формулюються для TmMSQ та MMSQ. Розглянемо специфічні властивості GMSQ, пов’язані з предикатами рівності. В TmMSQ і MMSQ ці властивості формулю- ються аналогічно. Твердження 1. 1) для кожної GMSQ M маємо M \|=  хх тa M \|=хх; 2) для кожної GMSQ= M маємо M \|= =хх тa M \|==хх. Справді, F(хх) =  та F(=хх) = . Теорема 3. Формули =ху→=ху тa =ху→=ху неспростовні в GMSQ=. Зокрема, =хх→=хх тa =хх→=хх неспростовні в GMSQ=. Водночас Теорема 4. 1) Формули ху→ху тaху→ху спростовні в GMSQ; 2) формули Ex→Ex тa Ex→Ex спростовні в GMSQ. Теоретичні і методологічні основи програмування 24 Теореми 3 та 4 засвідчують істотні відмінності GMSQ та GMSQ=. Ще одним підтвердженням цього є Теорема 5. 1) Формула =ху &=хz→=уz неспростовна в GMSQ=; 2) формула ху &хz→уz спростовна в GMSQ. 2. Відношення логічного наслідку Відношення логічного наслідку в TMS задаємо на множині формул, специ- фікованих (відмічених) іменами станів, або специфікованих станами формул. Специфікована іменем стану фор- мула має вигляд , де  – формула мови, S – її специфікація, S – певна множина імен станів світу. Специфікація вказує на стан світу, в якому розглядається формула. Множина специфікованих станами формул  із множиною специфікацій S уз- годжена із TMS M = (St, R, A, Im), якщо задана ін’єкція S у St. На множині специфікованих стана- ми формул введемо відношення неспрос- товнісного, істиннісного, хибнісного та сильного логічного наслідку, або логічного IR-наслідку, T-наслідку, F-наслідку, TF- наслідку. Такі відношення відповідають однойменним відношенням в логіках ква- зіарних предикатів (див. [5–7]). Нехай  та  – множини специфі- кованих станами формул. Надалі запис ви- гляду  M\|=*  за умовчанням передбачає узгодженість  та  із TMS M.  є IR-наслідком  в узгодженій із ними TMS M (позн.  M\|=IR ), якщо для всіх dVA маємо: (d) = T для всіх  Ψ(d)  F для деякого Ψ.  є логічним IR-наслідком  віднос- но TMS певного типу ℳ (позн.  ℳ\|=IR ), якщо  M\|=IR  для всіх Mℳ.  є T-наслідком  в узгодженій із ними TMS M (позн.  M\|=T ), якщо для всіх dVA маємо: (d) = T для всіх  Ψ(d) = T для деякого Ψ.  є логічним T-наслідком  віднос- но TMS певного типу ℳ (позн.  ℳ\|=T ), якщо  M\|=T  для всіх Mℳ.  є F-наслідком  в узгодженій із ними TMS M (позн.  M\|=F ), якщо для всіх dVA маємо: Ψ(d) = F для всіх Ψ (d) = F для деякого .  є логічним T-наслідком  віднос- но TMS певного типу ℳ (позн.  ℳ\|=F ), якщо  M\|=F  для всіх Mℳ.  є TF-наслідком  в узгодженій із ними TMS M (позн.  M\|=TF ), якщо  M\|=T  та  M\|=F .  є логічним TF-наслідком  відно- сно TMS певного типу ℳ (позн.  ℳ\|=TF ), якщо  M\|=TF  для всіх Mℳ. Тоді маємо:  ℳ\|=TF   ℳ \|=T  та  ℳ\|=F . Немодальні властивості цих відно- шень повторюють відповідні властивості однойменних відношень для множин фор- мул традиційної логіки квазіарних преди- катів (див. [5–8]). Це такі властивості. 1) Властивості декомпозиції фор- мул L, R, L, R, L, R, а також властивостіL, R для \|=IR (див. [5]). 2) Властивості спрощення та екві- валентних перетворень, пов’язані з рено- мінаціями; вони отримуються на основі властивостей R, R⊥I, R⊥U, R⊥R, R⊥, R⊥, R для предикатів предикатів (див. [7, 8]). 3) Властивості, пов’язані з еліміна- цією кванторів; для GMSQ вони повто- рюють властивості R⊥L, R⊥R, R⊥vR, R⊥vL (див. [8]), в GMSQ= маємо анало- гічні властивості R⊥L=, R⊥R=, R⊥vR=, R⊥vL=, де замість Ez пишемо =zz; до них в GMSQ додаємо властивості E- розподілу Ed та первісного означення Ev (див. [8]), а в GMSQ= додаємо аналогічні властивості =d та =v, де замість Ez пи- шемо =zz. 4) Властивості спрощення, пов’яза- ні з предикатами-індикаторами в GMSQ; це властивості, індуковані властивостями предикатів R⊥E, R⊥Ev та властивість ElRE. 5) Властивості, пов’язані з предика- тами ху в GMSQ; це властивості спро- щення, індуковані властивостями предика- тів R⊥xx, R⊥0, R⊥ 1, R⊥2, R⊥1E, R⊥2E; властивості елімінації константних Теоретичні і методологічні основи програмування 25 формул El та ElR; властивості транзити- вності Tr та заміни рівних R⊥rL, R⊥rL, R⊥rR, R⊥rR. 6) Допоміжні властивості в GMSQ: зняття  при перенесенні  з лівої час- тини відношення наслідку у праву і навпа- ки для символів Ez, ху та їхніх реноміна- цій. 7) Властивості, пов’язані з предика- тами =ху та =хх в GMSQ=; це властивості спрощення, індуковані властивостями пре- дикатів R⊥=zz, R⊥=zz0 R⊥=0, R⊥=1, R⊥=2; властивості ElR=L, ElR=R елімінації ⊥-формул та властивість El=L елімінації pT-формул = zz; властивості транзитивності Tr= та замі- ни рівних =R⊥rL, =R⊥rR. Наведемо умови гарантованої наяв- ності відповідного відношення  \|=. Відношення \|=IR в GMSQ=: С  СRf=  C⊥L  C⊥R. Відношення \|=IR в GMSQ: С  CF  СRf  CEL  CER  CT. Відношення \|=T в GMSQ: С  СL  CF  СRf  CEL  CER  CT. Відношення \|=F в GMSQ: С  СR  CF  СRf  CEL  CER  CT. Відношення \|=TF в GMSQ: С  СLR  CF  СRf  CEL  CER  CT. Зазначені окремі умови вигляду С означають таке для відношення  \|=: С) існує формула :  та ; С) існує формула :  та ; СL) існує формула :  та ; СR) існує формула :  та ; СLR) існують формули , : ,  та ,  ; СF) існує формула , , , , ( ) Γ;v u z xR Ez⊥ ⊥  СRf) існує формула xx; CEL) існують формули xy, Ex, Ey:  xy, Ex та Ey; CER) існують формули xy, Ex, Ey:  xy, Ex, Ey; CT) існує формула , , , , , ,R ( ) Δ;v u x z x xz⊥ ⊥ ⊥   СRf=) існує формула =xx; С⊥L) існує формула , , , , ( ) Γ;v u x w xyR ⊥ ⊥ =  С⊥R) існує формула , , , , ( ) Δ.v u x w xyR ⊥ ⊥ =  3. Cеквенційні числення Семантичною основою побудови для ТМЛ числень секвенційного типу є влас- тивості відношення логічного наслідку для множин специфікованих станами формул. Специфікації мають вигляд \|– чи –\|, де  – ім'я стану Секвенції трактуємо як множини таких формул. Виділяючи \|–- формули та –\|-формули, секвенції познача- ємо \|––\|. Секвенції збагачуємо збудованими на момент виведення множинами відно- шень на станах. Нехай M – схема моделі світу, тобто збудоване на цей момент від- ношення досяжності, записане для імен ста- нів. Збагачені секвенції записуємо  // M. Ми пропонуємо секвенційні чис- лення, які формалізують відношення M=\|=IR в GMSQ= та відношення M\|=IR, M\|=T, M\|=F, M\|=TF в GMSQ. Числення для відношення M=\|=IR в GMSQ= назвемо СGQ=IR, а числення для M\|=IR, M\|=T, M\|=F, M\|=TF в GMSQ назвемо СGQIR, СGQT, СGQF, СGQTF. Секвенційне числення задається ба- зовими секвенційними формами і умовами замкненості секвенції. Виведення в секвенційних числен- нях має вигляд дерева, вершинами якого є секвенції. Правилами виведення секвен- ційних числень є секвенційні форми, вони індукуються властивостями відношень логічного наслідку. Аксіомами секвенцій- ного числення є замкнені секвенції. Для замкненої секвенції \|––\| має вико- нуватись умова  \|= . Секвенційне дере- во замкнене, якщо кожний його лист – за- мкнена секвенція. Секвенція  вивідна, якщо існує замкнене секвенційне дерево з коренем , таке дерево – виведення сек- венції . Умови замкненості секвенції \|––\| задаються наведеними вище.умовами га- рантованої наявності відповідного відно- шення логічного наслідку  \|=. Охарактеризуємо детальніше числен- ня СGQT, СGQF, СGQTF. Вони мають од- Теоретичні і методологічні основи програмування 26 накові базові секвенційні форми, відрізня- ються різними умовами замкненості сек- венції. Ці форми можна розбити на групи. Секвенційні форми, які не пов’язані з модальностями, є аналогами відповідних секвенційних форм в численнях логік ква- зіарних предикатів С⊥ QT, С⊥ QF, С⊥ QTF (див. [7]). Ці форми індукуються власти- востями декомпозиції формул; властивос- тями, пов’язаними з елімінацією кванто- рів; властивостями спрощення та еквіва- лентних перетворень, пов’язаними з ре- номінаціями; властивостями спрощення, пов’язаними з предикатами-індикаторами; властивостями, пов’язаними з предиката- ми ху. Наведемо для прикладу форми, які є аналогами форм \|− , –\|R⊥, \|–R⊥EV− \| та R⊥r \|− α\| \| α\| Φ, Ψ,Σ / / ; (Φ Ψ),Σ / / M M − − −     –\|R⊥ , , α \| , , , α \| , (Φ) (Ψ),Σ / / ; (Φ Ψ),Σ / / v u v u x x v u x R R M R M − ⊥ ⊥ − ⊥   \|–R⊥EV α\| , , \|α , , ,Σ / / ; ( ),Σ / /v u z x y Ey M R Ez M − − ⊥ − \|R⊥r , , , , α\| α \| , , α \| , , , , α\| \| , , , ( ), ( ),Σ / / . , ( ),Σ / / v u z v u z xy w x w y v u z xy w x R p R p M R p M − − ⊥ − ⊥ − − ⊥   До цих форм додаються секвенційні форми, пов’язані з модальностями. Це фо- рми пронесення модальності через реномі- націю \|−R⊥, −\|R⊥, \|−R⊥, −\|R⊥, та форми елімінації модальних операторів (детально описані в [8]). Для прикладу: \|−R , \| , , \| , ( ), / / ; ( ), / / v u x v u x R M R M  − ⊥  − ⊥      −\|R , \| , , \| , ( ), / / . ( ), / / v u x v u x R M R M − ⊥ − ⊥       Для пропонованих модальних сек- венційних числень справджуються теоре- ми коректності та повноти. Доведення тео- рем повноти базується на теоремах про побудову контрмоделі за незамкненим шляхом у секвенційному дереві. Теорема повноти формулюється од- нотипно для кожного з розглянутих чис- лень. У цьому формулюванні відношенням M=\|=IR, M\|=IR, M\|=T, M\|=F, M\|=TF відповідають секвенційні числення СGQ=IR, СGQIR, СGQT, СGQF, СGQTF. Теорема 6 (коректності та повноти).  \|=   секвенція \|–– \| вивідна в чис- ленні C*. Детальний опис пропонованих сек- венційних числень буде зроблено в насту- пних роботах. Висновки Досліджено програмно-орієнтовані логічні формалізми модального типу – чи- сті першопорядкові модальні логіки част- кових немонотонних квазіарних предика- тів. Запропоновано різновиди таких логік з предикатами строгої рівності та слабкої рі- вності. Описано семантичні моделі та мови цих логік. Увагу акцентовано на властиво- стях, пов’язаних із предикатами рівності, описано особливості заміни рівних. Ви- значено низку відношень логічного нас- лідку для множин специфікованих станами формул. На цій семантичній основі для до- сліджених логік запропоновано відповідні числення секвенційного типу. Література 1. S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum (eds), Handbook of Logic in Computer Science, Vol. 1–5, Oxford University Press, 1993–2000. 2. D. Bjorner, M.C. Henson (eds), Logics of Specification Languages, EATCS Series, Monograph in Theoretical Computer Sciens, Springer, 2008. 3. V. Goranko, Temporal Logics, Cambridge University Press, 2023. 4. F. Kröger, S. Merz. Temporal logic and state systems, Springer Science & Business Media, 2008, 436 p. 5. М.С. Нікітченко, O.С. Шкільняк, С.С. Шкільняк, Чисті першопоряд- кові логіки квазіарних предикатів, Проблеми програмування, 2016, № 2–3, C. 73–86. 6. С.С. Шкільняк, Першопорядковi композиційно-номінативні логіки з предикатами слабкої та строгої рів- ності, Проблеми програмування. 2019, № 3, C. 28–44. Теоретичні і методологічні основи програмування 27 7. O. Shkilniak, S. Shkilniak. First-Order Sequent Calculi of Logics of Quasiary Predicates with Extended Renomina- tions and Equality, UkrPROG 2022, CEUR Workshop Proceedings (CEUR-WS.org), 2023, pp. 3–18. 8. М.С. Нікітченко, O.С. Шкільняк, C.С. Шкільняк, Cеквенційні числен- ня першопорядкових логік частко- вих предикатів з розширеними ре- номінаціями та композицією преди- катного доповнення, Проблеми про- грамування, 2020, № 2–3, C. 182–197. 9. О.С. Шкільняк. Mодальні логіки немонотонних часткових предика- тів. Вісник Київського ун-ту. Серія: фіз.-мат. науки. 2015. Вип. 3. C. 141–147. 10. О.С. Шкільняк. Транзиційні мода- льні логіки немонотонних квазіа- рних предикатів. Комп’ютерна ма- тематика. 2014, В. 2. C. 99–110. References 1. S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum (eds), Handbook of Logic in Computer Science, Vol. 1–5, Oxford University Press, 1993–2000. 2. D. Bjorner, M.C. Henson (eds), Logics of Specification Languages, EATCS Series, Monograph in Theoretical Computer Sciens, Springer, 2008. 3. V. Goranko, Temporal Logics, Cambridge University Press, 2023. 4. F. Kröger, S. Merz. Temporal logic and state systems, Springer Science & Business Media, 2008. 5. M. Nikitchenko, O. Shkilniak, S. Shkilniak, Pure first-order logics of quasiary predicates, in Problems in Progamming, 2016, No 2–3. pp. 73–86. 6. S. Shkilniak, First-order composition- nominative logics with predicates of weak equality and of strong equality, in Problems in Progamming, 2019, No 3, pp. 28–44. 7. O. Shkilniak, S. Shkilniak. First-Order Sequent Calculi of Logics of Quasiary Predicates with Extended Renomina- tions and Equality, UkrPROG 2022, CEUR Workshop Proceedings (CEUR-WS.org), 2023, pp. 3–18. 8. M. Nikitchenko, O. Shkilniak, S. Shkilniak, Sequent calculi of first- order logics of partial predicates with extended renominations and composition of predicate complement, in Problems in Progamming, 2020, No 2–3, pp. 182–197. 9. O. Shkilniak, Modal logics of non- monotone partial predicates, in Bulle- tin of Taras Shevchenko National University of Kyiv, Series Physics & Mathematics, 2015, 3, pp. 141–147. 10. O. Shkilniak, Transitional modal logics of non-monotone quasiary pre- dicates, in Computer Mathematics, 2014, 2, pp. 99–110. Одержано: 10.04.2024 Внутрішня рецензія отримана: 21.04.2024 Зовнішня рецензія отримана: 29.04.2024 Про авторів: 1Шкільняк Оксана Степанівна, к.ф.-м.н., доцент. http://orcid.org/0000-0003-4139-2525. 2Шкільняк Степан Степанович, д. ф.-м. н., професор http://orcid.org/0000-0001-8624-5778. Місце роботи авторів: 1Київський національний університет імені Тараса Шевченка, тел. (+38) (044) 259-05-11 E-mail: oksana.sh@knu.ua Сайт: http://csc.knu.ua 2Київський національний університет імені Тараса Шевченка, Тел. (+38) (044) 521-33-45 E-mail: ss.sh@knu.ua, Сайт: http://csc.knu.ua

Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics

Репозитарії

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