Propositional logics of partial predicates with composition of predicate complement

The paper studies new software-oriented logical formalisms – the logics of partial predicates with predicate complement. Such logics are denoted LC. A characteristic feature of these logics is the presence of a special non-monotonic operation (composition) of the predicate complement. Such operation...

Повний опис

Збережено в:

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

Репозитарії

Problems in programming

id	pp_isofts_kiev_ua-article-344
record_format	ojs
resource_txt_mv	ppisoftskievua/3c/e0bdd442d4e9afa2a8354c41b4911f3c.pdf
spelling	pp_isofts_kiev_ua-article-3442024-04-28T11:00:17Z Propositional logics of partial predicates with composition of predicate complement Пропозициональные логики частичных предикатов с композицией предикатного дополнения Пропозиційні логіки часткових предикатів з композицією предикатного доповнення Nikitchenko, M.S. Shkilniak, O.S. Shkilniak, S.S. Mamedov, T.A. logic; partial predicate; logical consequence; sequent сalculus UDC 004.42:510.69 логика, частичный предикат; логическое следствие; секвенциальное исчисление УДК 004.42:510.69 : логіка; предикат; логічний наслідок; секвенційне числення УДК 004.42:510.69 The paper studies new software-oriented logical formalisms – the logics of partial predicates with predicate complement. Such logics are denoted LC. A characteristic feature of these logics is the presence of a special non-monotonic operation (composition) of the predicate complement. Such operations are used in various versions of the Floyd-Hoare logic with partial pre- and post-conditions. Properties of LC propositional compositions are similar to the properties of the traditional logical connectives. Properties of the new composition of the predicate complement are investigated. The class of P-predicates (partial single-valued) is closed under the composition of the predicate complement, but the class of T-predicates (total) is not closed. Therefore, it is possible to consider the general class LC – the logic of R-predicates (relational predicates) with the composition of the predicate complement, and its subclass LPC – the logic of P-predicates with such a composition. The focus of the work is the study of PLC – propositional LC. Propositional composition algebras and PLC languages are described. For LC of partial single-valued predicates, an irrefutability logical consequence relation \|=IR^ is proposed and investigated under the conditions of undefinedness. The conditions for the validity of the \|=IR^ and the properties of the decomposition of formulas are given. Based on the properties of the \|=IR^, for PLC of P-predicates a calculus of sequential type is constructed. The basic sequential forms of this calculus and closure conditions of the sequents are given. For the constructed calculus, correctness and completeness theorems are hold. Proofs of these theorems will be given in the forthcoming articles.Problems in programming 2019; 1: 03-13 В работе исследованы новые программно-ориентированные логические формализмы – логики частичных предикатов с предикатным дополнением, названные LC. Характерная особенность таких логик – наличие специальной немонотонной операции (композиции) предикатного дополнения. Подобные операции используются в различных вариантах логик Флойда – Хоара с частичными пред- и после-условиями. Свойства пропозициональных композиций LC аналогичны свойствам традиционных логических связок. Исследованы свойства новой композиции предикатного дополнения. Класс P-предикатов (однозначных) замкнут относительно композиции предикатного дополнения, а класс T-предикатов (тотальных) незамкнут. Поэтому можно рассматривать общий класс LC – логики R-предикатов (реляционного типа) с композицией предикатного дополнения, и их подкласс LPC – это логики P-предикатов с такой композицией. В центре внимания работы – изучение пропозициональных LC, или PLC. Описаны пропозициональные композиционные алгебры и языки PLC. Для LC однозначных предикатов предложено и исследовано отношение \|=IR^ неопровержимого логического следствия при условиях неопределенности. Приведены условия наличия отношения \|=IR^ и свойства декомпозиции формул. На этой основе для PLC P-предикатов построено исчисление секвенциального типа. Приведены базовые секвенциальные формы этого исчисления и условия замкнутости секвенций. Для построенного исчисления верны теоремы корректности и полноты. Доказательства этих теорем будут приведены в последующих статьях.Problems in programming 2019; 1: 03-13 Досліджено нові програмно-орієнтовані логічні формалізми – логіки часткових предикатів з операцією (композицією) предикатного доповненням, названі LC. Подібні операції використовуються в різних варіантах логік Флойда – Хоара з частковими перед- та після-умовами. В даній роботі вивчаються LC пропозиційного рівня – PLC. Описано пропозиційні композиційні алгебри та мови PLC, запропоновано та досліджено відношення неспростовнісного логічного наслідку за умов невизначеності. На цій основі для PLC однозначних предикатів побудовано числення секвенційного типу.Problems in programming 2019; 1: 03-13 Інститут програмних систем НАН України 2019-03-26 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/344 10.15407/pp2019.01.003 PROBLEMS IN PROGRAMMING; No 1 (2019); 03-13 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2019); 03-13 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2019); 03-13 1727-4907 10.15407/pp2019.01 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/344/341 Copyright (c) 2019 PROBLEMS IN PROGRAMMING
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2024-04-28T11:00:17Z
collection	OJS
language	Ukrainian
topic	logic partial predicate logical consequence sequent сalculus UDC 004.42:510.69
spellingShingle	logic partial predicate logical consequence sequent сalculus UDC 004.42:510.69 Nikitchenko, M.S. Shkilniak, O.S. Shkilniak, S.S. Mamedov, T.A. Propositional logics of partial predicates with composition of predicate complement
topic_facet	logic partial predicate logical consequence sequent сalculus UDC 004.42:510.69 логика частичный предикат; логическое следствие; секвенциальное исчисление УДК 004.42:510.69 : логіка предикат логічний наслідок секвенційне числення УДК 004.42:510.69
format	Article
author	Nikitchenko, M.S. Shkilniak, O.S. Shkilniak, S.S. Mamedov, T.A.
author_facet	Nikitchenko, M.S. Shkilniak, O.S. Shkilniak, S.S. Mamedov, T.A.
author_sort	Nikitchenko, M.S.
title	Propositional logics of partial predicates with composition of predicate complement
title_short	Propositional logics of partial predicates with composition of predicate complement
title_full	Propositional logics of partial predicates with composition of predicate complement
title_fullStr	Propositional logics of partial predicates with composition of predicate complement
title_full_unstemmed	Propositional logics of partial predicates with composition of predicate complement
title_sort	propositional logics of partial predicates with composition of predicate complement
title_alt	Пропозициональные логики частичных предикатов с композицией предикатного дополнения Пропозиційні логіки часткових предикатів з композицією предикатного доповнення
description	The paper studies new software-oriented logical formalisms – the logics of partial predicates with predicate complement. Such logics are denoted LC. A characteristic feature of these logics is the presence of a special non-monotonic operation (composition) of the predicate complement. Such operations are used in various versions of the Floyd-Hoare logic with partial pre- and post-conditions. Properties of LC propositional compositions are similar to the properties of the traditional logical connectives. Properties of the new composition of the predicate complement are investigated. The class of P-predicates (partial single-valued) is closed under the composition of the predicate complement, but the class of T-predicates (total) is not closed. Therefore, it is possible to consider the general class LC – the logic of R-predicates (relational predicates) with the composition of the predicate complement, and its subclass LPC – the logic of P-predicates with such a composition. The focus of the work is the study of PLC – propositional LC. Propositional composition algebras and PLC languages are described. For LC of partial single-valued predicates, an irrefutability logical consequence relation \|=IR^ is proposed and investigated under the conditions of undefinedness. The conditions for the validity of the \|=IR^ and the properties of the decomposition of formulas are given. Based on the properties of the \|=IR^, for PLC of P-predicates a calculus of sequential type is constructed. The basic sequential forms of this calculus and closure conditions of the sequents are given. For the constructed calculus, correctness and completeness theorems are hold. Proofs of these theorems will be given in the forthcoming articles.Problems in programming 2019; 1: 03-13
publisher	Інститут програмних систем НАН України
publishDate	2019
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/344
work_keys_str_mv	AT nikitchenkoms propositionallogicsofpartialpredicateswithcompositionofpredicatecomplement AT shkilniakos propositionallogicsofpartialpredicateswithcompositionofpredicatecomplement AT shkilniakss propositionallogicsofpartialpredicateswithcompositionofpredicatecomplement AT mamedovta propositionallogicsofpartialpredicateswithcompositionofpredicatecomplement AT nikitchenkoms propozicionalʹnyelogikičastičnyhpredikatovskompoziciejpredikatnogodopolneniâ AT shkilniakos propozicionalʹnyelogikičastičnyhpredikatovskompoziciejpredikatnogodopolneniâ AT shkilniakss propozicionalʹnyelogikičastičnyhpredikatovskompoziciejpredikatnogodopolneniâ AT mamedovta propozicionalʹnyelogikičastičnyhpredikatovskompoziciejpredikatnogodopolneniâ AT nikitchenkoms propozicíjnílogíkičastkovihpredikatívzkompozicíêûpredikatnogodopovnennâ AT shkilniakos propozicíjnílogíkičastkovihpredikatívzkompozicíêûpredikatnogodopovnennâ AT shkilniakss propozicíjnílogíkičastkovihpredikatívzkompozicíêûpredikatnogodopovnennâ AT mamedovta propozicíjnílogíkičastkovihpredikatívzkompozicíêûpredikatnogodopovnennâ
first_indexed	2024-09-16T04:07:51Z
last_indexed	2024-09-16T04:07:51Z
_version_	1818568264019607552
fulltext	Теоретичні та методологічні основи програмування © М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк, Т.А. Мамедов, 2019 ISSN 1727-4907. Проблеми програмування. 2019. № 1 3 УДК 004.42:510.69 https://doi.org/10.15407/pp2019.01.003 М.С. Нікітченко, О.С. Шкільняк, C.С. Шкільняк, Т.А. Мамедов ПРОПОЗИЦІЙНІ ЛОГІКИ ЧАСТКОВИХ ПРЕДИКАТІВ З КОМПОЗИЦІЄЮ ПРЕДИКАТНОГО ДОПОВНЕННЯ Досліджено нові програмно-орієнтовані логічні формалізми – логіки часткових предикатів з операцією (композицією) предикатного доповненням, названі LC. Подібні операції використовуються в різних ва- ріантах логік Флойда – Хоара з частковими перед- та після-умовами. В даній роботі вивчаються LC пропозиційного рівня – PLC. Описано пропозиційні композиційні алгебри та мови PLC, запропоновано та досліджено відношення неспростовнісного логічного наслідку за умов невизначеності. На цій основі для PLC однозначних предикатів побудовано числення секвенційного типу. Ключові слова: логіка, предикат, логічний наслідок, секвенційне числення. Вступ Розроблено багато різноманітних логічних систем, які успішно застосову- ються в інформатиці й програмуванні [1]. Проте класична логіка має принципові об- меження, які істотно ускладнюють її вико- ристання. В основу цих систем зазвичай покладена класична логіка предикатів та базовані на ній спеціальні логіки (модаль- ні, темпоральні, програмні тощо). Обме- ження класичної логіки роблять актуаль- ною проблему побудови нових, програм- но-орієнтованих логічних формалізмів. В останні роки запропоновано різні підходи до побудови логік, орієнтованих на потре- би моделювання, специфікації та верифі- кації програмних систем [2 – 5. Перспек- тивним напрямком побудови програмно- орієнтованих логік є спільний для логіки й програмування композиційно-номіна- тивний підхід. Логіки, збудовані на його основі, названо композиційно-номінатив- ними (КНЛ). Різноманітні класи КНЛ опи- сано та досліджено в [6 – 10]. В даній роботі досліджено нові про- грамно-орієнтовані логічні формалізми – логіки часткових квазіарних предикатів з предикатним доповненням. Такі логіки на- звані LC. Характерною особливістю LC є наявність спеціальної немонотонної опе- рації (композиції) предикатного доповнен- ня. Подібні операції використовуються в різних варіантах логік Флойда – Хоара з частковими перед- та після-умовами [11]. Основна увага в роботі зосереджена на ви- вченні LC пропозиційного рівня – PLC. Досліджено властивості композиції преди- катного доповнення. Описано пропозицій- ні композиційні алгебри та мови PLC. Для LC однозначних предикатів запропоновано відношення неспростовнісного логічного наслідку за умов невизначеності. Дослі- джено властивості цього відношення, на цій семантичній основі для PLC однознач- них предикатів побудовано числення сек- венційного типу. Поняття, які тут не визначаються, тлумачимо в сенсі [7, 9]. Для полегшення читання нагадаємо основні визначення. V-A-квазіарний предикат – це част- кова неоднозначна, взагалі кажучи, функ- ція вигляду Р : V A {T, F}. Тут {T, F} – множина істиннісних значень, V A – мно- жина всіх V-A-іменних множин, тобто множина всіх однозначних функцій вигля- ду d : V A. Трактуємо V як множину пре- дметних імен (змінних), A – як множину базових значень. Множину всіх значень, які неодно- значний предикат P може приймати на ар- гументі (даному) d, будемо позначати P[d]. 1. Квазіарні предикати реляційного типу Далі будемо розглядати неоднозна- чні (недетерміновані) предикати реляцій- ного типу, або R-предикати. Клас V-A-квазіарних R-предикатів тут позначаємо Pr V–A . Кожний V-A-квазіарний R-предикат P : V A {T, F} на даному d V А може прий- мати лише значення T, лише значення F, http://dx.doi.org/10.7124/bc.000027 Теоретичні та методологічні основи програмування 4 обидва значення T та F, а також може бути невизначеним. Тому для R-предиката P множина P[d] може бути однією з множин , {T}, {F}, {T, F}. Кожний R-предикат P можна одно- значно задати за допомогою 2-х множин: – область істинності, або T-область T(P) = {d V A \| TP[d]}; – область хибності, або F-область F(P) = {d V A \| FP[d]}. Для R-предикатів область невизна- ченості, або -область, цілком залежить від T-області та F-області. -область (P) R-предикатa P визначається T(P) та F(P) так: ( ) ( ) ( ) ( ) ( )P T P F P T P F P     . V-A-квазіарний R-предикат P: – частковий однозначний або P-пре- дикат, якщо T(P)F(P) = ; – тотальний, або T-предикат, якщо T(P)F(P) = V A; тоді маємо (P) = . Для P-предикатів пишемо Q(d), якщо значення Q(d) визначене, та пишемо Q(d), якщо значення Q(d) невизначене. Таким чином, для P-предикатів T-область та F-область можна визначити так: T(Q) = {d V А \| Q(d) = T}, F(Q) = {d V А \| Q(d) = F}. Тоді ( )Q  {d V A \| Q(d)}. Клaс V-А-квазіарних P-предикатів будемо позначати PrP V–A . Використовуючи області істинності та хибності, можна виділити [9] низку різ- новидів R-предикатів. Зокрема, в класі R-предикатів виділено 4 константних: – тотожно істинний предикат T (ма- ємо T(T) = V А та F(T) = , тоді (T) = ); – тотожно хибний предикат F (має- мо F(F T) = V А та T(F) = , тоді (F) = ); – тотожно невизначений предикат  (маємо T() = F() = , тоді () = V А); – тотально амбівалентний предикат  (маємо T() = F() = V А, тоді () = ). 2. Пропозиційні композиції R-предикатів Hа пропозиційному рівні предикати можна трактувати як функції вигляду Р : D {T, F}, де D – сукупність абстракт- них даних. На гранично абстрактному рівні дані трактуємо як "чорні скриньки", які неможливо відрізнити одне від одного. Тому на пропозиційному рівні предикати можна розглядати як задані на одиничному абстрактному даному. Кожний предикат на цьому даному може приймати певне іс- тиннісне значення або бути невизначеним. Отже, на пропозиційному рівні композиції фактично працюють лише з виробленими предикатами істиннісними значеннями. Традиційно такі композиції називають логiчними зв’язками. Мінімально конкретизувавши рі- вень розгляду, трактуємо D як сукупність відмінних одне від одного даних, абстракт- них в тому розумінні, що їх структура не- відома ("чорні скриньки" різної ваги чи форми). Кожний предикат Р : D {T, F} тоді можна трактувати як об'єднання гра- нично абстрактних предикатів, заданих на одиничних даних – елементах D. Для квазіарних предикатів множину даних D уточнюємо як V A. Основними логічними зв’язками є 1-арна композиція заперечення  та бінар- ні композиції диз’юнкція , кон’юнкція &, імплікація , еквіваленція . Визначення композицій , , &, ,  дамо, задаючи предикати (P), (P, Q), &(P, Q), (P, Q), (P, Q). Ці предикати будемо скорочено позначати P, PQ, P&Q, PQ, PQ. У випадку R-предикатів визначення пропозиційних композицій природно дати [7] через області істинності й хибності від- повідних предикатів: T(P) = F(P); F(P) = T(P); T(PQ) = T(P)T(Q); Теоретичні та методологічні основи програмування 5 F(PQ) = F(P)F(Q); T(P&Q) = T(P)T(Q); F(P&Q) = F(P)F(Q); T(PQ) = F(P)T(Q); F(PQ) = T(P)F(Q); T(PQ) = (F(P)T(Q))(F(Q)T(P)); F(PQ) = (T(P)F(Q))(F(P)T(Q)). У випадку Р-предикатів визначення композицій , , &, ,  подібні до ви- значень відповідних класичних логічних зв’язок [12]. Такі пропозиційні композиції є аналогами відповідних сильних зв'язок Кліні [13], тому їх називають Клінієвими. Для Р-предикатів визначення про- позиційних композицій можна дати більш традиційно, через значення відповідних предикатів. Наведемо тут визначення ком- позицій , , &. Для довільного d V А задаємо: , якщо ( ) , ( )( ) , якщо ( ) , невизначене, якщо ( ) . T P d F P d F P d T P d      , якщо ( ) або ( ) , , якщо ( ) ( )( ) та ( ) , невизначене в усіх інших випадках. T P d T Q d T F P d F P Q d Q d F             , якщо ( ) та ( ) , , якщо ( ) ( & )( ) aбо ( ) , невизначене в усіх інших випадках. T P d T Q d T F P d F P Q d Q d F            Для Р-предикатів визначення про- позиційних композицій через області іс- тинності й хибності еквівалентні їх визна- ченням через значення відповідних преди- катів. Композиції  та  назвемо базови- ми пропозиційними композиціями. Композиції , &,  є похідними, вони виражаються через базові композиції  та : P&Q = (PQ); PQ = PQ; PQ = (PQ)&(QP). Твердження 1. Для -області R-пре- дикатів маємо: ( ) ( );Q Q   ( ) ( ( ) ( )) ( ( ) ( )).P Q P T Q Q T P        Справді, маємо (Q) ( ) ( )T Q F Q     ( ) ( )F Q T Q  (Q); ( ) ( ) ( )P Q T P Q F P Q       ( ) ( ) ( ( ) ( )T P T Q F P F Q     ( ) ( ) ( ( ) ( ))T P T Q F P F Q     ( ( ) ( ) ( ))T P F P T Q    ( ( ) ( ) ( ))T Q F Q T P    ( ( ) ( )) ( ( ) ( ))P T Q Q T P      . Тут враховано, що ( ) ( ) ( )S T S F S   ). В загальному випадку R-предикатів ( )T S  ( ) ( )S F S  . Водночас для P-предикатів множи- ни T(S), F(S), (S) – диз’юнктні, звідки ( )T S  ( ) ( )S F S  . Твердження 2. Для -області P-пре- дикатів маємо: ( ) ( ( ) ( ))P Q P Q      ( ( ) ( )) ( ( ) ( ))P F Q Q F P      ; ( & ) ( ( ) ( ))P Q P Q     ( ( ) ( )) ( ( ) ( ))P T Q Q T P      . Справді, маємо ( )P Q   ( ( ) ( )) ( ( ) ( ))P T Q Q T P       ( ( ) ( ( ) ( )))P Q F Q      Теоретичні та методологічні основи програмування 6 ( ( ) ( ( ) ( )))Q P F P      ( ( ) ( )) ( ( ) ( ))P Q P F Q       . ( ( ) ( ))Q F P   . Це означає: (PQ)(d)  P(d) та Q(d) або P(d) та Q(d) = F або P(d) = F та Q(d). Подібним чином отримуємо вираз для ( & )P Q . Зазначимо, що для найзагальнішого класу недетермінованих предикатів – GND-предикатів [14] – маємо такі ж по- дання (PQ) та (P&Q), як і для Р-предикатів. Водночас, на відміну від R-предикатів, для GND-предикатів можли- во (P)T(P)   та (P)F(P)  . Основні властивості пропозиційних композицій R-предикатів аналогічні влас- тивостям відповідних класичних логічних зв’язок [6, 12]. Клас P-предикатів замкнений [7, 9] щодо композицій , , &, , . 3. Композиція предикатного доповнення Характерною особливістю LC є на- явність спеціальної 1-арної композиції предикатного доповнення . Ця компози- ція задається так:  , якщо ( ) , ( )( ) невизначене, якщо ( ) . T P d P d P d  Отже, композиція немонотонна. Композицію можна задати через T-область і F-область відповідного преди- ката: ( )T P = ( ) ( ) ( ) ( ) ( ),P T P F P T P F P     ( )F P  . Тоді маємо ( ) ( ) ( )P T P F P   . Класи P-предикатів та R-предикатів замкнені щодо композиції . Для довільного R-предиката Q маємо, що Q є P-предикатом, тому клас T-предикатів незамкнений щодо . Отже, для T-предикатів LC не ма- ють смислу. Таким чином, можна розглядати загальний клас LC – логіки R-предикатів з композицією предикатного доповнення, та їх підклас LPC – логіки P-предикатів з композицією предикатного доповнення. Для LC пропозиційного рівня маємо загальний клас PLC R-предикатів та його підклас PLPC – PLC P-предикатів. Композиції , , – це базові ком- позиції PLC. 4. Пропозиційні композиційні алгебри та мови LC Семантичною основою LC є компо- зиційні предикатні системи вигляду ( V A, Pr V–A , CLС), де CLС – множина базових композицій. Така композиційна система задає дві алгебри: алгебру (алгебраїчну си- стему) даних ( V A, Pr V–A ) та композиційну алгебру предикатів ( V A, Pr V–A , CLС). Композиційну систему вигляду ( V A, Pr V–A , CPLС), де множина композицій CPLС ={ , , }  , назвемо пропозиційною композиційною LC-системою R-предика- тів. Алгебру APLC = (Pr V–A , CPLС) на- звемо пропозиційною композиційною LC- алгеброю R-предикатів. Клас P-предикатів замкнений щодо композиції . Тому можна говорити про те, що в алгебрі APLC виділена підалгебра APLCP = (PrP V–A , CPLС) – пропозиційна композиційна LC-алгебра P-предикатів. Розглянемо основні властивості композицій PLС. Твердження 3. Із визначень отри- муємо такі властивості композиції : P  P ; P  P ; P P . Для P-предикатів додатково маємо: P P P  . Таким чином, багатократне засто- сування композиції зводиться до 1-крат- ного та до 2-кратного її застосування. Теоретичні та методологічні основи програмування 7 Із визначень отримуємо:  , якщо ( ) , ( )( ) невизначене, якщо ( ) F P d P d P d   Маємо ( ) ( )F P T P  (P), зві- дки отримуємо: ( ) ( ) ( ) ( ) ( ),F P T P F P T P F P     ( )T P  . Властивості пропозиційних компо- зицій в LC аналогічні властивостям пропо- зиційних композицій R-предикатів у тра- диційних логіках квазіарних предикатів [7]. Твердження 4. Маємо такі основні властивості композицій , , & в LC. 1) комутативність  та &: PQ = QP; P&Q = Q&P. 2) асоціативність  та &: (PQ)R = P(QR); (P&Q)&R = P&(Q&R). 3) дистрибутивність  відносно & та & відносно : (PQ)&R = (P&R)(Q&R); (P&Q)R = (PR)&(QR). 4) ідемпотентність  та &: Р = РР; Р = Р&Р. 5) зняття подвійного заперечення: P = Р. 6) закон контрапозиції: P  Q = Q  P. 7) закони де Моргана: (PQ) = (P)&(Q); (P&Q) = (P)(Q). 8) закони поглинання: Р = P(P&Q); Р = P&(PQ). Опишемо мови PLC. Алфавiт мови: – множина V предметних імен, або змінних, – множина Ps предикатних сим- волів, – множина CsPLС = { , , }  симво- лів базових композицій. Множину Fr формул мови визнача- ємо так. Маємо Ps  Fr, а далі задаємо індук- тивно: , Fr  , , Fr . Інтерпретуємо мову на композицій- них системах ( V A, Pr V–A , CPLС). Задаємо тотальне однозначне відо- браження інтерпретації предикатних сим- волів I : Ps Pr V–A , яке далі продовжуємо до відображення інтерпретації формул I : Fr Pr V–A : I() = (I()), I() = (I(), I()), ( ) ( ( ))I I   . Нехай J = (A, I) – інтерпретація. Предикат J() позначаємо J. Композиції пропозиційного рівня беруть до уваги лише вироблені предика- тами істиннісні значення, тому кожне ві- дображення інтерпретації I : Ps Pr V–A індукує сукупність істиннісних оцінок (взагалі кажучи, часткових) таким чином. Для кожного d V A задаємо іс- тиннiсну оцiнку d : Ps {T, F} так: d(p) = pJ(d). Тоді для кожної Fr маємо d() = J(d). Зокрема, якщо J(d), то й d(). Виділення класів квазіарних преди- катів виділяє відповідні класи інтерпрета- цій. Такі класи інтерпретацій називають [9] семантиками. Клас T-предикатів незамкнений що- до , тому для LC змістовними є R-се- Теоретичні та методологічні основи програмування 8 мантика та P-семантика, будемо їх відпо- відно позначати RС та PС. Фіксуючи пропозиційний рівень, для PLC отримуємо семантики RPС та PPС. Зрозуміло, що наведені вище влас- тивості логічних зв'язок та композиції пре- дикатного доповнення можна подати із ви- користанням формул мови PLC. 5. Відношення логічного наслідку за умов невизначеності На множинах формул LC можна ви- значити низку відношень логічного нас- лідку. В даній роботі введемо та досліди- мо відношення неспростовнісного логічно- го наслідку за умов невизначеності. Таке відношення є узагальненням відомого [7, 9] відношення неспростовнісного логі- чного наслідку для традиційних логік ква- зіарних предикатів. Нехай деяка   Fr; нехай J – інте- рпретація. Далі позначаємо: ( )JT   як T  (J), ( )JF   як F  (J), ( )J    як   (J). Множина  може бути порожньою. У випадку, коли  = , маємо: T  () = T  () = F  () = F  () = =   () =   () = V A. Спочатку вводимо відношення не- спростовнісного наслідку за умов невизна- ченості при певній інтерпретації. Нехай , , Fr. Неформально те, що  є неспростовнісним наслідком  за умови невизначеності  при інтерпретації J, має означати: “якщо J невизначене, то неможливо, що J істинне та J хибне”. Це можна уточнити так: “для кожного d V A якщо J(d), то неможливо J(d) = T та J(d) = F”. Останнє твердження рівносильне такому: “для кожного d V A неправильно J(d) або неправильно J(d) = T та J(d) = F”. Це в свою чергу рівносильне такому: “для кожного d V A неправильно, що J(d), та J(d) = T та J(d) = F”. Таким чином, початкове твердження звелося до рівносильної умови: “не існує d V A таких, що d(J)  T(J)  F(J)”, що дає умову (J)  T(J)  F(J) = . Подібні міркування можна провести для множин формул. Нехай , U,   Fr. Неформально те, що  є неспростовнісним наслідком  за умов невизначеності U при інтерпретації J, має означати: “для кожного d V A, якщо J(d) для всіх JU, то неможливо J(d) = T для всіх  та J(d) = F для всіх ”. Це твердження рівносильне такому: “для кожного d V A, якщо d  (UJ), то неможливо dT  (J) та dF  (J)”. Останнє твердження рівносильне такому: “для кожного d V A неправильно, що d  (UJ) та dT  (J)  F  (J), тобто неправильно, що d  (UJ)  T  (J)   F  (J)”. Отже, те, що  є неспростовнісним наслідком  за умов невизначеності U, звелося до такої умови: “не існує d V A таких, що d  (UJ)  T  (J)  F  (J)”. Це означає: T  (J)    (UJ)  F  (J) = . Той факт, що  є неспростовнісним наслідком  за умов невизначеності U при інтерпретації J, будемо позначати U /  J\|=IR  . Таким чином, ми прийшли до наступ- ного визначення: U /  J\|=IR  , якщо T  (J)    (UJ)  F  (J) = . Зокрема, якщо U = , то отримуємо умову T  (J)  F  (J) =  – умову відно- шення неспростовнісного наслідку  J\|=IR . Відношення неспростовнісного ло- гічного наслідку в LC за умов невизна- ченості визначаємо традиційно.  є неспростовнісним логічним нас- лідком  за умов невизначеності U, що позначимо U /  \|=IR  , якщо U /  J\|=IR   для кожної інтерпретації JPС. Теоретичні та методологічні основи програмування 9 Зокрема, якщо U = , то отримуємо відоме відношення  \|=IR . 6. Властивості відношення \|=IR  Опишемо основні властивості від- ношення \|=IR  на пропозиційному рівні. Із визначень отримуємо властивість монотонності M: M) нехай   , U  W, та   ; тоді U /  \|=IR    W /  \|=IR  . Теорема 1. Маємо такі властивості гарантованої наявності відношення логіч- ного наслідку \|=IR  : С) U / ,  \|=IR  , ; СUL) U, / ,  \|=IR  ; СUR) U, /  \|=IR  , ; C ) U /  \|=IR  ,  . Доведемо властивість С. Для P-предикатів T(J)  F(J) = . Тоді для кожної інтерпретації J маємо T(J)T  (J)    (UJ)  F  (J)F(J) = , звідки U / ,  \|=IR  , . Доведемо властивість СUL. Маємо (J)  T(J) = . Звідси для кожної інтерпретації J отримуємо T(J)T  (J)    (UJ)(J)  F  (J) = , звідки U, / ,  \|=IR  . Доведемо властивість СUR. Маємо (J)  F(J) = . Звідси для кожної інтерпретації J отримуємо T  (J)    (UJ)(J)  F  (J)F(J) = , звідки U, /  \|=IR  , . Доведемо властивість C . Для кож- ної інтерпретації J маємо F( J) = , то- му T  (J)    (UJ)  F  (J)F( J) = , звідки U /  \|=IR  ,  . Теорема 2. Для відношення \|=IR  маємо наступні властивості декомпозиції формул: L) U /,  \|=IR    U /  \|=IR  , . R) U /  \|=IR  ,   U / ,  \|=IR  . L) U / ,  \|=IR     U / ,  \|=IR   та U / ,  \|=IR  . R) U /  \|=IR  ,    U /  \|=IR  , , . U) U, /  \|=IR    U,  /  \|=IR  . U) U, /  \|=IR     U,, /  \|=IR   та U, /  \|=IR  ,  та U, /  \|=IR  , . U) U,  /  \|=IR     U / ,  \|=IR   та U /  \|=IR  , . L) U / ,  \|=IR     U,  /  \|=IR  . Властивості L, R, L, R аналогі- чні відповідним властивостям відношення \|=IR [7, 9] та доводяться подібним чином. Новими для LC є специфічні властивості U, U, L, U. Доведемо властивість U. Для кожної інтерпретації J маємо (J) = (J), звідки U, /  J\|=IR     T  (J)    (UJ)(J)  F  (J) =   T  (J)    (UJ)(J)  F  (J) =   U,  /  J\|=IR  . Властивість U випливає з того, що для P-предикатів маємо: ( ) ( ( ) ( ))J J J J         ( ( ) ( )) ( ( ) ( ))J J J JF F         . При цьому враховуємо таке теоре- тико-множинне співвідношення: L(()(F)(F)) = = (L)(LF) (LF) =    L =  та LF =  та LF = . Таким чином, для кожної інтерпре- тації J маємо: U, /  J\|=IR     T  (J)    (UJ)(J)  F  (J) =  Теоретичні та методологічні основи програмування 10  T  (J)    (UJ)(((J)(J)) ((J)F(J))(F(J)(J)))F  (J) =   T  (J)  (UJ)(J)(J)F  (J) = , та T  (J)  (UJ)(J)F(J)F  (J) = , та T  (J)  (UJ)F(J)(J)F  (J) =   U,, /  J\|=IR   та U, /  J\|=IR  ,  та U, /  J\|=IR  , . Властивість U випливає із такого:  ( )J = T(J)  F(J). При цьому враховуємо наступне те- оретико-множинне співвідношення: L  (LT  LF) = (L  LT)  (L  LF) =    L  LT =  та L  LF = . Таким чином, для кожної інтерпре- тації J маємо: U,  /  J\|=IR     T  (J)    (UJ)   ( )J  F  (J) =   T  (J)    (UJ)  (T(J)F(J))   F  (J) =    T  (J)    (UJ)  T(J)  F  (J) =  та T  (J)    (UJ)  F(J)  F  (J) =    U / ,  J\|=IR   та U /  J\|=IR  , . Властивість L випливає із такого: ( )JT  = (J). Тоді для кожної інтерпретації J маємо: U / ,  \|=IR     ( )JT  T  (J)    (UJ)  F  (J) =   T  (J)    (UJ)  (J)  F  (J) =   U,  /  \|=IR  . 7. Пропозиційнe секвенційнe числення для відношення \|=IR  Для відношення \|=IR  в PLC побуду- ємо числення секвенційного типу. Таке числення назвемо PPC . Секвенції будемо трактувати як множини формул, специфікованих (відмі- чених) символами \|–, –\|,  . Формули із  (вони відмічені сим- волом \|–) назвемо T-формулами, формули із  (вони відмічені символом –\|) назвемо F-формулами, а формули із U (вони відмі- чені символом  ) –  -формулами, Це від- повідає семантичному трактуванню фор- мул із  як істинних, формул із  – як хиб- них. а формул із U – як невизначених. Позначаємо секвенції як \|–  U –\|, скорочено як . Виведення в секвенційних числен- нях має вигляд дерева, вершинами якого є секвенції. Такі дерева називають секвен- ційними. Правилами виведення секвенційних числень є секвенційні форми. Вони є син- таксичними аналогами семантичних влас- тивостей відповідних відношень логічного наслідку. Секвенційні форми будемо запису- вати у вигляді   або    , або     . Секвенції над рискою називають за- сновками, під рискою – висновками. У нашому випадку засновки – це секвенції, зіставлені правим частинам відповідних семантичних властивостей, висновки – це секвенції, зіставлені їх лівим частинам. Дамо індуктивне визначення секве- нційного дерева. 1. Секвенція  утворює тривіальне секвенційне дерево з єдиною вершиною , яка є коренем дерева. 2. Нехай , ,  – секвенційнi де- ревa, коренями яких є відповідно , , ; нехай   ,    ,     – секвенційні форми. Тоді \|   , \ /    , \ \| /     – секвен- ційні дерева з коренем . Аксіомами секвенційного числення є замкнені секвенції. Поняття замкненої секвенції уточню- ється так, що має виконуватись умова: Теоретичні та методологічні основи програмування 11 якщо секвенція \|– U –\| замкнена, то U /  \|=IR  . Секвенція  вивідна, або має виве- дення, якщо існує замкнене секвенційне дерево з коренем . Таке дерево називають виведенням секвенції . Тривіальне секвенційне дерево за- мкнене, якщо це замкнена секвенція. Нетривіальне секвенційне дерево замкнене, якщо кожний його лист (кінцева вершина, відмінна від кореня) – замкнена секвенція. Секвенційне числення визначається базовими секвенційними формами та умо- вами замкненості секвенції. Наведемо умову замкненості секвенції у численні PPC. Секвенція \|– U –\| замкнена, якщо виконується умова C  CUL  CUR C . Тут: C) існує :  та ; CUL) існує :  та U; CUR) існує :  та U. C ) існує :  . Замкненість секвенції \|– U –\| гарантує наявність логічного наслідку U /  \|=IR  . Це безпосередньо випливає з влас- тивостей гарантованої наявності логічного наслідку С, СUL, СUR, C . Базові секвенційні форми PPC- числень – це форми декомпозиції, вони індукуються відповідними властивостями декомпозиції формул: \| \| \| , ,       ; \|  \| \| , ,       ; \| \| \| \| , , ,          ; \| \| \| \| , , ,         ;  , ,       ;  \| \| , , , , , , ,                   ;  \| \|, , ,          ; \| \| , ,       . Форми декомпозиції індукуються відповідними властивостями декомпозиції формул L, R, L, R, U, U, U, L. На базі властивостей відношення \|=IR  маємо основну властивість секвенцій- них форм PPC-числень. Теорема 3. 1. Нехай \| \| \| \| W U           – базова сек- венційна форма. Тоді: a) U /  \|=IR    W /  \|=IR  ; b) U /  \|IR    W /  \|IR  ; 2. Нехай \| \| \| \| \| \| W V U                – ба- зова секвенційна форма. Тоді: a) U /  \|=IR    W /  \|=IR   та V /  \|=IR  ; b) U /  \|IR    W /  \|IR   або V /  \|IR  . 3. Нехай \| \| \| \| \| \| \| \| W V Y U                     – базова секвенційна форма. Тоді: a) U /  \|=IR    W /  \|=IR   та V /  \|=IR   та Y /  \|=IR  ; b) U /  \|IR    W /  \|IR   або V /  \|IR   або Y /  \|IR  . Для побудованого секвенційного числення справджуються теореми корект- ності та повноти. Доведення цих теорем будуть наведені в наступних статтях. Висновки В роботі досліджено нові програм- но-орієнтовані логічні формалізми – логіки часткових квазіарних предикатів з преди- катним доповненням. Такі логіки названі LC. Характерною особливістю цих логік є наявність спеціальної немонотонної опера- Теоретичні та методологічні основи програмування 12 ції (композиції) предикатного доповнення. Подібні операції використовуються в різ- них варіантах логік Флойда – Хоара з част- ковими перед- та після-умовами. Основна увага в роботі зосереджена на вивченні LC пропозиційного рівня – PLC. Досліджено властивості композиції предикатного доповнення. Описано пропо- зиційні композиційні алгебри та мови PLC. Для LC однозначних предикатів за- пропоновано та досліджено відношення неспростовнісного логічного наслідку за умов невизначеності. На основі власти- востей цього відношення для PLC одно- значних предикатів побудовано числення секвенційного типу. Література 1. Handbook of Logic in Computer Science. Edited by S. Abramsky, Dov M. Gabbay and T. S. E. Maibaum. Oxford University Press, Vol. 1–5. 1993–2000. 2. Avron A., Zamansky A. Non-deterministic semantics for logical systems, in Handbook of Philosophical Logic, D.M. Gabbay, F. Guenthner (eds.), 2 nd ed. Vol. 16. (2011). Springer Netherlands. P. 227–304. 3. Gries D., Schneider F.B. Avoiding the undefined by underspecification. Springer Berlin Heidelberg. 1995. P. 366–373. 4. Hähnle R. Many-valued logic, partiality, and abstraction in formal specification languages. Logic Journal of the IGPL. 13 (2005). P. 415–433. 5. Jones C. Reasoning about partial functions in the formal development of programs. In: Proceedings of AVoCS’05. Vol. 145. Elsevier, Electronic Notes in Theoretical Computer Science (2006). P. 3–25. 6. Нікітченко М.С. Математична логіка та теорія алгоритмів. К.: ВПЦ Київський уні- верситет. 2008. 528 с. 7. Нікітченко М.С. , Шкільняк С.С. Приклад- на логіка. К.: ВПЦ Київський університет. 2013. 278 с. 8. Nikitchenko М., Shkilniak S. Semantic Properties of Logics of Quasiary Predicates. Workshop on Foundations of Informatics: Proceedings FOI-2015. Chisinau, Moldova. P. 180–197. 9. Нікітченко М.С., Шкільняк О.С., Шкільняк С.С. Чисті першопорядкові логіки квазіар- них предикатів. Проблеми програмування. 2016. № 2–3. C. 73–86. 10. Мykola S. Nikitchenko and Stepan S. Shkilniak. Algebras and logics of partial quasiary predicates. Algebra and Discrete Mathematics, Volume 23 (2017). Number 2, P. 263–278. 11. Ivanov I., Nikitchenko M. On the sequence rule for the Floyd-Hoare logic with partial pre- and post-conditions. In Proceedings of the 14 th International Conference on ICT. 2018. Vol. 2104 of CEUR Workshop Proc. P. 716–724. 12. Клини С. Математическая логика. М.: Мир, 1973. 480 с. 13. Kleene S.C. Introductions to Metamathemat- ics. Van Nostrand, Princeton, 1952. 14. Нікітченко М.С., Шкільняк О.С., Шкільняк С.С. Логіки загальних недетермінованих предикатів: семантичні аспекти. Проблеми програмування. 2018. № 2–3. C. 31–45. References 1. Abramsky S., Gabbay D. and Maibaum T. (editors). (1993–2000). Handbook of Logic in Computer Science Oxford University Press, Vol. 1–5. 2. Avron A. and Zamansky A. (2011). Non- deterministic semantics for logical systems. In Handbook of Philosophical Logic, D.M. Gabbay, F. Guenthner (eds.), 2nd ed., Vol. 16, Springer Netherlands. P. 227–304. 3. Gries D. and Schneider F. (1995). Avoiding the undefined by underspecification. Springer Berlin Heidelberg. 4. Hähnle R. (2005). Many-valued logic, partiality, and abstraction in formal specification languages. In Logic Journal of the IGPL, 13. P. 415–433. 5. Jones C. (2006). Reasoning about partial functions in the formal development of programs. In Proceedings of AVoCS’05. Vol. 145. Elsevier, Electronic Notes in Theoretical Computer Science. P. 3–25. 6. Nikitchenko M. and Shkilniak S. (2008). Mathematical logic and theory of algorithms. Кyiv: VPC Кyivskyi Universytet (in ukr). 7. Nikitchenko M. and Shkilniak S. (2013). Applied logic. Кyiv: VPC Кyivskyi Universytet (in ukr). 8. Nikitchenko M. and Shkilniak S. (2015). Semantic Properties of Logics of Quasiary Predicates. In Workshop on Foundations of Теоретичні та методологічні основи програмування 13 Informatics: Proceedings FOI-2015. Chisinau, Moldova. P. 180–197. 9. 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). 10. Nikitchenko M. and Shkilniak S. (2017). Algebras and logics of partial quasiary predicates. In Algebra and Discrete Mathematics. Vol. 23. N 2. P. 263–278. 11. Ivanov I. and Nikitchenko M. (2018). On the sequence rule for the Floyd-Hoare logic with partial pre- and post-conditions. In Proceedings of the 14 th International Conference on ICT. Vol. 2104 of CEUR Workshop Proc. P. 716–724. 12. Kleene S. (1973) Mathematical Logic. Moscow: Mir (in rus). 13. Kleene S. (1952) Introductions to Metamathematics. Van Nostrand, Princeton. 14. Nikitchenko M., Shkilniak O. and Shkilniak S. (2018). Logics of general non-deterministic predicates: semantic aspects. In Problems in Progamming. N 2–3. P. 31–45 (in ukr). Одержано 07.02.2019 Про авторів: Нікітченко Микола Степанович, доктор фізико-математичних наук, професор, завідувач кафедри Теорії та технології програмування. Кількість наукових публікацій в українських виданнях – понад 250, у тому числі у фахових виданнях – понад 110. Кількість наукових публікацій в зарубіжних виданнях – понад 60. Scopus Author ID: 6602842336. h-індекс (Google Scholar): 13 (11 з 2014). http://orcid.org/0000-0002-4078-1062. Шкільняк Оксана Степанівна, кандидат фізико-математичних наук, доцент, доцент кафедри інформаційних систем. Кількість наукових публікацій в українських виданнях – понад 90, у тому числі у фахових виданнях – 35. Кількість наукових публікацій в зарубіжних виданнях – 12. Scopus Author ID: 57190873266 h-індекс (Google Scholar): 5 (4 з 2014) http://orcid.org/0000-0003-4139-2525. Шкільняк Степан Степанович, доктор фізико-математичних наук, професор, професор кафедри Теорії та технології програмування. Кількість наукових публікацій в українських виданнях – понад 240, у тому числі у фахових виданнях – понад 100. Кількість наукових публікацій в зарубіжних виданнях – 22. Scopus Author ID: 36646762300 h-індекс (Google Scholar): 7 (5 з 2014). http://orcid.org/0000-0001-8624-5778. Мамедов Тогрул Алірзайович, аспірант кафедри Теорії та технології програмування. Кількість наукових публікацій в українських виданнях – 9. http://orcid.org/0000-0002-6049-604X Місце роботи авторів: Київський національний університет імені Тараса Шевченка, 01601, Київ, вул. Володимирська, 60. Тел.: (044) 259 05 19. E-mail: me.oksana@gmail.com http://orcid.org/0000-0001%20-8624-5778

Propositional logics of partial predicates with composition of predicate complement

Репозитарії

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