Composition-nominative logics of free-quantifier levels

Composition-nominative logics of free-quantifier levels

Free-quantifier composition nominative logics of partial quasiary predicates are considered. We specify the following levels of these logics: renominative, renominative with predicates of weak equality, renominative with predicates of strong equality, free-quantifier, free-quantifier with compositio...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2018
Автори: Shkilniak, S.S., Volkovytskyi, D.B.
Формат: Стаття
Мова:Ukrainian
Опубліковано: Інститут програмних систем НАН України 2018
Теми:
free-quantifier logic
predicate
renomination
superposition
equality
logical consequence
UDC 004.42:510.69
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/180
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-180
record_format ojs
resource_txt_mv ppisoftskievua/e3/ea054125d5ef94465458dffe32175fe3.pdf
spelling pp_isofts_kiev_ua-article-1802024-04-28T13:09:55Z Composition-nominative logics of free-quantifier levels Композиционно-номинативные логики безкванторних уровней Композиційно-номінативні логіки безкванторних рівнів Shkilniak, S.S. Volkovytskyi, D.B. free-quantifier logic; predicate; renomination; superposition; equality; logical consequence UDC 004.42:510.69 Ключевые слова: бескванторная логика; предикат; реноминация; суперпозиция; равенство; логическое следствие УДК 004.42:510.69 безкванторна логіка; предикат; реномінація; суперпозиція; рівність; логічний наслідок УДК 004.42:510.69 Free-quantifier composition nominative logics of partial quasiary predicates are considered. We specify the following levels of these logics: renominative, renominative with predicates of weak equality, renominative with predicates of strong equality, free-quantifier, free-quantifier with composition of weak equality, free-quantifier with composition of strong equality. The paper is mainly dedicated to investigation ofNlogics of free-quantifier levels with equality. Languages and semantic models of such logics are described, their semantic properties are studied, in particular the properties of relations of logical consequence.Problems in programming 2016; 2-3: 38-47 Исследованы бескванторные композиционно-номинативные логики частичных квазиарных предикатов. Выделены такие уровни этих логик: реноминативный, реноминативный с предикатами слабого равенства, реноминативный с предикатами строгого равенства, бескванторно-функциональный, бескванторно-функциональный с композицией слабого равенства, бескванторно-функциональный с композицией строгого равенства. Основное внимание уделено логикам бескванторно-функциональных уровней с равенством. Описаны язики и семантические модели бескванторных логик, исследованы их семантические свойства, в частности, свойства отношений логического следствия для множеств формул.Problems in programming 2016; 2-3: 38-47 Досліджено безкванторні композиційно-номінативні логіки часткових квазіарних предикатів. Виділено такі рівні цих логік: реномінативний, реномінативний з предикатами слабкої рівності, реномінативний з предикатами строгої рівності, безкванторно-функціональний, безкванторно-функціональний з композицією слабкої рівності, безкванторно-функціональний з композицією строгої рівності. Основна увага приділена логікам безкванторно-функціональних рівнів з рівністю. Описано мови та семантичні моделі безкванторних логік, досліджено їх семантичні властивості, зокрема, властивості відношень логічного наслідку для множин формул.Problems in programming 2016; 2-3: 38-47 Інститут програмних систем НАН України 2018-07-06 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/180 10.15407/pp2016.02-03.038 PROBLEMS IN PROGRAMMING; No 2-3 (2016); 38-47 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2016); 38-47 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2016); 38-47 1727-4907 10.15407/pp2016.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/180/175 Copyright (c) 2017 ПРОБЛЕМИ ПРОГРАМУВАННЯ
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2024-04-28T13:09:55Z
collection OJS
language Ukrainian
topic free-quantifier logic
predicate
renomination
superposition
equality
logical consequence
UDC 004.42:510.69
spellingShingle free-quantifier logic
predicate
renomination
superposition
equality
logical consequence
UDC 004.42:510.69
Shkilniak, S.S.
Volkovytskyi, D.B.
Composition-nominative logics of free-quantifier levels
topic_facet free-quantifier logic
predicate
renomination
superposition
equality
logical consequence
UDC 004.42:510.69
Ключевые слова: бескванторная логика
предикат
реноминация
суперпозиция
равенство
логическое следствие
УДК 004.42:510.69
безкванторна логіка
предикат
реномінація
суперпозиція
рівність
логічний наслідок
УДК 004.42:510.69
format Article
author Shkilniak, S.S.
Volkovytskyi, D.B.
author_facet Shkilniak, S.S.
Volkovytskyi, D.B.
author_sort Shkilniak, S.S.
title Composition-nominative logics of free-quantifier levels
title_short Composition-nominative logics of free-quantifier levels
title_full Composition-nominative logics of free-quantifier levels
title_fullStr Composition-nominative logics of free-quantifier levels
title_full_unstemmed Composition-nominative logics of free-quantifier levels
title_sort composition-nominative logics of free-quantifier levels
title_alt Композиционно-номинативные логики безкванторних уровней
Композиційно-номінативні логіки безкванторних рівнів
description Free-quantifier composition nominative logics of partial quasiary predicates are considered. We specify the following levels of these logics: renominative, renominative with predicates of weak equality, renominative with predicates of strong equality, free-quantifier, free-quantifier with composition of weak equality, free-quantifier with composition of strong equality. The paper is mainly dedicated to investigation ofNlogics of free-quantifier levels with equality. Languages and semantic models of such logics are described, their semantic properties are studied, in particular the properties of relations of logical consequence.Problems in programming 2016; 2-3: 38-47
publisher Інститут програмних систем НАН України
publishDate 2018
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/180
work_keys_str_mv AT shkilniakss compositionnominativelogicsoffreequantifierlevels
AT volkovytskyidb compositionnominativelogicsoffreequantifierlevels
AT shkilniakss kompozicionnonominativnyelogikibezkvantornihurovnej
AT volkovytskyidb kompozicionnonominativnyelogikibezkvantornihurovnej
AT shkilniakss kompozicíjnonomínativnílogíkibezkvantornihrívnív
AT volkovytskyidb kompozicíjnonomínativnílogíkibezkvantornihrívnív
first_indexed 2024-09-16T04:07:30Z
last_indexed 2024-09-16T04:07:30Z
_version_ 1818568148629061632
fulltext Теоретичні та методологічні основи програмування © С.С. Шкільняк, Д.Б. Волковицький, 2016 48 ISSN 1727-4907. Проблеми програмування. 2016. № 2–3. Спеціальний випуск 004.42:510.69 КОМПОЗИЦІЙНО-НОМІНАТИВНІ ЛОГІКИ БЕЗКВАНТОРНИХ РІВНІВ С.С. Шкільняк, Д.Б. Волковицький Досліджено безкванторні композиційно-номінативні логіки часткових квазіарних предикатів. Виділено такі рівні цих логік: реномі- нативний, реномінативний з предикатами слабкої рівності, реномінативний з предикатами строгої рівності, безкванторно-функціо- нальний, безкванторно-функціональний з композицією слабкої рівності, безкванторно-функціональний з композицією строгої рів- ності. Основна увага приділена логікам безкванторно-функціональних рівнів з рівністю. Описано мови та семантичні моделі без- кванторних логік, досліджено їх семантичні властивості, зокрема, властивості відношень логічного наслідку для множин формул. Ключові слова: безкванторна логіка, предикат, реномінація, суперпозиція, рівність, логічний наслідок. Исследованы бескванторные композиционно-номинативные логики частичных квазиарных предикатов. Выделены такие уровни этих логик: реноминативный, реноминативный с предикатами слабого равенства, реноминативный с предикатами строгого равен- ства, бескванторно-функциональный, бескванторно-функциональный с композицией слабого равенства, бескванторно-функцио- нальный с композицией строгого равенства. Основное внимание уделено логикам бескванторно-функциональных уровней с равен- ством. Описаны язики и семантические модели бескванторных логик, исследованы их семантические свойства, в частности, свойс- тва отношений логического следствия для множеств формул. Ключевые слова: бескванторная логика, предикат, реноминация, суперпозиция, равенство, логическое следствие. Free-quantifier composition nominative logics of partial quasiary predicates are considered. We specify the following levels of these logics: renominative, renominative with predicates of weak equality, renominative with predicates of strong equality, free-quantifier, free-quantifier with composition of weak equality, free-quantifier with composition of strong equality. The paper is mainly dedicated to investigation of logics of free-quantifier levels with equality. Languages and semantic models of such logics are described, their semantic properties are studied, in particular the properties of relations of logical consequence. Key words: free-quantifier logic, predicate, renomination, superposition, equality, logical consequence. Вступ Апарат математичної логіки є основою сучасних інформаційних і програмних систем, він належить до основних засобів моделювання предметних областей. Для цього зазвичай використовується класична логіка предикатів та базовані на її основі спеціальні логіки (модальні, темпоральні, епістемічні, динамічні, програмні тощо). Водночас класична логіка має (див. [1, 2]) низку обмежень, вона недостатньо враховує неповноту, част- ковість, структурованість інформації про предметну область. Це значною мірою ускладнює її використання при розв’язанні задач інформатики й програмування. Таким чином, постає проблема побудови нових логічних фор- малізмів, більше орієнтованих на потреби програмування й моделювання. Концептуальною основою такої по- будови є спільний для логіки й програмування композиційно-номінативний підхід. Логіки, збудовані на його основі, названо композиційно-номінативними (КНЛ). Такі логіки базуються на класах часткових квазіарних відображень, що задаються на номінативних (іменних) даних. Метою даної роботи є дослідження нових класів КНЛ – безкванторних логік квазіарних предикатів. Такі логіки посідають проміжне становище між пропозиційною та першопорядковими логіками, в них немає компо- зицій квантифікації, характерних для першопорядкових логік. Описано рівні безкванторних логік, розглянуто їх семантичні моделі та мови, досліджено семантичні властивості. Описано композиції суперпозиції та слабкої і строгої рівності, розглянуто нормальні форми термів та формул, наведено властивості відношень логічного на- слідку для множин формул. Такі властивості є семантичною основою побудови для різних класів безквантор- них логік числень секвенційного типу. Можна виділити такі рівні безкванторних логік квазіарних предикатів: – реномінативний (РНЛ); – реномінативний з предикатами слабкої рівності (РНЛР); – реномінативний з предикатами строгої рівності (РНЛРС); – безкванторно-функціональний (БКФЛ); – безкванторно-функціональний з композицією слабкої рівності (БКФЛР); – безкванторно-функціональний з композицією строгої рівності (БКФЛРС). Найабстрактнішим з цих рівнів є реномінативний. Реномінативні логіки добре досліджені (див. [1–3]). Вивчення реномінативних логік з рівністю та безкванторно-функціональних логік започатковано в [4. 5], во- но продовжено в даній роботі, особлива увага приділена логікам безкванторно-функціонального рівня з рів- ністю. В цій роботі будемо вважати, що функції та предикати – часткові однозначні. Поняття, які в роботі не визначаються, тлумачимо в сенсі [1, 2]. Нагадаємо основні визначення. V-A-іменна множина (V-A-ІМ) – це однозначна функція d : VA. Множину всіх V-A-ІМ позначаємо V A. Функцію asn : V A  V2 вводимо так: asn(d) = {vV | vad для деякого Aa }. Теоретичні та методологічні основи програмування 49 Для V-A-ІМ операцію Х|| , де VX  , задаємо так: }{ Xd | vav d || Х   . Операцію  накладки V-A-ІМ h на V-A-ІМ d визначаємо так: ( )|| asn hd h d h   . Операцію реномінації 1 1 ,..., ,..., r :n n v v x x V А V A задаємо так: 1 1 ,..., ,..., r ( )n n v v x x d  d  [v1d(x1),...,vnd(xn)]. Замість y1,..., yn зазвичай будемо скорочено писати y . Тоді замість 1 1 ,..., ,..., r n n v v x x також пишемо r v x . Функції вигляду V AА назвемо V-А-квазіарними функціями. Клас цих функцій позначимо AFn . Функції вигляду V A{T, F} назвемо V-А-квазіарними предикатами. Клас цих предикатів позначимо APr . Область істинності та область хибності V-А-квазіарного предиката P – це множини )(PT = {d V А | P(d) = T} та )(PF = {d V А | FdP )( }. Предикат P : V А  {T, F} назвемо:  неспростовним (частково істинним), якщо )(PF ;  тотожно істинним, якщо )(PT V А та )(PF ;  виконуваним, якщо )(PT ;  всюди невизначеним, якщо )(PT )(PF . Предикат P : V А },{ FT еквітонний (монотонний), якщо: )(dP та )()( dPdPdd  . Предметне ім’я Vx неістотне для квазіарнoї функції (предиката) g , якщо )()( 2121 dgdg||d||d xx   . 1. Композиційні системи логік реномінативних та безкванторно-функціональних рівнів Семантичною основою КНЛ є композиційні предикатні системи. Для реномінативних логік такі системи мають вигляд ( V А, APr , C ), для безкванторно-функціональних – ( V А А, AFn  APr , C ). Тут AFn та APr – це множини V-А-квазіарних функцій та V-А-квазіарних предикатів, C – множина композицій відповідного рівня. Будемо розглядати КНЛ, розширені шляхом виділення підмножини VU  тотально неістотних пред- метних імен (неістотних для всіх базових функцій та предикатів). Будемо вважати, що така U розв’язна від- носно V . На рівні РНЛ можна перейменовувати компоненти вхідних даних, що дає змогу ввести композицію рено- мінації. Базовими композиціями РНЛ є логічні зв’язки ,  та реномінація Rv x . Композиція Rv x : APr  APr визначається так: для кожного d V А маємо R ( )( ) (r ( ))v v x xP d P d . Дамо визначення логічних зв’язок  та  через області істинності й хибності відповідних предикатів: T(P) = F(P); F(P) = T(P); T(PQ) = T(P)T(Q); F(PQ) = F(P)F(Q); Подібним чином можна визначити похідні логічні зв’язки , &,  (див. [1]). На рівнях РНЛР та РНЛРС можна ототожнювати й розрізняти значення предметних імен за допом о- гою спеціальних 0-арних композицій – параметризованих за іменами предикатів рівності. Можна розгляда- ти дві різновидності цих предикатів: слабкої (з точністю до визначеності) рівності xy та строгої (точної) рівності xy . Предикати xy та xy задаються їх областями істинності й хибності наступним чином: T( xy ) = {d V A | d(x), d(y) та d(x) = d(y)}, F( xy ) = {d V A | d(x), d(y) та d(x)  d(y)}; T( xy ) = {d V A | d(x), d(y) та d(x) = d(y)}  {d V A | d(x) та d(y)}, Теоретичні та методологічні основи програмування 50 F( xy ) = {d V A | d(x), d(y) та d(x)  d(y)}  {d V A | d(x), d(y) або d(x), d(y)}. Предикати xy є частковими еквітонними, предикати xy тотальні немонотонні (нееквітонні). Базовими композиціями РНЛР є , , R ,v x =ху. Базовими композиціями РНЛРС є , , R ,v x ху. На функціональних рівнях можна формувати нові базові значення для вхідних даних. Це дає змогу ввес- ти композицію суперпозиції. Нехай F А – клас квазіарних функцій вигляду f : V AR. Параметрична (n+1)-арна композиція суперпозиції 1,... S : ( )nv v A A n AF Fn F  визначається так. Для кожного d V А задаємо 1,... 1S ( , ,..., )( )nv v nf g g d  1 1( [ ( ),..., ( )])n nf d v g d v g d . Розглядатимемо суперпозиції двох типів: – суперпозиції вигляду AnA FnFn 1)( функцій у функції (результатом є функція); – суперпозиції вигляду APr  nAFn )( APr функцій у предикати (результатом є предикат). Для роботи з окремими компонентами даних доцільно ввести спеціальні 0-арні композиції – функції де- номінації (розіменування) 'v, де vV. Ці функції задаємо так: 'v(d) = d(v). При наявності функцій деномінації композиції реномінації можна промоделювати за допомогою компо- зицій суперпозиції: для кожної AFnf   APr маємо 1 1 1 ,..., ,..., 1,..., R ( ) S ( , v ,..., v )n n n u u u u nv v f f ' ' . Отримуємо рівень безкванторно-функціональних логік – БКФЛ. Базові композиції БКФЛ: , , S ,x 'v. На функціональних рівнях з рівністю можна ототожнювати й розрізняти предметні значення, що дає змогу ввести спеціальну композицію рівності. Розглядаємо дві її різновидності: слабкої (з точністю до ви- значеності) рівності  та строгої (точної) рівності  . Ці композиції задаються так. Для кожних AFngf , та d V А маємо: = , якщо ( ) , ( ) , ( ) ( ), ( , )( ) , якщо ( ) , ( ) , ( ) ( ), невизначене, якщо ( ) або ( ) ; T f d g d f d g d f g d F f d g d f d g d f d g d             , якщо ( ) , ( ) , ( ) ( ) або ( ) , ( ) ; ( , )( ) , якщо ( ) , ( ) , ( ) ( ) або ( ) , ( ) або ( ) , ( ) . T f d g d f d g d f d g d f g d F f d g d f d g d f d g d f d g d               Отже, композиція  в усіх випадках має результатом тотальний предикат. На функціональних рівнях з рівністю наявність функцій розіменування є цілком природною. Таким чином, отримуємо рівні БКФЛР та БКФЛРС безкванторно-функціональних логік з рівністю. Базові композиції БКФЛР: , , S ,x 'v,  . Базові композиції БКФЛРС: , , S ,x 'v,  . Властивості композицій реномінації та предикатів рівності розглянуто в [1, 2, 4]. Опишемо властивості композицій суперпозиції та рівності Теорема 1. Композиції Sv та  зберігають тотальність та еквітонність (монотонність) V-A-квазіарних функцій і предикатів; водночас композиція  еквітонність не зберігає. Таким чином, на рівні БКФЛРС логіки еквітонних предикатів не розглядаємо. Розглянемо основні властивості композицій суперпозиції. S) Дистрибутивність суперпозиції щодо : S ( , ) S ( , )v vP f P f  . S) Дистрибутивність суперпозиції щодо : S ( , ) S ( , ) S ( , )v v vP Q f P f Q f   . SS) Згортка суперпозицій: (тут  AA PrFn  та введені позначення: u для nuu ,...,1 ; t для ntt ,...,1 ; x для kxx ,...,1 ; r для krr ,...,1 ; w для kww ,...,1 ; v для mvv ,...,1 ; s для mss ,...,1 ): Теоретичні та методологічні основи програмування 51 , , , , , 1S (S ( , , ), , ) S ( , ,S ( , , ),u x x v u x v u xr s t w t r t w   , , , 1...,S ( , , ),S ( , , ),...,S ( , , ))u x u x u x k mr t w s t w s t w . CN) Згортка імен (тут  AA PrFn  ): 1,..., , 1S ( , x ,..., x , ) S ( , )mx x v v m' ' g g   ; зокрема, 1,..., 1S ( , x ,..., x )mx x m' '   . SD) Згорткa неістотних імен для функцій 'x: S (x, ) x за умови { }v ' g ' x v  . SF) Cпрощення для функцій 'x: ,S (x, , )x v ' f g f ; зокрема, S (x, )x ' f f . CU) Згортка за неістотним іменем (тут  AA PrFn  ): за умови x неістотне для  маємо ,S ( , , ) S ( ,, )x v vf g g   , зокрема, S ( , )x f   . Зауважимо, що властивості SS, CN, CU формулюються для квазіарних функцій та предикатів, а власти- вості SD, SF – лише для квазіарних функцій. Укажемо основні властивості композицій рівності. Вважаємо, що APrP та nn gggfffh ,...,,,,...,,, 11  AFn . Rf) (рефлективність) кожний предикат вигляду ),( ff є неспростовним; кожний предикат вигляду ),( ff є тотожно істинним. Sm) (симетричність) для кожного d V A маємо  ))(,( dgf ))(,( dfg та  ))(,( dgf ))(,( dfg ; це означає, що предикати ),( gf і ),( fg рівні та предикати ),( gf і ),( fg рівні; Tr) (транзитивність) для кожного d V A маємо: якщо Tdgf  ))(,( та Tdhg  ))(,( , то Tdhf  ))(,( ; якщо Tdgf  ))(,( та Tdhg  ))(,( , то Tdhf  ))(,( . Як наслідок маємо: кожний предикат вигляду ),( gf & ),( hg  ),( hf неспростовний; кожний предикат вигляду ),( gf & ),( hg  ),( hf тотожно істинний (адже він тотальний). Твердження 1. Якщо ),( gf та ),( hg тотожно істинні, то ),( hf тотожно істинний. Водночас для композиції  аналогічне твердження невірне. Приклад. Якщо ),( gf та ),( hg неспростовні, то ),( hf може бути спростовним. Справді, візьмемо )()( dhdf  для деякого d V A, та нехай функція g – всюди невизначена. Наведемо властивості, пов’язані з заміною рівних. EF) кожний предикат вигляду ),( gf  = , ,(S ( , , ), S ( , , ))z v z vh f r h g r є неспростовним; кожний предикат вигляду ),( gf   , ,(S ( , , ), S ( , , ))z v z vh f r h g r є тотожно істинним; EP) кожний предикат вигляду ),( gf  , ,(S ( , , ) S ( , , ))z v z vP f r P g r є неспростовним; кожний предикат вигляду ),( gf  , ,(S ( , , ) S ( , , ))z v z vP f r P g r є неспростовним. Дистрибутивність суперпозиції щодо рівності: SЕ) S (v = ( , ), )f g r = = (S ( , ), S ( , ))v vf r g r ; S (v  ( , ), )f g r =  (S ( , ), S ( , ))v vf r g r . 2. Мови логік безкванторно-функціональних рівнів. Відношення логічного наслідку На безкванторно-функціональних рівнях композиційна система (А, CPrFn AA , ) визначає композицій- ну алгебру квазіарних функцій і предикатів ( CPrFn AA , ) та алгебру (алгебраїчну систему) даних (А, AA PrFn  ). Побудова композиційної алгебри дає змогу визначити мову логіки: терми такої алгебри є фор- мулами мови. Теоретичні та методологічні основи програмування 52 Опишемо мову БКФЛ. Алфавіт мови: множини предметних імен (змінних) V та тотально неістотних імен U  V; множина Dns = {'v | vV} деномінаційних символів (ДНС) – імен функцій розіменування; множини Fns та Ps функціональних (ФНС) та предикатних (ПС) символів; множина {, , ,vS 'v} символів базових композицій. Множину  = FnsPs назвемо сигнaтурою мови. Множини термів Тr і формул Fr вводимо так. Т0) Кожний ФНС та кожний ДНС є термом, такі терми – атомарні. Т1) Нехай , 1,..., nt t Tr ; тоді 1,... 1...nv v nS t t Tr  . Ф0) Кожний ПС є формулою (атомарною), такі формули – атомарні. Ф1) Нехай , Fr, 1,..., nt t Tr ; тоді 1,... 1...nv v nS t t Fr  , Fr, Fr. При зафіксованій множині базових композицій мови БКФЛ істотно відрізняються сигнaтурами. Неістот- ні відмінності – це способи запису термів і формул. Ми використовуємо префіксну форму. Для бінарних композицій зазвичай використовують не префіксну, а інфіксну форму (див. [1]), коли сим- вол композиції записується між аргументами. Надалі вживаємо інфіксну форму та допоміжні символи – коми й дужки "(" і ")", а також символи похідних композицій &, , . Не пишемо зайвих дужок, вводячи пріоритет символів композицій: ,vS , &, , , . Подібні скорочені записи також називатимемо термами і формулами. У випадку БКФЛР множина базових композицій {, , ,vS 'v, =}. Визначення множини Тr термів таке ж, як для мови БКФЛ. Індуктивне визначення множини Fr формул задається пп. Ф0, Ф1, до якого додаємо: ФЕ) t, s Tr  =ts Fr . У випадку БКФЛРС множина базових композицій {, , S ,x 'v, }. Визначення множини Тr термів таке ж, як для мови БКФЛ. Індуктивне визначення множини Fr формул задається пп. Ф0, Ф1, до якого додаємо: ФЕS) t, s Tr  ts Fr . Замість =ts та ts також писатимемо t = s та t  s. Інтерпретуємо мови БКФЛ, БКФЛР, БКФЛРС на відповідних композиційних системах квазіарних функ- цій та предикатів. Символи сигнатури  = FnsPs позначають (виділяють) базові функції та базові предикати в множинах AFn та APr , символи 'v позначають відповідні функції деномінації 'v. Для такого позначення задає- мо тотальне однозначне відображення I : DnsFnsPs  AA PrFn  . При цьому I('v) = 'v для кожного 'vDns, кожне zU неістотне для кожного gI(). Далі продовжимо I до відображення інтерпретації I : TrFr AA PrFn  згідно побудови термів та формул із простіших за допомогою символів композицій: ІТ) 1 1,... ,... 1 1( ... ) S ( ( ), ( ),..., ( ))n nv v v v n nI S t t I I t I t   ; І) 1 1,... ,... 1 1( ... ) S ( ( ), ( ),..., ( ))n nv v v v n nI S t t I I t I t   ; I() = (I()), I() = (I(), I()). У випадках мови БКФЛР та мови БКФЛРС відповідно додаємо: IЕ) I(t = s =ts) = =(I(t), I(s)). IS) I(t  s) = (I(t), I(s)). Трійку J = (CS, , I) назвемо інтерпретацією мови БКФЛ (БКФЛР, БКФЛРС) сигнатури . Cкорочено інтерпретації мови також позначаємо як (A, , I) чи (A, I). Функцію I(t), яка є значенням терма t при інтерпретації J, позначаємо Jt . Предикат I(), який є значенням формули  при інтерпретації J, позначаємо J . Ім’я xV неістотне для термa t, якщо при кожній інтерпретації J ім’я x неістотне для функції Jt . Ім’я xV неістотне для формули , якщо при кожній інтерпретації J ім’я x неістотне для предиката J . Формула  виконувана при інтерпретації J, якщо предикат J – виконуваний. Формула  виконувана, якщо  виконувана при деякій інтерпретації J. Формула  неспростовна (частково істинна) при інтерпретації J, що позначаємо J |= , якщо предикат J – неспростовний. Формула  неспростовна, що позначаємо |= , якщо J |=  при кожній інтерпретації J. Теоретичні та методологічні основи програмування 53 Формула  тотожно істинна при інтерпретації J, що позначаємо J id , якщо предикат J – тотожно істинний. Формула  тотожно істинна, що позначаємо id , якщо J id при кожній інтерпретації J. Поняття тотожно істинної формули змістовне лише для БКФЛРС, тому що їх побудова неможлива без використання  . Зокрема, id t  t та id t  s  s  t. Водночас: Твердження 2. У випадках БКФЛ та БКФЛР множина тотожно істинних формул порожня. Справді, розглянемо таку інтерпретацію J, на якій кожний ПС інтерпретується як всюди невизначений предикат, а кожний ФНС інтерпретується як всюди невизначена функція. На множині формул можна ввести [2, 6] низку відношень логічного наслідку. Спочатку задаємо відно- шення наслідку між двома множинами формул при фіксованій інтерпретації J. Нехай  Fr,   Fr. Введемо позначення ( )JT   як T(J), ( )JF   як FJ), ( )JT   як T(J), ( )JF   як F(J).  є IR-наслідком  при J (позн.  IDJ  ), якщо T(J)  F (J) = .  є T-наслідком  при J (позн.  TJ ), якщо T(J)  T (J).  є F-наслідком  при J (позн.  FJ ), якщо F(J)  F (J).  є TF-наслідком  при J (позн.  TFJ ), якщо T(J)  T (J) та F(J)  F (J). Відповідні відношення логічного наслідку визначаємо за схемою:  * , якщо  *J для кожної J. Твердження 3. Маємо такі співвідношення: FTTF  ; IRTTF  , IRFTF  . Окремим випадком розглянутих відношень для множин формул є відповідні відношення для пари фор- мул: відношення наслідку при фіксованій J та відношення логічного наслідку; для них вводимо традиційні поз- начення  *J та  *J , де , Fr. Відношення логічного наслідку для пари формул індукують відношення логічної еквівалентності. Відношення еквівалентності при інтерпретації J визначаємо за схемою:  J , якщо  *J та  *J . Відношення логічної еквівалентності IR, T, F, TF визначаємо за схемою:   , якщо  * та  * . Із визначень випливає:      J  для кожної інтерпретації J. Властивості описаних вище відношень вивчались в [1, 2]. Зокрема, зазначимо, що відношення логічного наслідку для пар формул рефлексивні й транзитивні; відношення логічної еквівалентності рефлексивні, тран- зитивні й симетричні; відношення логічного наслідку для множин рефлексивні та нетразитивні. Особливу роль мають відношення IR  та IR , вони традиційно позначаються [1] як  та  . Це пов’язано з тим фактом, що логічні зв’язки  та  узгоджуються з відношеннями IR  та IR :  IR    ;  IR   |=  . Важливим є також відношення J TF :  JTF   )()( JJ TT  та )()( JJ FF   JJ  . Розглянемо співвідношення між id і  TF та між id і  TF . Для БКФЛ та БКФЛР множина тотожно істинних формул порожня (твердження 2), проте для БКФЛРС це питання нетривіальне. Теорема 2. 1) id   TF , водночас зворотне невірне; 2) id   TF , водночас зворотне невірне. Доводимо п. 1. id  для кожних J = (A, I) маємо )()( JJ TF  = V A. Звідси, враховуючи Теоретичні та методологічні основи програмування 54 диз’юнктність множини та її доповнення, із )()( JJ TF  = V A, маємо ( ) ( )J JT F   та ( ) ( )J JF T   . Враховуючи )()( JJ TF  =  та )()( JJ TF  = , отримуємо ( ) ( )J JF T   та ( ) ( )J JT F   . Звідси ( ) ( )J JF F   та )()( JJ TT  , що дає  TFJ . Це вірно для кожної J, звідки  TF . Отже,  TFid . Водночас зворотне невірне: завжди маємо  TF , проте id вимагає, щоб для кожної J преди- кат J , тобто  J , був тотальним, звідки для кожної J предикат J має бути тотальним. Така ситу- ація можлива для БКФЛРС, проте неможлива для БКФЛ та БКФЛР. Доводимо п. 2. id для кожних J = (A, I) та d V A маємо TdJ  )()(  для кожних J = (A, I) та d V A маємо  )()( dd JJ . Тепер  TF   для кожних J = (A, I) та d V A маємо  )()( dd JJ або  )(dJ та )(dJ . Отже, id  TF . Водночас зворотне невірне: завжди  TF , проте id вимагає тотальності предиката  J для кожної J. Це можливо для БКФЛРС, не- можливо для БКФЛ і БКФЛР. 3. Семантичні властивості логік безкванторно-функціональних рівнів Виділення тим чи іншим способом (див. [1, 2]) множини U  V тотально неістотних предметних імен дає змогу визначити для кожного терма чи формули  множину () імен, які гарантовано неістотні. Для кожного gFnsPs маємо (g) = U. Для кожного 'xDns задамо ('x) = V\{x}. Далі задаємо: 1,... 1( ... )nx x nS t t  =((){x1,..., xn}) { | ( )} ( ) i i i v t    ; 1,... 1( ... )nx x nS t t  = ((){x1,..., xn}) { | ( )} ( ) i i i v t    ; (t = s) = (t)(s); (t  s) = (t)(s); () = (Ф); () = ()(). Теорема 3 (див. [1]). х()  х неістотне для термa ; х()  х неістотне для формули . Семантичні властивості формул індуковані відповідними властивостями композицій та записуються ана- логічно, але замість рівності предикатів фігурує строга еквівалентність формул, які позначають ці предикати. S) ( , ) ( , )v v TFS t S t   ; S) ( , ) ( , ) ( , )v v v TFS t S t S t    . SSФ) Згортка суперпозицій для формул (тут позначення: u для nuu ,...,1 ; t для ntt ,...,1 ; x для kxx ,...,1 ; r для krr ,...,1 ; w для kww ,...,1 ; v для mvv ,...,1 ; s для mss ,...,1 ): , , , , , 1( ( , , ), , ) ( , , ( , , ),u x x v u x v u x TFS S r s t w S t S r t w  , , , 1..., ( , , ), ( , , ),..., ( , , ))u x u x u x k mS r t w S s t w S s t w . CNФ) Згортка імен для формул: , ( , , ) ( , )x v v TFS 'x t S t  ; зокрема, ( , )x TFS 'x  . СUФ) Згортка за неістотним іменем для формул: , ( , , ) ( , )x v v TFS s t S t  , якщо x неістотне для ; зокрема, ( , )x TFS t  , якщо x неістотне для  . Властивості SS, CN, CU для функцій та властивості SD, SF, які формулюються лише для функцій, у ви- падку БКФЛ індукують відповідні властивості нормалізації термів у формулах, які подаємо у вигляді ї теореми: Теорема 4. Нехай формула  отримана з формули  заміною деяких входжень термів: rpSS) , ,( ( , , ), , )u x x vS S r s t w на , , , 1( , , ( , , ),u x v u xS t S r t w , , , 1..., ( , , ), ( , , ),..., ( , , ));u x u x u x k mS r t w S s t w S s t w rpCN) , ( , , ) на ( , )x v vS 'x t S t  , зокрема, ( , ) на xS 'x  ; rpCU) , ( , , )x vS t t на ( , )vS t , якщо x неістотне для ; зокрема, ( , ) на xS t  , якщо x неістотне для . rpSD) ( , )vS 'x t на 'x за умови { }x v ; rpSF) , ( , , )x vS 'x t на , зокрема, ( , ) на xS 'x   . Теоретичні та методологічні основи програмування 55 Тоді  TF  . Основою еквівалентних перетворень формул є теорема еквівалентності: Теорема 5. Нехай  отримано з формули  заміною деяких входжень n ,...,1 на n ,...,1 . 1) Якщо 1 TF ,...,1 n TF n , то    (тут  – одне з відношень T, F, TF, IR). 2) Якщо 1 IR ,...,1 n IR n , то  IR  . Для відношень T та F теорема 5 невірна (див. [2]). Для множин формул подібне твердження – це теорема заміни еквівалентних (  – одне з T  , F  , TF  , IR  ): Теорема 6. 1) Нехай  TF , тоді  ,  |=   ,  |=  та  |= ,   |= , . 2) Нехай  IR , тоді  ,  IR    ,  IR   та  IR  ,   IR  , . Властивості рівності. Спочатку розглянемо властивості, пов’язані з композицією слабкої рівності. RfW) tt  ; SmW) tsst  ; це можна подати так: st  IR ts  ; більше того, маємо st  TF ts  ; TrW) st  & rtrs  ; це можна подати так: st  , rs  IR  rt  ; EF) st   , ,( , , ) ( , , )v z v zS r t S r s   ; це можна подати так: st  IR  , ,( , , ) ( , , )v z v zS r t S r s   ; EP) st   , ,( ( , , ) ( , , ))v z v zS r t S r s   ; це можна подати так: st  IR  , ,( , , ) ( , , )v z v zS r t S r s   . SЕ) |= ( , ) ( , ) ( , )v v vS s r t S s t S r t   ; це можна подати так: ( , ) ( , ) ( , )v v v IRS s r t S s t S r t  . Властивості кроку нормалізації термів, індуковані властивостям SS, CN, CU, SD, SF для функцій: ST) , ,| ( ( , , ), , )u x x vS S r s t w  = , , , 1( , , ( , , ),u x v u xS t S r t w , , , 1..., ( , , ), ( , , ),..., ( , , ));u x u x u x k mS r t w S s t w S s t w CNT) ,| ( , , ) ( , )x v vS 'x t S t    ; зокрема, | ( , )xS 'x    ; CUT) за умови x неістотне для  маємо: ,| ( , , ) ( , )x v vS t t S t    , зокрема, | ( , )xS t    ; SDT) | ( , )vS 'x t 'x  , де { }x v ; SFT) ,| ( , , )x vS 'x t    ; зокрема, | ( , )xS 'x    . Наведемо властивості, пов’язані з композицією строгої рівнoсті. RfS) tt id  ; SmS) tsst id  ; TrS) st id  & rtrs  . Враховуючи, що st  та ts  завжди інтерпретуються як тотожні предикати, властивості SmS та TrS можна подати так: st  TF ts  ; st  , rs  TF  t  r . EFS) |=id t  s  , ,( , , ) ( , , )v z v zS r t S r s   ; це можна подати так: st  TF  , ,( , , ) ( , , )v z v zS r t S r s   . Подібну властивість для формул так подати неможливо, адже формула вигляду ( , ) ( , )x xS t S s   не завжди інтерпретується як тотальний предикат. Подібним способом можна записати лише ослаблену власти- вість  st   , ,( ( , , ) ( , , ))v z v zS r t S r s   , або st  IR  , ,( ( , , ) ( , , ))v z v zS r t S r s   Тому EPS формулюємо так: Теоретичні та методологічні основи програмування 56 EPSL) , ,, ( , , ) | ( , , )v z v z TFt s S r t S r s    . SЕS) id  ( , ) ( , ) ( , )v v vS s r t S s t S r t   ; це можна подати так: ( , ) ( , ) ( , )v v v TFS s r t S s t S r t  . Властивості кроку нормалізації термів, індуковані властивостями SS, CN, CU, SD, SF для функцій: STS) , ,| ( ( , , ), , )u x x v id S S r s t w   , , , 1( , , ( , , ),u x v u xS t S r t w , , , 1..., ( , , ), ( , , ),..., ( , , ));u x u x u x k mS r t w S s t w S s t w CNTS) ,| ( , , ) ( , )x v v id S 'x t S t    ; зокрема, | ( , )x id S 'x    ; CUTS) за умови x неістотне для  маємо: ,| ( , , ) ( , )x v v id S t t S t    , зокрема, | ( , )x id S t    ; SDS) | ( , )v id S 'x t 'x  , де { }x v ; SFS) ,| ( , , )x v id S 'x t    ; зокрема, | ( , )x id S 'x    . Тавтології. Введемо поняття тавтології для КНЛ безкванторно-функціональних рівнів. Формула мови БКФЛ (БКФЛР, БКФЛРС) пропозиційно нерозкладна, якщо вона атомарна або має вигляд vS t (вигляд vS t чи t = s, вигляд vS t чи t  s). Множину таких формул позначимо Fr0 Істиннiсна оцiнка мови РНЛ – це [1] довільне тотальне відображення  : Fr0  {T, F}. Таке відображення продовжимо до  : Fr  {T, F} так:  , якщо ( ) , ( ) , якщо ( ) ; T F F T           , якщо ( ) або ( ) , ( ) , якщо ( ) та ( ) . T T T F F F                Враховуючи Rf, Sm, Tr, EF, EP, у випадках БКФЛР та БКФЛРС на  накладаємо додаткові умови: (t = t) = T; (t = s) = (s = t); (t = s) = (s = r) = T  (t = r) = T; (t = s) = T  , ,( ( , , ) ( , , ))z v z vS t r S s r T     ; (t = s) = T  , ,( ( , , ) ( ( , , )z v z vS t r S s r     ; (х  х) = T; (х  y) = (y  х); (х  y) = (х  y) = T  (х  z) = T; (t  s) = T  , ,( ( , , ) ( ( , , )z v z vS t r S s r T      ; (t  s) = T  , ,( ( , , )) ( ( , , ))z v z vS t r S s r     . Формула  – тавтологiя, якщо () = T для кожної істиннісної оцінки . Твердження 4. Кожна тавтологія є неспростовною формулою. Нормальні форми. Терм мови БКФЛ назвемо нормальним, якщо:  всі його символи суперпозиції (якщо вони є) застосовані тільки до ФНС;  в усіх його символах суперпозиції (якщо вони є) згорнуті неістотні імена й виконані спрощення згі- дно з пп. 2–5 теореми 4. Терм мови БКФЛР (мови БКФЛРР) назвемо нормальним, якщо:  всі його символи суперпозиції (якщо вони є) застосовані тільки до ФНС;  в усіх його символах суперпозиції (якщо вони є) згорнуті неістотні імена й виконані спрощення згі- дно з CNT, CUT, SD, SF (згідно з CNTS, CUTS, SDS, SFS). Формула Ψ мови БКФЛ (мови БКФЛР, мови БКФЛРР) знаходиться в нормальній формі, або Ψ є норма- льною формулою, якщо:  в усіх символах суперпозиції формули Ψ (якщо вони є) згорнуті неістотні імена й виконані спро- щення;  усі символи суперпозиції формули Ψ (якщо вони є) застосовані тільки до ФНС чи ПС. Теоретичні та методологічні основи програмування 57 Нормальність формули Ф мови БКФЛ (мови БКФЛР, мови БКФЛРР) означає, що вона набуває класично- подібного вигляду: усі її символи суперпозиції застосовані тільки до ФНС чи ПС, усі її терми нормальні та в усіх її символах суперпозиції згорнуті неістотні імена й виконані належні спрощення. Теорема 7. Для кожної формули  мови БКФЛ можна збудувати нормальну формулу Ψ таку:  TF Ψ. Зведення формули  до нормальної форми виконуємо так. Використовуючи властивості S та S, про- суваємо символи суперпозиції вглиб формули. Використовуючи SSФ та п. 1 теореми 4, згортаємо символи су- перпозиції. При появі відповідної ситуації виконуємо спрощення згідно з CNФ, CUФ та пп.2–5 теореми 4. Після виконання кожного з таких перетворень ми від формули i переходимо до формули i+1 так, що при цьому i TF i+1. За теоремою еквівалентності отримуємо формулу Ψ у нормальній формі таку, що  TF Ψ. Теорема 8. Для кожної формули  мови БКФЛР (мови БКФЛРР) можна збудувати нормальну формулу Ψ таку, що  TF Ψ. Зведення  до нормальної форми виконуємо так. Використовуючи S та S, просуваємо символи су- перпозиції вглиб формули. Використовуючи SSФ і SST, згортаємо символи суперпозиції. У випадку мови БКФЛР, використовуючи SЕ, проносимо = через суперпозицію; при появі відповідної ситуації виконуємо спрощення згідно з CNФ, CUФ та CNT, CUT, SD, SF. У випадку мови БКФЛРС, використовуючи SЕS, проносимо  через суперпозицію. При появі відповідної ситуації виконуємо спрощення згідно з CNФ, CUФ та CNTS, CUTS, SDS, SFS Після кожного з таких перетворень ми від формули i переходимо до формули i+1 так, що при цьому i TF i+1. За теоремою еквівалентності отримуємо формулу Ψ у нормальній формі таку, що  TF Ψ. Таким чином, кожну формулу мови БКФЛ (БКФЛР, БКФЛРР) можна перетворити до класичноподібного вигляду, коли символи суперпозиції застосовані тільки до символів базових функцій і базових предикатів. 4. Властивості відношень логічного наслідку для множин формул Тут і надалі, якщо інше не зазначене окремо,  означає одне з відношень TF  , T  , F  , IR  . Для всіх зазначених відношень маємо монотонність: якщо    та   , то  |=   |= . Властивості декомпозиції формул: L) ,     ,   . R)   ,     , . L) ,     ,    та ,   . R)   ,     , , . L) (),     , ,   . R)   , ()    ,  та   , . Для відношення IR  можна знімати заперечення, переносячи формулу з лівої частини відношення у пра- ву і навпаки (проте це невірно для TF  , T  , F  ): L) ,  IR     IR  , . R)  IR  ,   ,  IR  . Теоретичні та методологічні основи програмування 58 Наявність кожного з відношень TF  , T  , F  , IR  . гарантує властивість: С) ,   , . Додатково гарантують наявність відношень логічного наслідку такі властивості: СL) , ,    (  – це T  чи IR  ); СR)   , ,  (  – це F  чи IR  ); СLR) , ,  TF  , , . Для IR  в силу L та R властивості СLR, СL, СR зайві, бо зводяться до властивості С Для відношення t  справджуються усі наведені вище властивості пропозиційного рівня. Властивості С, СL, СR, СLR назвемо умовами наявності логічного наслідку. Властивості декомпозиції формул L, R, L, R, L, R, L, R назвемо властивостями переходу. Наведемо властивості, пов’язані з суперпозицією. Такі властивості віднесемо до властивостей переходу, вони безпосередньо відтворюють відповідні семантичні властивості, пов’язані з еквівалентністю формул. Рівень БКФЛ. Для БКФЛ це властивості спрощення, базовані на CNФ і СUФ, та властивості нормаліза- ції SSФ, S, S та теоремі 4. Для відношення IR  кожна така властивість розщеплюється на дві відповідні вла- стивості, коли еквівалентні формули знаходяться зліва та справа від IR  . Для відношень TF  , T  , F  не мо- жна знімати заперечення, переносячи формулу з лівої частини відношення у праву і навпаки, тому кожна така властивість розщеплюється на 4 відповідні властивості, коли еквівалентні формули чи їх заперечення знахо- дяться зліва та справа від символа відношення логічного наслідку. Наведемо властивості, базовані на CNФ, СUФ, SSФ, S, S. CNФL) , ( , , ), | ( , ), |x v vS 'x t S t         ; CNФR) ,| ( , , ), | ( , ),x v vS 'x t S t         ; CNФL) , ( , , ), | ( , ), |x v vS 'x t S t           ; CNФR) ,| ( , , ), | ( , ),x v vS 'x t S t          ; CUФL) , ( , , ), | ( , ), |x v vS s t S t         , де x неістотне для ; CUФR) ,| ( , , ), | ( , ),x v vS s t S t         , де x неістотне для ; CUФL) , ( , , ), | ( , ), |x v vS s t S t           , де x неістотне для ; CUФR) ,| ( , , ), | ( , ),x v vS s t S t          , де x неістотне для . В наступних властивостях SSФL, SSФR, SSФL, SSФR позначено як  формулу , , , , , , 1 1( , , ( , , ),..., ( , , ), ( , , ),..., ( , , ))u x v u x u x u x u x k mS t S r t w S r t w S s t w S s t w : SSФL) , ,( ( , , ), , ), | , |u x x vS S r s t w         ; SSФR) , ,| ( ( , , ), , ), | ,u x x vS S r s t w         ; Теоретичні та методологічні основи програмування 59 SSФL) , ,( ( , , ), , ), | , |u x x vS S r s t w          ; SSФR) , ,| ( ( , , ), , ), | ,u x x vS S r s t w         ; SL) ( , ), | ( , ), |v vS t S t          ; SR) | ( , ), | ( , ),v vS t S t         ; SL) ( , ), | ( , ), |v vS t S t           ; SR) | ( , ), | ( , ),v vS t S t          ; SL) ( , ), | ( , ) ( , ), |v v vS t S t S t           ; SR) | ( , ), | ( , ) ( , ),v v vS t S t S t           ; SL) ( , ), | ( ( , ) ( , )), |v v vS t S t S t             ; SR) | ( , ), | ( ( , ) ( , )),v v vS t S t S t            . До цих властивостей додаємо базовані на теоремі 4 властивості нормалізації термів. Нехай формула  отримана з формули  нормалізацією термів на основі еквівалентних перетворень згідно з теоремою 4. Тоді маємо: NrTrL) ,     ,   . NrTrR)   ,     ,. NrTrL) ,     ,   . NrTrR)   ,     ,. Рівень БКФЛP. Розглянемо властивості, пов’язані з композицією слабкої рівності. Із SmW отримуємо: SmW) t = s,     t = s, s = t,   ; зокрема, t = s,  IR    t = s, s = t,  IR  ; Із TrW отримуємо транзитивність слабкої рівності для IR  : TrW) t = s, s = r,  IR    t = s, s = r, t = r,  IR  . Водночас у випадку БКФЛР для відношень T  , F  , TF  транзитивність слабкої рівності порушується. Це випливає з того, що властивість TrW можна посилити лише так: TrL) x = y, y = z,     x = y, y = z, x = z,    (тут  – це IR  чи T  ); TrR)   ,  x = y,  y = z    ,  x = y,  y = z,  x = z (тут  – це IR  чи F  ). Справді, маємо T(t = s)  T(s = r) = T(t = s)  T(s = r)  T(t = r), звідси TrL вірне для T  та TrR вірне для F  . Згідно T   IR  та в силу F   IR  властивості TrL та TrR вірні для IR  . Маємо x = y, y = z |F x = y & y = z & x = z та  x = y   y = z   x = z |T  x = y,  y = z. Справді, при a  b для d = [xa, zb] маємо dF(x = y)  F(y = z), проте dF(x = z)  dF(x = z)  F(x = y)  F(y = z). Теоретичні та методологічні основи програмування 60 Водночас x = y, y = z, x = z |=F x = y & y = z & x = z та  x = y   y = z   x = z |=T  x = y,  y = z,  x = z. Таким чином, TrL невірна для F  , а TrR невірна для T  . тому для TF  невірні обидві властивості TrL та TrR. Отже, для БКФЛР адекватним залишається лише відношення | IR . Властивість RfW індукує достатню умову наявності відношення | IR : СRfW)  | IR t = t, . Властивість SЕ індукує властивості дистрибутивності суперпозиції відносно рівності для відношення |=IR : SЕL) ( , ), | ( , ) ( , ), |v v v IR IRS s r t S s t S r t         ; SЕR) | ( , ), | ( , ) ( , ),v v v IR IRS s r t S s t S r t         . Властивість EP індукує властивості заміни рівних для відношення | IR : EPL) , , ,, ( , , ), | , ( , , ), ( , , ), |v z v z v z IR IRt s S r t t s S r t S r s            ; EPR) , , ,, | ( , , ), , | ( , , ), ( , , ),v z v z v z IR IRt s S r t t s S r t S r s            . Властивості кроку нормалізації термів, індуковані ST, CNT, CUT, SDT, SFT, мають вигляд: Nr*L) ,  | IR   ,  | IR ; Nr*R)  | IR ,    | IR ,. Тут  утворена із  заміною деяких входжень термів, що є лівими частинами рівностей, які фігурують в цих властивостях, на терми, що є правими частинами відповідних рівностей, так, як описано в теоремі 4. Рівень БКФЛPС. Розглянемо властивості, пов’язані з композицією строгої рівності. Властивість RfS індукує достатню умову наявності кожного з відношень | IR , |=T, |=F, |=TF : СRfS)   t  t, . На основі SmS та TrS отримуємо: SmS) t  s,     t  s, s  t,   ; TrS) t  s, s  r,     t  s, s  r, t  r,   . Властивість SЕS індукує властивості дистрибутивності суперпозиції відносно рівності: SЕSL) ( , ), | ( , ) ( , ), |v v vS s r t S s t S r t         ; SЕSR) | ( , ), | ( , ) ( , ),v v vS s r t S s t S r t         . Властивість EPS індукує властивості заміни рівних: EPSL) , , ,, ( , , ), | , ( , , ), ( , , ), |v z v z v zt s S r t t s S r t S r s            ; EPSR) , , ,, | ( , , ), , | ( , , ), ( , , ),v z v z v zt s S r t t s S r t S r s            . EPSL) , , ,, ( , , ), | , ( , , ), ( , , ), |v z v z v zt s S r t t s S r t S r s               ; EPSR) , , ,, | ( , , ), , | ( , , ), ( , , ),v z v z v zt s S r t t s S r t S r s               . Теоретичні та методологічні основи програмування 61 Для відношення |=IR достатньо властивостей EPSLта EPSR. Властивості кроку нормалізації термів, індуковані STS, CNTS, CUTS, SDS, SFS, мають вигляд: NrS*L) ,     ,   ; NrS*R)   ,     ,. Тут  утворена із  заміною деяких входжень термів, що є лівими частинами рівностей, які фігурують в цих властивостях, на терми, що є правими частинами відповідних рівностей, так, як описано в теоремі 4. Підсумовуючи, отримуємо наступне. Для відношення | IR множин формул БКФЛ маємо базові властивості переходу NrTrL, NrTrR, CNФL, CNФR, СUФL, CUФR, SSФL, SSФR, SL, SR, SL, SR; L, R, L, R . Властивість наявності логічного наслідку: С. Для відношень TF  , T  , F  множин формул БКФЛ маємо базові властивості переходу NrTrL, NrTrR, NrTrL, NrTrR, CNФL, CNФR, CNФL, CNФR, СUФL, CUФR, СUФL, CUФR, SSФL, SSФR, SSФL, SSФR, SL, SR, SL, SR, SL, SR, SL, SR; L, R, L, R, L, R . Властивості наявності логічного наслідку: С та СLR для TF  ; С та СL для T  ; С та СR для F  . Для відношення IR  множин формул БКФЛР маємо базові властивості переходу Nr*L, Nr*R, SmW, TrW, SЕL, SЕR, EPL, EPR, CNФL, CNФR, СUФL, CUФR, SSФL, SSФR, SL, SR, SL, SR; L, R, L, R . Властивості наявності логічного наслідку: С та СRfW. Для відношення IR  множин формул БКФЛРС маємо базові властивості переходу NrS*L, NrS*R, SmW, TrW, SЕSL, SЕSR, EPSL, EPSR, CNФL, CNФR, СUФL, CUФR, SSФL, SSФR, SL, SR, SL, SR; L, R, L, R . Властивості наявності логічного наслідку: С та СRfS. Для відношень TF  , T  , F  множин формул БКФЛРС маємо базові властивості переходу NrS*L, NrS*R, SmW, TrW, SЕSL, SЕSR, EPSL, EPSR, EPSL, EPSR, NrTrL, NrTrR, CNФL, CNФR, CNФL, CNФR, СUФL, CUФR, СUФL, CUФR, SSФL, SSФR, SSФL, SSФR, SL, SR, SL, SR, SL, SR, SL, SR; L, R, L, R, L, R . Властивості наявності логічного наслідку: С, СRfS, СLR для TF  ; С, СRfS, СL для T  ; С, СRfS, СR для F  . Описані властивості відношень логічного наслідку для множин формул є семантичною основою побудо- ви для цих відношень в БКФЛ, БКФЛР та БКФЛРС низки числень секвенційного типу. Властивості наявності логічного наслідку індукують умови замкненості секвенції, властивості переходу індукують відповідні секвен- ційні форми. Висновки Досліджено безкванторні композиційно-номінативні логіки часткових квазіарних предикатів. Виділено наступні рівні цих логік: реномінативний, реномінативний з предикатами слабкої рівності, реномінативний з предикатами строгої рівності, безкванторно-функціональний, безкванторно-функціональний з композицією слабкої рівності, безкванторно-функціональний з композицією строгої рівності. Основна увага приділена логі- кам безкванторно-функціональних рівнів з рівністю. Описано мови та семантичні моделі безкванторних логік, досліджено їх семантичні властивості. Наведено властивості композицій суперпозиції, слабкої рівності та стро- гої рівності, розглянуто нормальні форми термів та формул. Досліджено властивості відношень логічного нас- лідку для множин формул. Такі властивості є семантичною основою побудови для різних класів безкванторних логік низки числень секвенційного типу, що планується зробити в наступних роботах. 1. Нікітченко М.С. , Шкільняк С.С. Математична логіка та теорія алгоритмів. – К.: ВПЦ Київський університет, 2008. – 528 с. 2. Нікітченко М.С. , Шкільняк С.С. Прикладна логіка. – К.: ВПЦ Київський університет, 2013. – 278 с. 3. Шкільняк С.С. Секвенційні числення реномінативних логік квазіарних предикатів // Наукові записки НаУКМА. Серія: Комп’ютерні науки. – К., 2012. – Т. 138. – C. 23–29. Теоретичні та методологічні основи програмування 62 4. Шкільняк С.С., Волковицький Д.Б. Реномінативні композиційно-номінативні логіки з предикатами рівності // Вісник Київського націо- нального університету імені Тараса Шевченка. Сер.: фіз.-мат. науки. – 2014. – Вип. 3. – C. 198–205. 5. Шкільняк С.С., Волковицький Д.Б. Безкванторно-функціональні логіки часткових квазіарних предикатів // Вісник Київського націона- льного університету імені Тараса Шевченка. Серія: фіз.-мат. науки. – 2015. – Вип. 3. 6. Nikitchenko М. , Shkilniak S. Semantic Properties of Logics of Quasiary Predicates // Workshop on Foundations of Informatics: Proceedings FOI-2015. – Chisinau, Moldova. – P. 180–197. References 1. NIKITCHENKO, M. and SHKILNIAK, S. (2008). Mathematical logic and theory of algorithms. Кyiv: VPC Кyivskyi Universytet (in ukr). 2. NIKITCHENKO, M. and SHKILNIAK, S. (2013). Applied logic. Кyiv: VPC Кyivskyi Universytet (in ukr). 3. SHKILNIAK, S. (2012). Sequent calculi of renominative logics of quasiary predicates. In Scientific Notes of NaUKMA. Series: Computer Sciences. 138, p. 23–29 (in ukr). 4. SHKILNIAK, S. and VOLKOVYTSKYI, D. (2014). Renominative composition-nominative logics with predicates of equality. In Bulletin of Taras Shevchenko National University of Kyiv. Series: Physics & Mathematics. No 3. P. 198–205 (in ukr). 5. SHKILNIAK, S. and VOLKOVYTSKYI, D. (2015). Free-quantifier functional logics of partial quasi-ary predicates. In Bulletin of Taras Shevchenko National University of Kyiv. Series: Physics & Mathematics. No 3. P. (in ukr). 6. NIKITCHENKO, M. and SHKILNIAK, S. (2015). Semantic Properties of Logics of Quasiary Predicates. In Workshop on Foundations of Informatics: Proceedings FOI-2015. Chisinau, Moldova. P. 180–197. Про авторів: Шкільняк Степан Степанович, доктор фізико-математичних наук, професор, професор кафедри Теорії та технології програмування. Кількість наукових публікацій в українських виданнях – понад 200, у тому числі у фахових виданнях – 92. Кількість наукових публікацій в іноземних виданнях – 14. Індекс Гірша – 4 (3 з 2010). http://orcid.org/0000-0001-8624-5778, Волковицький Дмитро Борисович, аспірант факультету кібернетики. Кількість наукових публікацій в українських виданнях – 10, у тому числі у фахових виданнях – 4. Кількість наукових публікацій в іноземних виданнях – 1. http://orcid.org/0000-0002-4620-1444. Місце роботи авторів: Київський національний університет імені Тараса Шевченка , 01601, Київ, вул. Володимирська, 60. Тел.: (044) 259 0519. E-mail: sssh@unicyb.kiev.ua, dimmka86@gmail.com

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