Повнота секвенційних числень модальних логік немонотонних часткових предикатів
Для чистих першопорядкових композиційно-номінативних модальних логік часткових немонотонних предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них вказано базові секвенційні форми та умови замкненості секвенцій, доведено їх коректність і повноту. Доведення теореми...
Збережено в:
| Дата: | 2016 |
|---|---|
| Автори: | , , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут проблем штучного інтелекту МОН України та НАН України
2016
|
| Назва видання: | Штучний інтелект |
| Теми: | |
| Онлайн доступ: | http://dspace.nbuv.gov.ua/handle/123456789/132074 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Повнота секвенційних числень модальних логік немонотонних часткових предикатів / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Штучний інтелект. — 2016. — № 3. — С. 92-102. — Бібліогр.: 7 назв. — укр. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-132074 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-1320742018-04-11T03:03:26Z Повнота секвенційних числень модальних логік немонотонних часткових предикатів Шкільняк, О.С. Касьянюк, В.С. Малютенко, Л.М. Теорія та засоби обчислювального інтелекту Для чистих першопорядкових композиційно-номінативних модальних логік часткових немонотонних предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них вказано базові секвенційні форми та умови замкненості секвенцій, доведено їх коректність і повноту. Доведення теореми повноти опирається на теорему про існування контрмоделі для незамкненого шляху в секвенційному дереві, для її побудови використано метод систем модельних множин. In this paper we construct sequent calculi for pure first-order composition nominative modal logics of partial non-monotone predicates. We specify various variants of the introduced calculi, their basic sequent forms and sequent closure conditions. The proof of the completeness theorem is based on the theorem about existence of a counter-model for a non-closed path in a sequent tree; the counter-model is obtained using the Hintikka sets method. 2016 Article Повнота секвенційних числень модальних логік немонотонних часткових предикатів / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Штучний інтелект. — 2016. — № 3. — С. 92-102. — Бібліогр.: 7 назв. — укр. 1561-5359 http://dspace.nbuv.gov.ua/handle/123456789/132074 004.42:510.69 uk Штучний інтелект Інститут проблем штучного інтелекту МОН України та НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Ukrainian |
| topic |
Теорія та засоби обчислювального інтелекту Теорія та засоби обчислювального інтелекту |
| spellingShingle |
Теорія та засоби обчислювального інтелекту Теорія та засоби обчислювального інтелекту Шкільняк, О.С. Касьянюк, В.С. Малютенко, Л.М. Повнота секвенційних числень модальних логік немонотонних часткових предикатів Штучний інтелект |
| description |
Для чистих першопорядкових композиційно-номінативних модальних логік часткових немонотонних предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них вказано базові секвенційні форми та умови замкненості секвенцій, доведено їх коректність і повноту. Доведення теореми повноти опирається на теорему про існування контрмоделі для незамкненого шляху в секвенційному дереві, для її побудови використано метод систем модельних множин. |
| format |
Article |
| author |
Шкільняк, О.С. Касьянюк, В.С. Малютенко, Л.М. |
| author_facet |
Шкільняк, О.С. Касьянюк, В.С. Малютенко, Л.М. |
| author_sort |
Шкільняк, О.С. |
| title |
Повнота секвенційних числень модальних логік немонотонних часткових предикатів |
| title_short |
Повнота секвенційних числень модальних логік немонотонних часткових предикатів |
| title_full |
Повнота секвенційних числень модальних логік немонотонних часткових предикатів |
| title_fullStr |
Повнота секвенційних числень модальних логік немонотонних часткових предикатів |
| title_full_unstemmed |
Повнота секвенційних числень модальних логік немонотонних часткових предикатів |
| title_sort |
повнота секвенційних числень модальних логік немонотонних часткових предикатів |
| publisher |
Інститут проблем штучного інтелекту МОН України та НАН України |
| publishDate |
2016 |
| topic_facet |
Теорія та засоби обчислювального інтелекту |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/132074 |
| citation_txt |
Повнота секвенційних числень модальних логік немонотонних часткових предикатів / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Штучний інтелект. — 2016. — № 3. — С. 92-102. — Бібліогр.: 7 назв. — укр. |
| series |
Штучний інтелект |
| work_keys_str_mv |
AT škílʹnâkos povnotasekvencíjnihčislenʹmodalʹnihlogíknemonotonnihčastkovihpredikatív AT kasʹânûkvs povnotasekvencíjnihčislenʹmodalʹnihlogíknemonotonnihčastkovihpredikatív AT malûtenkolm povnotasekvencíjnihčislenʹmodalʹnihlogíknemonotonnihčastkovihpredikatív |
| first_indexed |
2025-07-09T16:40:06Z |
| last_indexed |
2025-07-09T16:40:06Z |
| _version_ |
1837189032206925824 |
| fulltext |
ISSN 1561-5359. Штучний інтелект, 2016, № 3
92 © О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко
УДК 004.42:510.69
О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко
Київський національний університет імені Тараса Шевченка, Україна
вул. Володимирська, 60, м. Київ, 01601
ПОВНОТА СЕКВЕНЦІЙНИХ ЧИСЛЕНЬ МОДАЛЬНИХ ЛОГІК
НЕМОНОТОННИХ ЧАСТКОВИХ ПРЕДИКАТІB
O. Shkilniak, V. Kasianiuk, L. Malutenko
Taras Shevchenko National University of Kyiv, Ukraine
Volodymyrska st., 60, Kyiv, 01601
СOMPLETENESS OF SEQUENT CALCULI FOR MODAL LOGICS OF
NON-MONOTONE PARTIAL PREDICATES
Для чистих першопорядкових композиційно-номінативних модальних логік часткових немонотонних
предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них вказано
базові секвенційні форми та умови замкненості секвенцій, доведено їх коректність і повноту. Доведення
теореми повноти опирається на теорему про існування контрмоделі для незамкненого шляху в
секвенційному дереві, для її побудови використано метод систем модельних множин.
Ключові слова: модальна логіка, секвенційне числення, коректність, повнота.
In this paper we construct sequent calculi for pure first-order composition nominative modal logics of partial
non-monotone predicates. We specify various variants of the introduced calculi, their basic sequent forms and
sequent closure conditions. The proof of the completeness theorem is based on the theorem about existence of a
counter-model for a non-closed path in a sequent tree; the counter-model is obtained using the Hintikka sets method.
Key words: modal logic, sequent calculus, soundness, completeness.
Вступ
Автоматизація пошуку виведень належить до найважливіших застосувань матема-
тичної логіки. Конструктивне знаходження виведень необхідне для успішного розв'язання
низки задач, що виникають у сучасних інформаційних і програмних системах. Ефективним
апаратом побудови виведень є секвенційні числення. Побудові та дослідженню секвен-
ційних числень першопорядкових модальних логік часткових немонотонних предикатів
присвячена дана робота.
Модальні логіки з великим успіхом використовуються для опису й моделювання
різноманітних предметних областей, для специфікації й верифікації програм. Можливості
традиційних модальних логік [1] і композиційно-номінативних логік квазіарних предикатів
[2], [3], [4] синтезують композиційно-номінативні модальні логіки (КНМЛ), що будуються
на основі спільного для логіки й програмування композиційно-номінативного підходу.
Найважливішим класом КНМЛ є транзиційні модальні логіки (ТМЛ), які відбивають аспект
зміни й розвитку предметних областей. Першопорядкові ТМЛ часткових предикатів, не
обмежених умовою монотонності, досліджено в [5], [6], [7].
Метою даної роботи є доведення теорем коректності та повноти секвенційних числень
чистих першопорядкових ТМЛ немонотонних предикатів. Такі числення збудовано на
основі властивостей відношення логічного наслідку для множин специфікованих станами
формул. Теорема про повноту опирається на теорему про існування контрмоделі для
незамкненого шляху в секвенційному дереві, для її побудови використано метод систем
модельних множин.
Поняття, які тут не визначаються, будемо тлумачити в змісті робіт [3], [4] [6].
Транзиційні модальні системи
Центральним для ТМЛ є поняття транзиційної модальної системи (ТМС). Це об'єкт
вигляду (Cms, Fт, Iт), де Cms – композиційна модальна система (КМС), Fm – множина
формул мови, Iт – відображення інтерпретації формул на станах світу. КМС мають вигляд
Cms = (S, R, Pr, C), де S – множина станів світу, R – множина відношень на S вигляду
R S S (трактуємо їх як відношення переходу на станах), Pr – множина предикатів на
станах, C – множина композицій на Pr. Для чистих першопорядкових ТМС S – це множина
алгебраїчних систем вигляду = (A, Pr), де Pr – множина квазіарних предикатів вигляду
ISSN 1561-5359. Штучний інтелект, 2016, № 3
© О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко 93
VA {T, F} (предикати стану ). Предикати вигляду VA {T, F}, де ,
S
A A
назвемо гло-
бальними. Множина C визначається базовими загальнологічними композиціями , , R ,v
x x
та базовими модальними композиціями. Залежно від R та базових модальних композицій
можна виділити [5] мультимодальні, епістемічні, темпоральні, загальні ТМС (ЗМС). У цій
роботі обмежимось розглядом ЗМС, у них { }R та єдина базова модальна композиція .
Опишемо мову чистих першопорядкових ЗМС. Алфавіт мови: множини V
предметних імен (змінних), Ps предикатних символiв (сигнатура мови); символи
базових композицій , , v
xR , x та . Множину Fт формул визначимо так.
Маємо Ps Fт, а далі задаємо: , Fт , Ф, ,v
xR x, Fт.
Введемо відображення інтерпретації формул на станах. Спочатку задамо
Iт : Рs S® Pr, при цьому Iт(p, ) Pr (базові предикати є предикатами станів).
Продовжимо Iт до відображення Iт : Fт S® Pr так:
Iт(, ) = (Iт(, )); Iт(, ) = (Iт(, ), Iт(, ));
( , ) R ( ( , ))v v
x xIm R Im ;
( , )Im x
, якщо існує : ( , )( ) ,
, якщо ( , )( ) для всіх ,
невизначене в усіх інших випадках;
T a A Im d x a T
F Im d x a F a A
Iт(, )(d) =
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
T Im d T S
F S Im d F
Якщо для S не існує : , то Iт(, )(d) для кожного dVA.
Предикати, які є значеннями немодалізованих формул (при їх побудові не
використовуються символи ), належать до предикатів станів.
Предикат Iт(, ), який є значенням формули у стані , позначаємо .
Формула неспростовна (частково істинна) в ТМС M (позн. M |= ), якщо
неспростовний для всіх S. Формула неспростовна (позн. |= ), якщо M |= для
всіх ТМС M одного типу. ТМС далі подаємо у вигляді M = (S, R, А, Iт).
Залежно від умов, накладених на відношення , можна визначати різні класи
ТМС. Традиційними є випадки, коли рефлексивне, симетричне чи транзитивне, тоді
до назви ТМС додаємо R, T чи S. Зокрема, маємо такі типи ЗМС:
R-ЗМС, T-ЗМС, S-ЗМС, RT-ЗМС, RS-ЗМС, TS-ЗМС, RTS-ЗМС.
Введемо відношення логічного наслідку для множин специфікованих станами
формул, яке відповідає відношенню |=IR неспростовнісного логічного наслідку в логіках
квазіарних предикатів [4]. Нехай M = (S, R, А, Iт), S – множина імен станів S.
Специфіковані станом формули подамо як , де S – специфікація .
Нехай та – множини специфікованих станами формул.
Множина узгоджена із ТМС M, якщо задана ін’єкція S у S.
є наслідком в узгодженій із ними ТМС M, якщо для всіх dVA маємо:
(d) = T для всіх неможливо Ψ(d) = F для всіх Ψ.
Це позначимо M|= . Такий запис завжди означає узгодженість M із та .
є логічним наслідком (відносно ТМС певного типу), якщо M|= для всіх
ТМС M (які належать до цього типу). Це позначаємо |= .
Немодальні властивості відношення |= повторюють відповідні властивості
відношення |=IR (див. [4]). При цьому для елімінації кванторів використовуємо
спеціальні предикати-індикатори Ez [4].
ISSN 1561-5359. Штучний інтелект, 2016, № 3
94 © О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко
Властивості елімінації модальностей у загальному вигляді та для випадків, коли
може бути транзитивним, рефлексивним чи симетричним, наведено в [6].
Секвенційні числення чистих першопорядкових ЗМЛ
Розглядаємо числення чистих першопорядкових ЗМЛ. Подібним чином можна
розглядати числення мультимодальних ТМЛ. Числення темпоральних ТМЛ отримуємо
з числень ЗМЛ «розщепленням» секвенційних форм із модульностями.
У численнях ТМЛ під секвенціями будемо розуміти множини специфікованих
станами формул. Специфікації мають вигляд |– чи –|, де – ім'я стану. Формули,
специфіковані |–, назвемо |–-формулами, а специфіковані –| ––|-формулами.
Виділяючи такі формули, секвенції позначаємо як |––|. Для секвенції та фіксованого
задаємо секвенцію = { | = |– чи = –|} формул стану . При побудові
виведення збагачуємо секвенції збудованими на даний момент множинами відношень
на станах. Збагачені секвенції записуємо як // M, де M – схема моделі світу, тобто
збудоване на цей момент відношення досяжності, записане для імен станів.
Виведення в секвенційних численнях має вигляд дерева, вершинами якого є
секвенції. Правилами виведення секвенційних числень є секвенційні форми, вони
індукуються відповідними властивостями відношення логічного наслідку для множин
специфікованих станами формул |=. Аксіомами секвенційних числень є замкнені
секвенції. Для замкненої секвенції |––| має виконуватись умова |= .
Секвенційне дерево замкнене, якщо всі його листи – замкнені секвенції.
Секвенція вивідна, якщо існує замкнене секвенційне дерево з коренем .
Для опису умови замкненості секвенції для формул ТМЛ введемо поняття Un-
unv-еквівалентності (про Un-unv-еквівалентність див. [4]).
Множини означених, неозначених, нерозподілених імен стану секвенції :
val() = {u | |–Eu}; unv() = {u | –|Eu}; ud() = nm() \ (val() unv()).
Формули вигляду ( )x
yR назвемо R-формулами.
Rs-форма R-формули , ,
, , ( ),x u v
x y zR де { } ( ),u – це формула ( ),v
zR утворена з
, ,
, , ( )x u v
x y zR всеможливими спрощеннями зовнішньої реномінації згідно з
властивостями R, RI, RU [4].
Нехай Un = unv(), а , ,
, ,
r x u
s y vR така: { , , } , { , } .r s y Un x v Un
Un-форма формули , ,
, ,
r x u
s y vR – це вираз ,
,
x u
vR (тут символ V позначає
відсутність значення).
R-формули та назвемо Rs-Un-еквівалентними, якщо та мають однакові
Rs-форми або ці Rs-форми мають однакові Un-форми. Якщо R-формули та Rs-Un-
еквівалентні, то та теж назвемо Rs-Un-еквівалентними.
Теорема 1. Якщо та – Rs-Un-еквівалентні, то (d) = (d) для всіх d, для
яких Eu(d) = F для всіх uUn, тобто asn(d)Un = .
Таким чином, отримуємо наступну умову замкненості секвенції :
С) існують та Un-unv-еквівалентні |– та –| такі: |– та –|;
зокрема, існують та формула така: |– та –|.
Опишемо базові секвенційні форми. Форми еквівалентних перетворень:
|RR
|
|
( ), //
( ( )), //
v w
x y
v w
x y
R M
R R M
; |RR
|
|
( ), //
( ( )), //
v w
x y
v w
x y
R M
R R M
;
|R
|-
|-
( ), //
( ), //
v
x
v
x
R M
R M
; |R
|
|
( ), //
( ), //
v
x
v
x
R M
R M
;
|R
| |
|
( ), // ( ), //
( ), //
v v
x x
v
x
R M R M
R M
; |R
| |
|
( ), ( ), //
( ), //
v v
x x
v
x
R R M
R M
;
ISSN 1561-5359. Штучний інтелект, 2016, № 3
© О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко 95
|–Rs
|
|
( ), //
, { , }
( ), //
v
x
v
x
yR M
y v x
R y M
; –|Rs
|
|
( ), //
, { , }
( ), //
v
x
v
x
yR M
y v x
R y M
;
|–R
|
|
( ), //
( ), //
v y
x z
v
x
zR M
R y M
; –|R
|
|
( ), //
( ), //
v y
x z
v
u
zR M
R x M
.
Для |–R i –|R умова: ( ( ))v
xz fu R x .
|R
|
|
( ), //
( ), //
v
x
v
x
R M
R M
; |R
|
|
( ), //
( ), //
v
x
v
x
R M
R M
.
Для |–R i –|R умова: ( ( ))v
xz fu R x .
|R
|
|
( ), //
( ), //
v
x
v
x
R M
R M
; |R
|
|
( ), //
( ), //
v
x
v
x
R M
R M
.
Окрім наведених базових форм, можна використовувати допоміжні форми
спрощення. Перетворення на основі цих форм вже закладені в умови замкненості
секвенції: для встановлення Rs-Un-еквівалентності формул необхідна побудова їх Rs-
форм, що робиться на основі R, RI, RU. Форми спрощення:
|–R
|
|
, //
( ), //
M
R M
; |–R
|
|
, //
( ), //
M
R M
;
|–RI
|
,
| ,
( ), //
( ), //
v
u
y v
y u
R M
R M
; –|RI
|
,
| ,
( ), //
( ), //
v
u
y v
y u
R M
R M
;
|–RU
|
,
| ,
( ), //
, ( )
( ), //
v
u
y v
z u
R M
y v
R M
; –|RU
|
,
| ,
( ), //
, ( )
( ), //
v
u
y v
z u
R M
y v
R M
.
Форми декомпозиції формул:
|–
|
|
, //
, //
M
M
; |
|
|
, //
, //
M
M
;
|
| |
|
, // , //
, //
M M
M
; |
| |
|
, , //
, //
M
M
.
Форми елімінації кванторів та E-розподілу:
|–
| |
|
( ), , //
, ( , )
, //
x
zR Ez M
z fu x
x M
; –|v
| | |
| |
, ( ), , //
, , //
x
yx R Ey M
x Ey M
;
Ed
| |, // , //
Ex M Ex M
, де |–Ex, –|Ex .
Форми елімінації модальних операторів залежать від властивостей .
Розглянемо випадки, коли може бути рефлексивним, транзитивним чи
симетричним. Це дає (див. [6]) різновиди чистих першопорядкових числень ЗМЛ.
На не накладені додаткові умови. Маємо CMG-числення.
Якщо в момент застосування форми до | маємо стани 1, …, n такі, що
1,..., n , то до | застосовуємо
| 1| | |
|
, ,..., , //
, //
n
M
M
.
Якщо таких , що , немає, то до | застосовуємо форму
ISSN 1561-5359. Штучний інтелект, 2016, № 3
96 © О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко
|f
| |
|
, , // { }
, //
M
M
, – новий стан.
Форма елімінації, яка застосовується до |:
|
|
|
, // { }
, //
M
M
, – новий стан.
рефлексивне. Маємо CMG_R-числення. Тоді завжди .
До | застосовуємо форму | для всіх станів 1, …, n таких, що в момент її
застосування 1,..., n . Форма елімінації, яка застосовується до |:
|R
|
|
, // { , }
, //
M
M
, – новий стан.
симетричне. Маємо CMG_S-числення. Тоді завжди .
Якщо в момент застосування форми до | маємо стани 1, …, n такі, що
1,..., n , то застосовуємо |. Якщо таких : , немає, то застосовуємо
|fS
| |
|
, , // { , }
, //
M
M
, – новий стан
До | застосовується така форма:
|S
|
|
, // { , }
, //
M
M
, – новий стан.
рефлексивне та симетричне. Маємо CMG_RS-числення.
Тоді завжди та завжди .
До | застосовуємо форму | для всіх станів 1, …, n таких, що в момент її
застосування 1,..., n . До | застосовується така форма:
|RS
|
|
, // { , , }
, //
M
M
, – новий стан.
транзитивне. Маємо CMG_T-числення.
До | застосовуємо форму |. Якщо в момент застосування форми до |
маємо стани 1, …, n такі, що 1,..., n , то застосовуємо
|T 1 1| | | | |
|
, ,..., , ,..., , //
, //
n n
M
M
.
Специфіковані
1| |,...,
n тут необхідні через транзитивність .
Якщо ж таких , що , немає, то застосовуємо форму:
|fT
| | |
|
, , , // { }
, //
M
M
, – новий стан
транзитивне й рефлексивне. Маємо CMG_RT-числення.
До | застосовуємо форму |R. До | застосовуємо форму |T для всіх
1, …, n таких, що в момент її застосування 1,..., n (тут маємо ).
транзитивне й симетричне. Отримуємо CMG_TS-числення.
До | застосовуємо форму |S. Якщо в момент застосування форми до |
маємо стани 1, …, n такі, що 1,..., n , то застосовуємо |T (тут маємо
). Якщо немає таких , що , то застосовуємо
ISSN 1561-5359. Штучний інтелект, 2016, № 3
© О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко 97
|fTS
| | |
|
, , , // { , }
, //
M
M
, – новий стан.
транзитивне, рефлексивне й симетричне. Маємо CMG_RTS-числення.
До | застосовуємо |RS. До | застосовуємо |T для всіх 1, …, n
таких, що в момент її застосування 1,..., n (тут та ).
Теорема 2. 1) Нехай
| |
| |
// M
// M
– секвенційна форма, тоді:
|= |= ; | | .
2) Нехай
| | | |
| |
// M // M
// M
– секвенційна форма, тоді:
|= та |= |= ; | | або | .
Побудова секвенційного дерева. Теорема коректності
Побудова секвенційного дерева для першопорядкових числень ТМЛ немонотонних
предикатів подібна до відповідних побудов для числень логік немонотонних квазіарних
предикатів [4] та числень ТМЛ еквітонних предикатів. Побудова дерева ведеться
паралельно із побудовою схеми моделі світу. Ця схема оновлюється при застосуванні
відповідних форм елімінації модальностей, які додають нові стани.
Побудова дерева розбита на етапи. Вона починається з кореня дерева – початкової
секвенції . Кожне застосування секвенційної форми проводимо до скінченної
множини доступних на даний момент формул. На початку кожного етапу виконуємо
крок доступу: до списку доступних формул додаємо по одній формулі зі списків |-
формул та |-формул. На початку побудови доступна пара перших формул списків
(єдина |-формула чи |-формула, якщо один зі списків порожній).
Після виконання кожної секвенційної форми перевіряємо, чи буде відповідна
вершина-секвенція замкненою. При появі замкненої секвенції до неї незастосовна
жодна форма, тому процес побудови дерева на цьому шляху обривається.
Секвенції ми трактуємо як множини специфікованих формул, тому повторів
формул у секвенціях бути не може.
Якщо всі листи збудованого дерева замкнені, то маємо замкнене секвенційне
дерево, побудова завершена позитивно. Якщо ні, то при виведенні скінченної секвенції
додатково перевіряємо, чи буде хоч один із листів фінальною секвенцією.
Незамкнена вершина-секвенція виведення секвенції – фінальна, якщо до неї
вже незастосовна жодна секвенційна форма, або якщо кожне застосування секвенційної
форми до не вводить нових формул, тобто формул, відмінних від формул секвенцій
на шляху від до . Поява фінальної секвенції означає ситуацію повторення
незамкненої секвенції на даному шляху. Це сигналізує про наявність в дереві шляху
(від кореня до даної фінальної секвенції), всі вершини якого незамкнені. Такий шлях
назвемо незамкненим.
Якщо побудова не завершена, то для кожного незамкненого листа робимо
наступний крок доступу, далі добудовуємо скінченне піддерево з вершиною таким
чином. Активізуємо всі доступні (окрім примітивних) формули . Далі до кожної
активної формули застосовуємо відповідну секвенційну форму. Після застосування
основної форми утворені нею формули на даному етапі пасивні, до таких формул на
цьому етапі основні секвенційні форми незастосовні. В процесі застосування основних
форм усуваємо, у разі наявності, тотожні реномінації, тотожні перейменування та пари
імен реномінацій за неістотним верхнім іменем. Для цього належну кількість разів
ISSN 1561-5359. Штучний інтелект, 2016, № 3
98 © О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко
застосовуємо допоміжні форми типів R, RI, RU.
Застосування на етапі основних секвенційних форм проводимо так.
Спочатку виконуємо (за можливості) всі форми типу RR, R, R, Rs, R, R, ,
та |–-форми. При застосуванні |–-форми кожен раз беремо нове тотально неістотне
zV. Далі застосовуємо форми –|v, це має певні особливості.
Нехай – множина доступних формул секвенцій на шляху від до . Для кож-
ного стану задаємо Ud = ud(). Якщо при переході до застосування –|v до –|x
маємо Ud , то є нерозподілені імена стану , тому за допомогою Еd робимо
всеможливі розподіли імен із Ud на означені та неозначені. Це веде до побудови
піддерева висоти |Ud| з вершиною , що дає | |2Udm наступників – секвенції
1,…,m з множинами Vnk Ud нових означених імен.
Якщо val() = , то для тієї j, де Vnj = , робимо первісне означення – додаємо
|–Ez для нового тотально неістотного z, що дає Vnj = {z}. В кожній з цих k
застосовуємо –|v до –|x для кожного уVnk.
Далі виконуємо –|-форми, а на завершення етапу – |-форми.
Побудова секвенційного дерева може завершуватися або не завершуватися.
Якщо побудова завершена позитивно, то маємо замкнене дерево.
Якщо побудова завершена негативно, то маємо скінченне незамкнене дерево.
Якщо побудова не завершується, то маємо нескінченне незамкнене дерево. За лемою
Кеніга нескінченне дерево зі скінченним розгалуженням має хоча б один нескінченний
шлях. Таким чином, якщо побудова завершена негативно або не завершується, то в
дереві існує скінченний або нескінченний незамкнений шлях . Кожна з формул
початкової секвенції зустрінеться на і стане доступною.
Теорема 3 (коректності). Нехай секвенція |––| вивідна. Тоді |= .
Нехай |––| вивідна, тоді для неї побудоване замкнене секвенційне дерево. Усі
його листи – замкнені секвенції, тому |= для кожного такого листа |––|. Рух від
листів дерева до його кореня робимо за допомогою секвенційних форм. За теоремою 2,
при переході від засновків до висновків секвенційних форм зберігається відношення |=.
Тому для кожної вершини секвенційного дерева |––| маємо |= . Зокрема, для
секвенції |––| – кореня дерева – теж маємо |= .
Теорема про контрмодель. Теорема повноти
Для доведення повноти секвенційних числень модальних логік традиційно
використовується метод систем модельних множин.
Система модельних множин – це пара ({Н | S}, M), де кожна Н –модельна
множина стану , M – схема моделей світу, яка задається R.
Для множин Н задаємо Un = unv(Н), W = nm(Н) \ Un.
Модельна множина стану Н визначається умовою коректності та умовами
переходу. Умова коректності індукується умовою замкненості секвенції:
MС) не існує Rs-Un-еквівалентних формул та : |–Н та –|Н.
Умови переходу індуковані виконанням відповідних секвенційних форм.
MRR) | ( ( ))v w
x yR R H | ( )v w
x yR H ;
| ( ( ))v w
x yR R H | ( )v w
x yR H ;
MR) | ( )v
xR H | ( )v
xR H ;
| ( )v
xR H | ( )v
xR H ;
MR) | ( )v
xR H | ( )v
xR H або | ( )v
xR H ;
| ( )v
xR H | ( )v
xR H та | ( )v
xR H ;
ISSN 1561-5359. Штучний інтелект, 2016, № 3
© О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко 99
MRs) за умови { , }y v x маємо:
| ( )v
xR y H | ( )v
xyR H ; | ( )v
xR y H | ( )v
xyR H .
MR) за умови ( ( ))v
xz fu R x маємо:
| ( )v
xR y H | ( )v y
x zzR H ;
| ( )v
xR y H | ( )v y
x zzR H ;
MR) | ( )v
xR H | ( )v
xR H ; | ( )v
xR H | ( )v
xR H .
M) |–Н –|Н; –|Н |–Н;
M) |–Н |–Н або |–Н; –|Н –|Н і –|Н;
M) |–хН існує уW: | ( )x
yR H ;
–|хН | ( )x
yR H для всіх уW;
M) |–Н |–Н для всіх S таких, що ;
–|Н –|Н для деякого S такого, що .
Теорема 4 (про контрмодель). Нехай – незамкнений шлях в секвенційному
дереві, Н – множина всіх специфікованих формул стану на шляху , M – об'єднання
усіх схем моделей світу секвенцій шляху , НM = ({Н | S}, M),
S
W W
, де кожна
W – множина предметних імен формул Н.
Тоді існують загальна ТМС M = (S, R, А, Iт) та VA з asn() = W такі:
|–Н () = Т; –|Н () = F.
Для переходу від нижчої вершини шляху до вищої використовується одна з
базових секвенційних форм. Переходи згідно таких форм відповідають пунктам
визначення системи модельних множин. Кожна непримітивна формула на шляху
рано чи пізно буде розкладена згідно відповідної форми. Всі секвенції шляху
незамкнені, тому для них не виконуються умови замкненості C, звідки для всіх
виконується умова коректності MС визначення системи модельних множин.
Візьмемо деяку множину А таку, що |А| = |W|, та ін'єктивну VA з asn() = W. Така
є бієкцією W на A. вона розпадається на бієкції : WA .
Кожна А продубльовує множину W всіх предметних імен Н.
Задамо значення базових предикатів на та на даних вигляду r ( )v
x :
|–EyН Ey() = Т, –|EyН Ey() = F;
|– рН р() = Т, –| рН р() = F;
| ( ) (r ( )) ( ) ( ) ;v v v
x x xR p H p R p T
| ( ) (r ( )) ( ) ( ) .v v v
x x xR p H p R p F
В інших випадках
Wd A
значення р(d) можна задавати довільним чином.
Для примітивних формул твердження теореми випливає з визначення значень
базових предикатів. Далі доводимо індукцією за складністю формули згідно побудови
системи модельних множин.
MRR) Нехай | ( ( ))v w
x yR R H . За визначенням НM тоді | ( )v w
x yR H . За
припущенням індукції ( ) ( ) ,v w
x yR T тому ( ( )) ( )v w
x yR R T .
Нехай | ( ( ))v w
x yR R H . За визначенням НM тоді | ( )v w
x yR H . За
припущенням індукції ( ) ( ) ,v w
x yR F тому ( ( )) ( )v w
x yR R F .
ISSN 1561-5359. Штучний інтелект, 2016, № 3
100 © О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко
MR) Нехай | ( )v
xR H . За визначенням НM тоді | ( )v
xR H . За
припущенням індукції ( ( )) ( ) ,v
xR T звідки ( ) ( )v
xR T .
Нехай | ( )v
xR H . За визначенням НM тоді | ( )v
xR H . За припущенням
індукції ( ( )) ( ) ,v
xR F звідки ( ) ( )v
xR F .
MR) Нехай | ( )v
xR H . Тоді | ( )v
xR H або | ( )v
xR H за визна-
ченням НM. За припущенням індукції маємо ( ) ( )v
xR T або ( ) ( )v
xR T , тому
( ) ( )v
xR T .
Нехай | ( )v
xR H . Тоді | ( )v
xR H та | ( )v
xR H за визначенням
НM. За припущенням індукції маємо ( ) ( )v
xR F та ( ) ( )v
xR F , тому
( ) ( )v
xR F .
MRs) Нехай | ( )v
xR y H , { , }y v x . Тоді | ( )v
xyR H за визначенням
НM. За припущенням індукції ( ) ( ) ,v
xyR T звідки ( ) ( )v
xR y T .
Нехай | ( )v
xR y H , { , }y v x . Тоді | ( )v
xyR H за визначенням НM. За
припущенням індукції маємо ( ) ( ) ,v
xyR F звідки ( ) ( )v
xR y F .
MR) Нехай | ( ) ,v
xR y H ( ( ))v
xz fu R x . Tоді | ( )v y
x zzR H за
визначенням НM. За припущенням індукції ( ) ( ) ,v y
x zzR T звідки маємо
( ) ( ) .v
xR y T
Нехай | ( )v
xR y H , ( ( ))v
xz fu R x . Tоді | ( )v y
x zzR H за визначенням
НM. За припущенням індукції ( ) ( ) ,v y
x zzR F тому ( ) ( ) .v
xR y F
MR) Нехай | ( )v
xR H . За визначенням НM тоді | ( )v
xR H . За при-
пущенням індукції ( ) ( ) ,v
xR T звідки ( ) ( ) .v
xR T
Нехай | ( )v
xR H . За визначенням НM тоді | ( )v
xR H . За припущенням
індукції ( ) ( )v
xR F , звідки ( ) ( )v
xR F .
M) Нехай |–Н. За визначенням НM маємо –|Н. За припущенням
індукції () = F, звідки ()() = Т.
Нехай –|Н. За визначенням НM маємо |–Н. За припущенням індукції
() = Т, звідки ()() = F.
M) Нехай |–Н. За визначенням НM маємо |–Н або |–Н. За
припущенням індукції () = Т або () = Т, звідки ()() = Т.
Нехай –|Н. За визначенням НM маємо –|Н та –|Н. За
припущенням індукції () = F та () = F, звідки ()() = F.
M) Нехай |–хН. За визначенням НM існує уW таке: | ( )x
yR H . За
припущенням індукції ( ) ( )x
yR T . Звідси (х(у)) = Т. Але (у)А згідно
уW, тому для а = (у)А маємо (ха) = Т, звідки (х)() = Т.
Нехай –|хН. За визначенням НM тоді | ( )x
yR H для всіх уW. За при-
пущенням індукції ( ) ( )x
yR F для всіх уW. Звідси (х(у)) = F для всіх
уW. Кожне bА має вигляд b = (у) для деякого уW, адже визначає бієкцію
ISSN 1561-5359. Штучний інтелект, 2016, № 3
© О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко 101
: WA. Звідси (хb) = F для всіх bА, тому (х)() = F.
M) Нехай |–Н. За визначенням НM маємо |–Н для всіх S таких, що
. За припущенням індукції () = Т для всіх станів таких, що . Звідси за
визначенням отримуємо ()() = T.
Нехай –|Н. За визначенням НM тоді –|Н для деякого S: . За
припущенням індукції () = F, тому ()() = F за визначенням .
Із теореми про контрмодель отримуємо теорему повноти.
Теорема 5. Нехай |= . Тоді секвенція |––| вивідна.
Припустимо супротивне: |= , тобто M|= для кожної узгодженої ТМС M, проте
секвенція = |––| невивідна. Тоді в дереві для існує незамкнений шлях. За теоремою 4
НM = ({Н | S}, M) – система модельних множин, тому існують ТМС M = (S, R, А, Jт) та
VA: |–Н () = Т та –|Н () = F. Зокрема, це вірно для формул секвенції |–
–|. Тому для всіх маємо () = Т та для всіх Ψ маємо Ψ() = F. Це заперечує
M|= , тому | . Отримали суперечність. Отже, припущення про невивідність |––|
невірне, що й доводить теорему.
Висновки
Вивчаються чисті першопорядкові композиційно-номінативні модальні логіки
часткових немонотонних предикатів. Для загальних транзиційних модальних логік
немонотонних предикатів побудовано і досліджено числення секвенційного типу. Такі
числення формалізують відношення неспростовнісного логічного наслідку для множин
специфікованих станами формул. Описано різновиди цих числень, для них наведено
базові секвенційні форми та умови замкненості секвенцій, доведено їх коректність та
повноту. Доведення теореми повноти опирається на теорему про існування
контрмоделі для незамкненого шляху в секвенційному дереві. Для побудови
контрмоделі використано метод систем модельних множин.
В наступних роботах планується побудова секвенційних числень модальних логік
часткових немонотонних предикатів, які формалізують відношення істиннісного,
хибнісного та сильного логічного наслідку.
Література
1. Cocchiarella N.B. Modal logic / N.B. Cocchiarella, M.A. Freund. – Oxford University Press, 2008. – 267 p.
2. Нікітченко М.С. Математична логіка та теорія алгоритмів / М.С. Нікітченко, С.С. Шкільняк. – К.:
ВПЦ Київський університет, 2008. – 528 с.
3. Нікітченко М.С. Прикладна логіка/М.С. Нікітченко, С.С. Шкільняк. – К.:ВПЦ Київ. університет, 2013.– 278 с.
4. Нікітченко М. С. Чисті першопорядкові логіки квазіарних предикатів / М. С. Нікітченко,
О. С. Шкільняк, С. С. Шкільняк // Пробл. програмування. – 2016. – № 2–3. – C. 73–86.
5. Шкільняк О.С. Транзиційні модальні логіки немонотонних квазіарних предикатів / О.С. Шкільняк //
Компьютерная математика. – 2014. – В. 2. – C. 99–110.
6. Шкільняк О.С. Mодальні логіки немонотонних часткових предикатів / О.С. Шкільняк // Вісник
Київського ун-ту. Серія: фіз.-мат. науки. – 2015. – Вип. 3. – C. 141–147.
7. Shkilniak O. Modal Logics of Partial Predicates without Monotonicity Restriction / O. Shkilniak // Workshop on
Foundations of Informatics: Proceedings FOI-2015. August 24–29, 2015, Chisinau, Moldova. – P. 198–211.
Literaturа
1. Cocchiarella N.B. Modal logic / N.B. Cocchiarella, M.A. Freund. – Oxford University Press, 2008. – 267 p.
2. Nikitchenko M.S. Matematychna lohika ta teoriya alhorytmiv / M.S. Nikitchenko, S.S. Shkil'nyak. – K.:
VPTs Kyyivs'kyy universytet, 2008. – 528 s.
3. Nikitchenko M.S. Prykladna lohika /M.S.Nikitchenko, S.S.Shkil'nyak.–K.:VPTs Kyyivs'kyy universytet, 2013.–278s.
4. Nikitchenko M. S. Chysti pershoporyadkovi lohiky kvaziarnykh predykativ / M. S. Nikitchenko, O. S.
Shkil'nyak, S. S. Shkil'nyak // Probl. prohramuvannya. – 2016. – # 2–3. – C. 73–86.
5. Shkil'nyak O.S. Tranzytsiyni modal'ni lohiky nemonotonnykh kvaziarnykh predykativ / O.S. Shkil'nyak //
Komp'yuternaya matematyka. – 2014. – V. 2. – C. 99–110.
6. Shkil'nyak O.S. Modal'ni lohiky nemonotonnykh chastkovykh predykativ / O.S. Shkil'nyak // Visnyk
Kyyivs'koho un-tu. Seriya: fiz.-mat. nauky. – 2015. – Vyp. 3. – C. 141–147.
7. Shkilniak O. Modal Logics of Partial Predicates without Monotonicity Restriction / O. Shkilniak // Workshop on
Foundations of Informatics: Proceedings FOI-2015. August 24–29, 2015, Chisinau, Moldova. – P. 198–211.
ISSN 1561-5359. Штучний інтелект, 2016, № 3
102 © О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко
RESUME
O. Shkilniak, V. Kasianiuk, L. Malutenko
Completeness of sequent calculi for modal logics of non-monotone partial predicates
Modal logics are successfully used in computer science and programming. Composition
nominative modal logics (CNML) combine facilities of traditional modal logics and composition
nominative logics of quasiary predicates. Modal transitional logics (MTL) are an important
variant of CNML, they represent the fact of changing and evolution in subject domains. In this
paper we study first-order MTL of partial quasiary predicates without monotonicity restrictions.
Sequent (Gentzen) calculi are an effective formal deduction system. In this paper we
propose sequent calculi for pure first-order general MTL of non-monotone partial predicates.
Sequent calculi are a formalization of logical consequence for sets of formulas. These calculi are
constructed basing on properties of logical consequence relations for sets of state-specified
formulas. We describe a number of variants of the introduced calculi, their basic sequent forms
and sequent closure conditions. The key parts of this paper are proofs of the soundness and
completeness theorems for the proposed calculi.
Soundness theorem. Let a sequent |––| is derivable. Then |= .
The proof of the completeness theorem is based on the theorem about existence of a
counter-model a non-closed path in a sequent tree. For the construction of the counter-model we
use the Hintikka sets method.
Theorem about a counter-model. Let is a non-closed path in the sequent tree, Н is a
set of specified with |– or –| formulas of sequents of the path , M is a union of all the schemes
of models of the universe of the path , let НM = ({Н | S}, M), W is union of sets of variables
of formulas of Н. Then exist MTS M = (S, R, А, Jт) and VA with asn() = nт(W) such that:
|–Н () = Т; –|Н () = F.
Completeness theorem. Let |= . Then a sequent |––| is derivable.
Надійшла до редакції 05.11.2016
|