Властивості відношень логічного наслідку в логіках квазіарних предикатів
У статті досліджено відношення логічного наслідку для множин формул у чистих першопорядкових композиційно-номінативних логіках часткових однозначних, тотальних неоднозначних та часткових не- однозначних предикатів. Основна увага приділена вивченню властивостей відношень, пов’язаних з елімінацією...
Gespeichert in:
| Datum: | 2013 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
Інститут проблем штучного інтелекту МОН України та НАН України
2013
|
| Schriftenreihe: | Искусственный интеллект |
| Schlagworte: | |
| Online Zugang: | http://dspace.nbuv.gov.ua/handle/123456789/85208 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Властивості відношень логічного наслідку в логіках квазіарних предикатів / С.С. Шкільняк // Искусственный интеллект. — 2013. — № 1. — С. 67–78. — Бібліогр.: 7 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-85208 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-852082015-07-22T03:02:04Z Властивості відношень логічного наслідку в логіках квазіарних предикатів Шкільняк, С.С. Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем У статті досліджено відношення логічного наслідку для множин формул у чистих першопорядкових композиційно-номінативних логіках часткових однозначних, тотальних неоднозначних та часткових не- однозначних предикатів. Основна увага приділена вивченню властивостей відношень, пов’язаних з елімінацією кванторів. Для опису таких властивостей використано спеціальні предикати, які визначають наявність значення для змінних. В статье исследованы отношения логического следствия для множеств формул в чистых первопорядковых композиционно-номинативных логиках частичных однозначных, тотальных неоднозначных и частичных неоднозначных предикатов. Основное внимание уделено изучению свойств отношений, связанных с элиминацией кванторов. Для описания таких свойств использованы специальные предикаты, опреде- ляющие наличие значений для переменных. Logical consequence relation for sets of formulas is studied for pure first-order composition-nominative logics of partial single-valued, total and partial multiple-valued predicates. We focus on the properties of relations concerned with quantifier elimination. Special variable definedness predicates are used for description of such properties. 2013 Article Властивості відношень логічного наслідку в логіках квазіарних предикатів / С.С. Шкільняк // Искусственный интеллект. — 2013. — № 1. — С. 67–78. — Бібліогр.: 7 назв. — укр. 1561-5359 http://dspace.nbuv.gov.ua/handle/123456789/85208 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 |
2013 |
| topic_facet |
Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/85208 |
| citation_txt |
Властивості відношень логічного наслідку в логіках квазіарних предикатів / С.С. Шкільняк // Искусственный интеллект. — 2013. — № 1. — С. 67–78. — Бібліогр.: 7 назв. — укр. |
| series |
Искусственный интеллект |
| work_keys_str_mv |
AT škílʹnâkss vlastivostívídnošenʹlogíčnogonaslídkuvlogíkahkvazíarnihpredikatív |
| first_indexed |
2025-07-06T12:22:23Z |
| last_indexed |
2025-07-06T12:22:23Z |
| _version_ |
1836900201213722624 |
| fulltext |
ISSN 1561-5359 «Штучний інтелект» 2013 № 1 67
2Ш
УДК 004.42:510.69
С.С. Шкільняк
Київський національний університет імені Тараса Шевченка, Україна
Україна, 01601, м. Київ, вул. Володимирська, 60
Властивості відношень логічного наслідку
в логіках квазіарних предикатів
S.S. Shkilnak
Taras Shevchenko National University of Kyiv
Ukraine, 01601, Kyiv, Volodymyrska st., 60
Properties of Logical Consequence Relations
in Logics of Quasi-Ary Predicates
С.С. Шкильняк
Киевский национальный университет имени Тараса Шевченко, Украина
Украина, 01601, г. Киев, ул. Владимирская, 60
Cвойства отношений логического следствия
в логиках квазиарных предикатов
У статті досліджено відношення логічного наслідку для множин формул у чистих першопорядкових
композиційно-номінативних логіках часткових однозначних, тотальних неоднозначних та часткових не-
однозначних предикатів. Основна увага приділена вивченню властивостей відношень, пов’язаних з
елімінацією кванторів. Для опису таких властивостей використано спеціальні предикати, які визначають
наявність значення для змінних.
Ключовi слова: логіка, предикат, квантор, логічний наслідок.
Logical consequence relation for sets of formulas is studied for pure first-order composition-nominative logics of
partial single-valued, total and partial multiple-valued predicates. We focus on the properties of relations concerned
with quantifier elimination. Special variable definedness predicates are used for description of such properties.
Key words: logic, predicate, quantifier, logical consequence.
В статье исследованы отношения логического следствия для множеств формул в чистых первопорядковых
композиционно-номинативных логиках частичных однозначных, тотальных неоднозначных и частичных
неоднозначных предикатов. Основное внимание уделено изучению свойств отношений, связанных с
элиминацией кванторов. Для описания таких свойств использованы специальные предикаты, опреде-
ляющие наличие значений для переменных.
Ключевые слова: логика, предикат, квантор, логическое следствие.
Вступ
Поняття і методи математичної логіки доводять свою ефективність при розв’язан-
ні широкого кола задач інформатики й програмування [1]. Водночас таке використання
вимагає зробити логіку ближчою і адекватнішою до потреб програмування й моделю-
вання. В основі різноманітних прикладних логічних систем зазвичай лежить класична
логіка предикатів. Проте така логіка має принципові обмеження, що ускладнює її ви-
користання. Тому першочерговою постає проблема побудови нових, програмно-
орієнтованих логічних формалізмів. Природною основою такої побудови є спільний
Шкільняк С.С.
«Искусственный интеллект» 2013 № 1 68
2Ш
для логіки й програмування композиційно-номінативний підхід. Логіки, побудовані
на його базі, названо композиційно-номінативними (КНЛ), вони досліджені, зокрема, в
роботах [2-7].
Поняття логічного слідування є центральним поняттям логіки. Формалізація ло-
гічного слідування в КНЛ квазіарних предикатів за допомогою відношень логічного
наслідку запропонована в [3]. Досліджено [3-6] такі «природні» відношення: «істинніс-
ний» |=T, «хибнісний» |=F, «сильний» |=TF, «неспростовнісний» |=Cl, «насичений» |=Cm
логічні наслідки. Усі вони збігаються в класичній логіці, яка є логікою тотальних
однозначних предикатів. Для логік однозначних часткових предикатів (неокласична
семантика) можна розглядати відношення |=T, |=F, |=TF, |=Cl. Традиційним для цих логік є
|=Cl. Для логік тотальних неоднозначних предикатів (пересичена семантика, дуальна до
неокласичної) розглядаємо |=T, |=F, |=TF, |=Cm. Для логік часткових неоднозначних пре-
дикатів (загальна семантика) маємо єдине змістовне відношення |=TF, із ним збігаються |=T
та |=F. Властивості відношень логічного наслідку для множин формул є семантичною
основою побудови числень секвенційного типу.
Метою даної статті є дослідження відношень логічного наслідку для множин
формул в чистих першопорядкових КНЛ (ЧКНЛ) часткових однозначних, тотальних
неоднозначних та часткових неоднозначних предикатів. Основна увага приділена
вивченню властивостей цих відношень, пов’язаних з елімінацією кванторів. Для опи-
су таких властивостей використано спеціальні предикати, які визначають наявність
значення для змінних.
Поняття, які тут не визначаються, тлумачимо в сенсі робіт [2-6]. Будемо дотри-
муватись позначень роботи [6], продовженням якої є дана стаття.
Відношення логічного наслідку
Для полегшення читання наведемо основні визначення та позначення.
Область істинності й область хибності V-квазіарного предиката P :
V
A→{T, F} –
це множини T(P) = {d∈V
A | T∈P(d)} та F(P) = {d∈V
A | F∈P(d)}.
Якщо Р однозначний, то T(P)∩F(P) = ∅; якщо Р тотальний, то T(P)∪F(P) =
V
A.
Мова ЧКНЛ визначається так. Алфавіт мови: символи , , ,
v
x
R x¬ ∨ ∃ базових ком-
позицій; множини Ps предикатних символів (сигнатура мови) та V предметних імен.
Множина Fr формул мови ЧКНЛ визначається індуктивно.
1) Кожний р∈Ps є формулою; такі формули атомарні.
2) Нехай Φ та Ψ – формули. Тоді ¬Φ, ∨ФΨ, v
x
R Φ , ∃xΦ – формули.
Моделями мови ЧКНЛ є алгебраїчні системи з доданою сигнатурою вигляду
((A, Pr
A
), I). Тут Pr
A
– клас V-квазіарних предикатів над A, а тотальне однозначне
I : Ps → Pr
A
задає відображення інтерпретації формул J : Fr→Pr
A
:
1) J(р) = I(p) для кожного р∈Ps.
2) J(¬Φ) = ¬(J(Φ)), J(∨ΦΨ) = ∨(J(Φ), J(Ψ)), J ( )
v
x
R Φ = R
v
x
(J(Φ)), J(∃xΦ) = ∃x(J(Φ)).
Предикат J(Φ) позначаємо ΦA .
Характерною ознакою логіки квазіарних предикатів є те, що значення предика-
та P(d) може бути різним залежно від того, входить чи не входить до d компонента з
певним предметним іменем. Це веде до того, що для цих логік вже невірні [3-6] деякі
важливі закони класичної логіки. Тому при інтерпретаціях формул варто явно вказу-
вати означені та неозначені предметні імена. Це робимо за допомогою запропоно-
Властивості відношень логічного наслідку в логіках квазіарних предикатів
«Штучний інтелект» 2013 № 1 69
2Ш
ваних в [7] спеціальних 0-арних композицій – параметризованих за предметними
іменами предикатів εz, які визначають наявність в даних компоненти з відповідним
іменем z. Називатимемо їх індикаторами наявності значення для предметного імені.
Предикати-індикатори εz визначаємо так:
T(εzA) = {d | d(z)↑} = {d∈V
A | z∉asn(d)};
F(εzA) = {d | d(z)↓} = {d∈V
A | z∈asn(d)}.
Теорема 1.
,
,
( ( ))
u x
v y
T R P ∩ F(εy) ⊆ ( ( ))
u
v
T R xP∃ та ( ( ))
u
v
F R xP∃ ∩ F(εy) ⊆
,
,
( ( ))
u x
v y
F R P .
Доведення. Нехай ,
,
( ( ))
u x
v y
d T R P∈ ∩ F(εy), тоді d(y)↓ та ,
,
( ( ))
u x
v y
d T R P∈ . Нехай
d(y) = a, тоді ( ) ( ) ( ) ( )d u d v x d y d u d v x a T P∇ ∇ = ∇ ∇ ∈a a a a для такого a∈A,
звідки
( ) ( ),
u
v
r d T xP∈ ∃ тому ( ( ))
u
v
d T R xP∈ ∃ . Отже, ,
,
( ( ))
u x
v y
T R P ∩ F(εy) ⊆ ( ( ))
u
v
T R xP∃ .
Нехай ( ( ))
u
v
d F R xP∈ ∃ ∩ F(εy), тоді d(y)↓ та ( ( )).
u
v
d F R xP∈ ∃ Із останнього
маємо ( ) ( ),d u d v F xP∇ ∈ ∃a тому ( ) ( )d u d v x b F P∇ ∇ ∈a a для всіх b∈A. Нехай
d(y) = a, для такого a∈A маємо ( ) ( ) ( ) ( ),d u d v x a d u d v x d y F P∇ ∇ = ∇ ∇ ∈a a a a
звідки d∈F ,
,
( ( ))
u x
v y
R P . Отже, F ( ( ))
u
v
R xP∃ ∩ F(εy) ⊆ F
,
,
( ( ))
u x
v y
R P .
Наслідок 1. ( ( ))
x
y
T R P ∩ F(εy) ⊆ T(∃xР) та F(∃xР) ∩ F(εy) ⊆ ( ( ))
x
y
F R P .
Далі розглядаємо ЧКНЛ, в яких мови розширені за допомогою множини символів
предикатів-індикаторів {εx | x∈V}. Такі розширені логіки назвемо ε-ЧКНЛ, вони зада-
ють окремий підрівень кванторного рівня із базовими композиціями ¬, ∨, R ,
v
x
∃x, εx.
Задамо відношення наслідку для двох формул при інтерпретації на моделі мови A:
1) «істиннісний» наслідок A|=T : Φ A|=T Ψ ⇔ T(ΦA) ⊆ T(ΨA);
2) «хибнісний» наслідок A|=F : Φ A|=F Ψ ⇔ F(ΨA) ⊆ F(ΦA);
3) «сильний» наслідок A|=TF : Φ A|=TF Ψ ⇔ T(ΦA) ⊆ T(ΨA) та F(ΨA) ⊆ F(ΦA);
4) «неспростовнісний» наслідок A|=Cl : Φ A|=Cl Ψ ⇔ T(ΦA)∩F(ΨA) = ∅;
5) «насичений» наслідок A|=Cm : Φ A|=Cm Ψ ⇔ F(ΦA)∪T(ΨA) = D.
Відповідні відношення логічного наслідку для двох формул |=T, |=F, |=TF, |=Cl,
|=Cm визначаємо за такою схемою:
Φ |=∗ Ψ ⇔ Φ A|=∗ Ψ для кожної моделі мови A.
Для класичної логіки скінченно-арних тотальних однозначних предикатів від-
ношення |=Cl, |=Cm, |=T, |=F, |=TF збігаються.
Для логік часткових однозначних предикатів (неокласична семантика) можна
розглядати |=Cl, |=T, |=F, |=TF, відношення |=Cm тут порожнє.
Для логік тотальних неоднозначних предикатів (пересичена семантика) можна
розглядати |=Cm, |=T, |=F, |=TF, відношення |=Cl порожнє.
Для логік часткових тотальних неоднозначних предикатів (загальна семанти-
ка) відношення |=T, |=F, |=TF збігаються, відношення |=Cl та |=Cm порожні.
Відношення еквівалентності A∼T, A∼F, A∼TF, A∼Cl, A∼Cm в моделі мови A та
відношення логічної еквівалентності ∼T, ∼F, ∼TF, ∼Cl, ∼Cm визначаємо за схемою:
Φ A∼∗ Ψ, якщо Φ A|=∗ Ψ та Ψ A|=∗ Φ;
Φ ∼∗ Ψ, якщо Φ |=∗ Ψ та Ψ |=∗ Φ.
Для кожної A маємо: Φ A∼TF Ψ ⇔ T(ΦA) = T(ΨA) та F(ΨA) = F(ΦA), тобто ΦA = ΨA.
Тому Φ ∼TF Ψ означає, що Φ та Ψ завжди інтерпретуються як один і той же предикат.
У відповідних семантиках для ∼Cl, ∼Cm, ∼TF справджується теорема семантичної
Шкільняк С.С.
«Искусственный интеллект» 2013 № 1 70
2Ш
еквiвалентності, водночас [4] для ∼T та ∼F вона невірна (тут ∗ – одне з Cl, Cm, TF).
Теорема 2. Нехай формула Φ', отримана з Φ заміною деяких входжень формул
Φ1, ..., Φn на Ψ1, ..., Ψn вiдповiдно. Якщо Φ1 ∼∗ Ψ1, ..., Φn ∼∗ Ψn, то Φ ∼∗ Φ'.
Поширимо поняття наслідку на множини формул. Нехай Γ⊆ Fr та ∆ ⊆ Fr.
Γ A|=T ∆, якщо ( ) ( )
A A
T T
Φ∈Γ Ψ∈∆
Φ ⊆ ΨI U .
Γ A|=F ∆, якщо ( ) ( )
A A
F F
Ψ∈∆ Φ∈Γ
Ψ ⊆ ΦI U .
Γ A|=TF ∆, якщо ( ) ( )
A A
T T
Φ∈Γ Ψ∈∆
Φ ⊆ ΨI U та ( ) ( )
A A
F F
Ψ∈∆ Φ∈Γ
Ψ ⊆ ΦI U .
Γ A|=Cl ∆, якщо ( ) ( )
A A
T F
Φ∈Γ Ψ∈∆
Φ ∩ Ψ =∅I I .
Γ A|=Cm ∆, якщо ( ) ( )
V
A A
F T A
Φ∈Γ Ψ∈∆
Φ ∪ Ψ =U U .
Відношення логічного наслідку для множин формул |=T , |=F , |=TF , |=Cl , |=Cm
визначаємо за такою схемою:
Γ |=∗ ∆, якщо Γ A|=∗ ∆ для кожної моделі мови A.
У відповідних семантиках справджується
Теорема 3 (заміни еквівалентних). Нехай Φ ∼TF Ψ. Тоді маємо:
Φ, Γ |=∗ ∆ ⇔ Ψ, Γ |=∗ ∆ та Γ |=∗ ∆, Φ ⇔ Γ |=∗ ∆, Ψ.
Тут і надалі, якщо інше окремо не зазначено, |=∗ позначає:
– одне із |=T, |=F, |=TF, |=Cl – для неокласичної семантики;
– одне із |=T, |=F, |=TF, |=Cm – для пересиченої семантики;
– |=TF – для загальної семантики.
До основних властивостей відношень логічного наслідку для множин формул
найперше віднесемо такі:
U) Нехай Γ ⊆ Λ та ∆ ⊆ Σ, тоді Γ |=∗ ∆ ⇒ Λ |=∗ Σ.
C) Якщо Γ∩∆ ≠ ∅, то Γ |=∗ ∆.
Властивість С гарантує наявність кожного із введених логічних наслідків у
відповідних семантиках.
Додатково гарантують наявність відповідного логічного наслідку властивості:
СL) Φ, ¬Φ, Γ |=∗ ∆
(для неокласичної семантики |=∗ – це |=T або |=Cl ; для пересиченої – це |=F або |=Cm );
СR) Γ |=∗ ∆, Φ, ¬Φ
(для неокласичної семантики |=∗ – це |=F або |=Cl ; для пересиченої – це |=T або |=Cm );
СLR) Φ, ¬Φ, Γ |=TF ∆, Ψ, ¬Ψ (для неокласичної або для пересиченої семантики).
Для |=Cl та |=Cm властивості СL, СR, СLR зводяться до С.
До базових властивостей пропозиційного рівня віднесемо:
¬¬|– ) ¬¬Φ, Γ |=∗ ∆ ⇔ Φ, Γ |=∗ ∆;
¬¬–| ) Γ |=∗ ∆, ¬¬Φ ⇔ Γ |=∗ ∆, Φ;
∨|– ) Φ∨Ψ, Γ |=∗ ∆ ⇔ Φ, Γ |=∗ ∆ та Ψ, Γ |=∗ ∆;
∨–| ) Γ |=∗ ∆, Φ∨Ψ ⇔ Γ |=∗ ∆, Φ, Ψ;
¬∨|– ) ¬(Φ∨Ψ), Γ |=∗ ∆ ⇔ ¬Φ, ¬Ψ, Γ |=∗ ∆;
¬∨–| ) Γ |=∗ ∆, ¬(Φ∨Ψ) ⇔ Γ |=∗ ∆, ¬Φ та Γ |=∗ ∆, ¬Ψ.
Для |=Cl (неокласична семантика) та |=Cm (пересичена семантика) також маємо:
Властивості відношень логічного наслідку в логіках квазіарних предикатів
«Штучний інтелект» 2013 № 1 71
2Ш
¬|– ) ¬Φ, Γ |=∗ ∆ ⇔ Γ |=∗ ∆, Φ;
¬–| ) Γ |=∗ ∆, ¬Φ ⇔ Φ, Γ |=∗ ∆.
Це означає, що для |=Cl та |=Cm можна знімати зовнішнє заперечення, перенося-
чи формулу з лівої частини у праву і навпаки. Проте це не можна робити [2], [5] для
|=T, |=F та |=TF, для цих наслідків властивості ¬|– та ¬–| невірні.
Наведемо базові властивості реномінативного і кванторного рівнів.
RT|–)
,
,
( ),
z v
z x
R Φ Γ |=∗ ∆ ⇔ ( ),
v
x
R Φ Γ |=∗ ∆;
RT–|) Γ |=∗ ∆, ,
,
( )
z v
z x
R Φ ⇔ Γ |=∗ ∆, ( );
v
x
R Φ
¬RT|–)
,
,
( ),
z v
z x
R¬ Φ Γ |=∗ ∆ ⇔ ( ),
v
x
R¬ Φ Γ |=∗ ∆;
¬RT–|) Γ |=∗ ∆, ,
,
( )
z v
z x
R¬ Φ ⇔ Γ |=∗ ∆, ( );
v
x
R¬ Φ
ΦN|–)
,
,
( ),
y v
z x
R Φ Γ |=∗ ∆ ⇔ ( ),
v
x
R Φ Γ |=∗ ∆;
ΦN–|) Γ |=∗ ∆, ,
,
( )
y v
z x
R Φ ⇔ Γ |=∗ ∆, ( )
v
x
R Φ (тут у∈ν(Φ));
¬ΦN|–)
,
,
( ),
y v
z x
R¬ Φ Γ |=∗ ∆ ⇔ ( ),
v
x
R¬ Φ Γ |=∗ ∆;
¬ΦN–|) Γ |=∗ ∆, ,
,
( )
y v
z x
R¬ Φ ⇔ Γ |=∗∆, ( )
v
x
R¬ Φ (тут у∈ν(Φ);
RR|–) ( ( )),
v w
x y
R R Φ Γ |=∗ ∆ ⇔ ( ),
v w
x y
R Φ Γo |=∗ ∆;
RR–|) Γ |=∗ ∆, ( ( ))
v w
x y
R R Φ ⇔ Γ |=∗ ∆, ( );
v w
x y
R Φo
¬RR|–) ( ( )),
v w
x y
R R¬ Φ Γ |=∗ ∆ ⇔ ( ),
v w
x y
R¬ Φ Γo |=∗ ∆;
¬RR–|) Γ |=∗ ∆, ( ( ))
v w
x y
R R¬ Φ ⇔ Γ |=∗ ∆, ( );
v w
x y
R¬ Φo
R¬|–) ( ),
v
x
R ¬Φ Γ |=∗ ∆ ⇔ ( ),
v
x
R¬ Φ Γ |=∗ ∆;
R¬–|) Γ |=∗ ∆, ( )
v
x
R ¬Φ ⇔ Γ |=∗ ∆, ( );
v
x
R¬ Φ
¬R¬|–) ( ),
v
x
R¬ ¬Φ Γ |=∗ ∆ ⇔ ( ),
v
x
R Φ Γ |=∗ ∆;
¬R¬–|) Γ |=∗ ∆, ( )
v
x
R¬ ¬Φ ⇔ Γ |=∗ ∆, ( );
v
x
R Φ
R∨|–) ( ),
v
x
R Φ∨Ψ Γ |=∗ ∆ ⇔ ( ) ( ),
v v
x x
R RΦ ∨ Ψ Γ |=∗ ∆;
R∨–|) Γ |=∗ ∆, ⇔ Γ |=∗ ∆, ( ) ( );
v v
x x
R RΦ ∨ Ψ
¬R∨|–) ( ),
v
x
R¬ Φ∨Ψ Γ |=∗ ∆ ⇔ ( ), ( ),
v v
x x
R R¬ Φ ¬ Ψ Γ |=∗ ∆;
¬R∨–|) Γ |=∗ ∆, ( )
v
x
R¬ Φ∨Ψ ⇔ Γ |=∗ ∆, ( )
v
x
R¬ Φ та Γ |=∗ ∆, ( );
v
x
R¬ Ψ
R∃R|–)
,
,
( ),
u x
v y
R x∃ Φ Γ |=∗ ∆ ⇔ ( ),
u
v
R x∃ Φ Γ |=∗ ∆;
R∃R–|) Γ |=∗ ∆, ,
,
( )
u x
v y
R x∃ Φ ⇔ Γ |=∗ ∆, ( );
u
v
R x∃ Φ
R∃p|–) ( ),
x
y
R x∃ Φ Γ |=∗ ∆ ⇔ ∃хΦ, Γ |=∗ ∆;
R∃p–|) Γ |=∗ ∆, ( )
x
y
R x∃ Φ ⇔ Γ |=∗ ∆, ∃хΦ;
¬R∃R|–)
,
,
( ),
u x
v y
R x¬∃ Φ Γ |=∗ ∆ ⇔ ( ),
u
v
R x¬∃ Φ Γ |=∗ ∆;
¬R∃R–|) Γ |=∗ ∆, ,
,
( )
u x
v y
R x¬∃ Φ ⇔ Γ |=∗ ∆, ( );
u
v
R x¬∃ Φ
¬R∃p|–) ( ),
x
y
R x¬∃ Φ Γ |=∗ ∆ ⇔ ¬∃хΦ, Γ |=∗ ∆;
¬R∃p–|) Γ |=∗ ∆, ( )
x
y
R x¬∃ Φ ⇔ Γ |=∗ ∆, ¬∃хΦ.
Шкільняк С.С.
«Искусственный интеллект» 2013 № 1 72
2Ш
Властивості елімінації кванторів
Розглянемо властивості, пов’язані з елімінацією кванторів, зокрема, властивості
елімінації кванторів під реномінацією. У випадку Γ A|= ∆ будемо надалі позначати
( )
A
T
Φ∈Γ
ΦI як T(ΓA), ( )
A
T
Ψ∈∆
ΨU як T(∆A), ( )
A
F
Φ∈Γ
ΦU як F(ΓA), ( )
A
F
Ψ∈∆
ΨI як F(∆A).
Множину тотально (строго) неістотних імен позначаємо VT .
Теорема 4. При умові z∈VT та ( , , ( ))
u
v
z nm R x∉ Γ ∆ ∃ Φ маємо:
( ),
u
v
R x∃ Φ Γ |=∗ ∆ ⇔ ,
,
( ),
u x
v z
R Φ Γ |=∗ ∆, εz (тут ∗ може бути Cl, Cm, T, F, TF ).
Випадок |=Cl .
Доводимо ⇒. Нехай ( ),
u
v
R x∃ Φ Γ |=Cl ∆, тоді T(ΓA) ( ( ) )
u
v A
T R x∩ ∃ Φ ∩ F(∆A) = ∅.
Згідно з теоремою 1 маємо ,
,
( ( ) )
u x
v z A
T R Φ ∩F(εzA) ⊆ ( ( ) )
u
v A
T R x∃ Φ , тому T(ΓA) ∩ F(∆A) ∩
,
,
( ( ) )
u x
v z A
T R∩ Φ ∩F(εzA) = ∅. Отже, ,
,
( ),
u x
v z
R Φ Γ |=Cl ∆, εz.
Доводимо ⇐. Нехай ,
,
( ),
u x
v z
R Φ Γ |=Cl ∆, εz, звідси T(ΓA) ,
,
( ( ) )
u x
v z A
T R∩ Φ ∩F(∆A) ∩
∩ F(εzA) = ∅. Покажемо, що тоді T(ΓA) ( ( ) )
u
v A
T R x∩ ∃ Φ ∩ F(∆A) = ∅, звідки отримаємо
( ),
u
v
R x∃ Φ Γ |=Cl ∆. Припустимо супротивне: T(ΓA) ,
,
( ( ) )
u x
v z A
T R∩ Φ ∩F(∆A) ∩ F(εzA) = ∅ та
існує d∈V
A таке, що d∈T(ΓA) ( ( ) )
u
v A
T R x∩ ∃ Φ ∩ F(∆A). Маємо ( ( ) ),
u
v A
d T R x∈ ∃ Φ d∈T(ΓA)
та d∈F(∆A). Із умови ( ( ) )
u
v A
d T R x∈ ∃ Φ маємо ( ) ( ),
A
d u d v T x∇ ∈ ∃ Φa звідки
( ) ( )
A
d u d v x a T∇ ∇ ∈ Φa a для деякого a∈A. Але z∈VT та ( , , ( )),
u
v
z nm R x∉ Γ ∆ ∃ Φ
тому ( ) ( ),
A
d u d v x a z a T∇ ∇ ∇ ∈ Φa a a d∇zaa∈T(ΓA), d∇zaa∈F(∆A). Із останнього
отримуємо ,
,
( ( ) ),
u x
v z A
d z a T R∇ ∈ Φa за визначенням εz маємо d∇zaa∈F(εzA), тому
отримуємо ,
,
( ) ( ( ) )
u x
A v z A
d z a T T R∇ ∈ Γ ∩ Φ ∩a F(∆A) ∩ F(εzA), що суперечить нашому
припущенню ,
,
( ) ( ( ) )
u x
A v z A
T T RΓ ∩ Φ ∩F(∆A) ∩ F(εzA) = ∅.
Випадок |=Cm . Доведення проводиться подібно доведенню для |=Cl.
Випадок |=T . Доводимо ⇒. Треба показати:
( ( ) )
u
v A
T R x∃ Φ ∩T(ΓA) ⊆ T(∆A) ⇒ ,
,
( ( ) )
u x
v z A
T R Φ ∩T(ΓA) ⊆ T(∆A) ∪ T(εzA).
За теоремою 1 маємо ,
,
( ( ) )
u x
v z A
T R Φ ∩F(εzA) ⊆ ( ( ) ),
u
v A
T R x∃ Φ звідси та з умови
( ( ) )
u
v A
T R x∃ Φ ∩T(ΓA) ⊆ T(∆A) отримуємо: ,
,
( ( ) )
u x
v z A
T R Φ ∩F(εzA) ∩ T(ΓA) ⊆ T(∆A) ⇒
⇒ ,
,
( ( ) )
u x
v z A
T R Φ ∩F(εzA) ∩ T(ΓA)) ∪ T(εzA) ⊆ T(∆A)∪ T(εzA) ⇒
⇒ ,
,
(( ( ( ) )
u x
v z A
T R Φ ∩T(ΓA)) ∪ T(εzA)) ∩ (F(εzA) ∪ T(εzA)) ⊆ T(∆A)∪ T(εzA), звідки
,
,
( ( ( ) )
u x
v z A
T R Φ ∩T(ΓA)) ∪ T(εzA) ⊆ T(∆A)∪ T(εzA) ⇒ ,
,
( ( ) )
u x
v z A
T R Φ ∩T(ΓA)) ⊆ T(∆A)∪ T(εzA).
Доводимо ⇐. Треба показати:
,
,
( ( ) )
u x
v z A
T R Φ ∩T(ΓA) ⊆ T(∆A) ∪ T(εzA) ⇒ ( ( ) )
u
v A
T R x∃ Φ ∩T(ΓA) ⊆ T(∆A).
Нехай (1) – це умова ,
,
( ( ) )
u x
v z A
T R Φ ∩T(ΓA) ⊆ T(∆A) ∪ T(εzA). Припустимо супро-
тивне: (1) та невірно ( ( ) )
u
v A
T R x∃ Φ ∩T(ΓA) ⊆ T(∆A). Із останнього маємо: існує d∈V
A
Властивості відношень логічного наслідку в логіках квазіарних предикатів
«Штучний інтелект» 2013 № 1 73
2Ш
таке, що ( ( ) ),
u
v A
d T R x∈ ∃ Φ d∈T(ΓA), d∉T(∆A). Із умови ( ( ) )
u
v A
d T R x∈ ∃ Φ отримуємо
( ) ( )
A
d u d v x a T∇ ∇ ∈ Φa a для деякого a∈A. Але z∈VT та ( , , ( )),
u
v
z nm R x∉ Γ ∆ ∃ Φ тому
маємо ( ) ( ),
A
d u d v x a z a T∇ ∇ ∇ ∈ Φa a a ( ( ) ),u
v A
d z a T R x∇ ∈ ∃ Φa d∇zaa∈T(ΓA),
d∇zaa∉T(∆A). Із першої умови тоді ,
,
( ( ) ),
u x
v z A
d z a T R∇ ∈ Φa звідси, враховуючи
d∇zaa∈F(εzA), маємо ,
,
( ( ) ) ( )
u x
v z A A
d z a T R T∇ ∈ Φ ∩ Γa та d∇zaa∉T(∆A) ∪ T(εzA). Це
суперечить умові ,
,
( ( ) )
u x
v z A
T R Φ ∩T(ΓA) ⊆ T(∆A) ∪ T(εzA).
Випадок |=F . Доводимо ⇒. Треба показати:
F(∆A) ⊆ ( ( ) )
u
v A
F R x∃ Φ ∪F(ΓA) ⇒ F(εzA) ∩ F(∆A) ⊆
,
,
( ( ) )
u x
v z AF R Φ ∪ F(ΓA).
За теоремою 1 маємо ( ( ) )
u
v A
F R x∃ Φ ∩F(εzA) ⊆
,
,
( ( ) ),
u x
v z A
F R Φ звідси та з умови
F(∆A) ⊆ ( ( ) )
u
v A
F R x∃ Φ ∪F(ΓA) маємо: F(∆A) ∩ F(εzA) ⊆ ( ( ( ) )
u
v A
F R x∃ Φ ∪F(ΓA)) ∩ F(εzA) ⇒
⇒ F(∆A) ∩ F(εzA) ⊆ ( ( ( ) )
u
v A
F R x∃ Φ ∩F(εzA)) ∪ (F(ΓA)) ∩ F(εzA)) ⇒ F(∆A) ∩ F(εzA) ⊆
⊆ ,
,
( ( ))
u x
v yF R P ∪ (F(ΓA)) ∩ F(εzA)) ⇒ F(∆A) ∩ F(εzA) ⊆
,
,
( ( ) )
u x
v z AF R Φ ∪ F(ΓA).
Доводимо ⇐. Треба показати:
F(εzA) ∩ F(∆A) ⊆
,
,
( ( ) )
u x
v z AF R Φ ∪ F(ΓA) ⇒ F(∆A) ⊆ ( ( ) )
u
v A
F R x∃ Φ ∪F(ΓA).
Нехай (1) – це умова F(εzA) ∩ F(∆A) ⊆
,
,
( ( ) )
u x
v z AF R Φ ∪ F(ΓA). Припустимо супро-
тивне: (1) та невірно F(∆A) ⊆ ( ( ) )
u
v A
F R x∃ Φ ∪F(ΓA). Із останнього маємо: існує d∈V
A
таке, що d∈F(∆A), d∉F(ΓA), ( ( ) ).
u
v A
d F R x∉ ∃ Φ Із останнього маємо, що для деякого
a∈A, тоді ( ) ( ).
A
d u d v x a F∇ ∇ ∉ Φa a Але z∈VT та ( , , ( )),
u
v
z nm R x∉ Γ ∆ ∃ Φ тому
d∇zaa∈F(∆A), d∇zaa∉F(ΓA), ( ) ( ).Ad u d v x a z a F∇ ∇ ∇ ∉ Φa a a Останнє означає
d∇zaa∉ ,
,
( ( ) ).
u x
v z AF R Φ Враховуючи d∇zaa∈F(εzA), тоді d∇zaa∈F(εzA) ∩ F(∆A) та
d∇zaa∉ ,
,
( ( ) )
u x
v z AF R Φ ∪ F(ΓA). Це суперечить F(εzA) ∩ F(∆A) ⊆
,
,
( ( ) )
u x
v z AF R Φ ∪ F(ΓA).
Випадок |=TF . Доводячи ⇒ для |=T та |=F так, як описано вище, отримуємо ⇒
для |=TF . Доводячи ⇐ для |=T та |=F так, як описано вище, отримуємо ⇐ для |=TF .
Наслідок 2. При умові z∈VT та z∉nm(Γ, ∆, ∃хΦ) маємо:
∃хΦ, Γ |=∗ ∆ ⇔ ( ),
x
z
R Φ Γ |=∗ ∆, εz (тут ∗ може бути Cl, Cm, T, F, TF ).
Теорема 5. При умові z∈VT та ( , , ( ))
u
v
z nm R x∉ Γ ∆ ∃ Φ маємо:
Γ |=∗ ∆, ( )
u
v
R x¬ ∃ Φ ⇔ Γ |=∗ ∆, ,
,
( ), .
u x
v z
R z¬ Φ ε
Тут ∗ може бути T, F, TF; для |=Cl та |=Cm в силу ¬|– і ¬–| достатньо теореми 4.
Випадок |=T . Для доведення ⇒ треба показати:
T(ΓA) ⊆ ( ( ) )
u
v A
F R x∃ Φ ∪ T(∆A) ⇒ T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A) ∪ T(εzA).
У доведенні ⇒ для |=F теореми 5 замість F(∆A) беремо T(ΓA), замість F(ΓA) бере-
мо T(∆A); маємо T(ΓA) ⊆ ( ( ) )
u
v A
F R x∃ Φ ∪ T(∆A) ⇒ F(εzA) ∩ T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A).
Використавши теоретико-множинне співвідношення A ∩ F ⊆ B ⇒ A ⊆ ,B F∪ звідси,
враховуючи F(εzA) ∪ T(εzA) =
V
A, отримуємо T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A) ∪ T(εzA).
Шкільняк С.С.
«Искусственный интеллект» 2013 № 1 74
2Ш
Для доведення ⇐ треба показати:
T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A) ∪ T(εzA) ⇒ T(ΓA) ⊆ ( ( ) )
u
v A
F R x∃ Φ ∪ T(∆A).
Використавши теоретико-множинне співвідношення A ⊆B F∪ ⇒ A ∩ F ⊆ B, маємо
T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A) ∪ T(εzA) ⇒ F(εzA) ∩ T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A). У дове-
денні ⇐ для |=F теореми 5 замість F(∆A) беремо T(ΓA), замість F(ΓA) беремо T(∆A);
маємо T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A) ⇒ T(ΓA) ⊆
,
,
( ( ) )
u x
v z A
F R Φ ∪ T(∆A). Звідси отримуємо
шукане співвідношення.
Випадок |=F . Для доведення ⇒ треба показати:
F(∆A) ( ( ) )
u
v A
T R x∩ ∃ Φ ⊆ F(ΓA) ⇒ F(∆A) ∩ F(εzA) ,
,
( ( ) )
u x
v z A
T R∩ Φ ⊆ F(ΓA).
За теоремою 1 маємо T ,
,
( ( ) )
u x
v z A
T R Φ ∩F(εzA) ⊆ ( ( ) ),
u
v A
T R x∃ Φ звідси із умови
F(∆A) ( ( ) )
u
v A
T R x∩ ∃ Φ ⊆ F(ΓA) випливає F(∆A) ∩ F(εzA) ,
,
( ( ) )
u x
v z A
T R∩ Φ ⊆ F(ΓA).
Для доведення ⇐ треба показати:
F(∆A) ∩ F(εzA) ,
,
( ( ) )
u x
v z A
T R∩ Φ ⊆ F(ΓA) ⇒ F(∆A) ( ( ) )
u
v A
T R x∩ ∃ Φ ⊆ F(ΓA).
Із F(∆A) ∩ F(εzA) ,
,
( ( ) )
u x
v z A
T R∩ Φ ⊆ F(ΓA), згідно з теоретико-множинним співвід-
ношенням A ∩ F ⊆ B ⇒ A ⊆ ,B F∪ маємо F(∆A) ,
,
( ( ) )
u x
v z A
T R∩ Φ ⊆ F(ΓA) ∪ T(εzA). У
доведенні ⇐ для |=T теореми 5 замість T(ΓA) беремо F(∆A), замість T(∆A) беремо
F(ΓA); маємо F(∆A) ,
,
( ( ) )
u x
v z A
T R∩ Φ ⊆ F(ΓA) ∪ T(εzA) ⇒ F(∆A) ( ( ) )
u
v A
T R x∩ ∃ Φ ⊆ F(ΓA).
Звідси отримуємо шукане співвідношення.
Випадок |=TF . Доводячи ⇒ для |=T та |=F так, як описано вище, отримуємо ⇒
для |=TF . Доводячи ⇐ для |=T та |=F так, як описано вище, отримуємо ⇐ для |=TF .
Наслідок 3. При умові z∈VT та z∉nm(Γ, ∆, ∃хΦ) маємо:
Γ |=∗ ∆, ¬∃хΦ ⇔ Γ |=∗ ∆, ( ),
x
z
R z¬ Φ ε (∗ може бути T, F, TF ).
Теорема 6. При умові z∈VT та ( , , ( ))
u
v
z nm R x∉ Γ ∆ ∃ Φ маємо:
Γ |=∗ ∆, ( )
u
v
R x∃ Φ ⇔ Γ |=∗ ∆, ( ),
u
v
R x∃ Φ
,
,
( ),
u x
v z
R Φ εz (∗ може бути Cl, Cm, T, F, TF ).
Твердження ⇒ вірне згідно з властивістю U. Тому залишається довести ⇐.
Наведемо для прикладу доведення для |=T та |=F .
Випадок |=T . Треба показати:
T(ΓA) ⊆ T(∆A) ,
,
( ( ) ) ( ( ) )
u u x
v A v z A
T R x T R∪ ∃ Φ ∪ Φ ∪T(εzA) ⇒ T(ΓA) ⊆ T(∆A) ( ( ) )
u
v A
T R x∪ ∃ Φ .
Нехай (1) – це умова T(ΓA) ⊆ T(∆A) ,
,
( ( ) ) ( ( ) )
u u x
v A v z A
T R x T R∪ ∃ Φ ∪ Φ ∪T(εzA). При-
пустимо супротивне: вірна умова (1) та існує d∈V
A таке: d∈T(ΓA), d∉T(∆A),
( ( ) ).
u
v A
d T R x∉ ∃ Φ Але ( , , ( ))
u
v
z nm R x∉ Γ ∆ ∃ Φ та z∈VT, тому для всіх a∈A маємо
d∇zaa∈T(ΓA), d∇zaa∉T(∆A), d∇zaa ( ( ) ).
u
v A
T R x∉ ∃ Φ Із останнього тоді отримуємо
( )d u d v x a z a∇ ∇ ∇a a a ∉T(ΦA), тому d∇zaa ,
,
( ( ) ).
u x
v z A
T R∉ Φ Але d∇zaa∉T(εzA),
звідки отримуємо d∇zaa∉T(∆A) ,
,
( ( ) ) ( ( ) )
u u x
v A v z A
T R x T R∪ ∃ Φ ∪ Φ ∪T(εzA). При цьому
d∇zaa∈T(ΓA), тому маємо суперечність із (1).
Випадок |=F . Треба показати:
F(∆A) ,
,
( ( ) ) ( ( ) )
u u x
v A v z A
F R x F R∩ ∃ Φ ∩ Φ ∩F(εzA) ⊆ F(ΓA) ⇒ F(∆A) ( ( ) )
u
v A
F R x∩ ∃ Φ ⊆ F(ΓA).
Властивості відношень логічного наслідку в логіках квазіарних предикатів
«Штучний інтелект» 2013 № 1 75
2Ш
Нехай (1) – це умова F(∆A) ,
,
( ( ) ) ( ( ) )
u u x
v A v z A
F R x F R∩ ∃ Φ ∩ Φ ∩F(εzA) ⊆ F(ΓA). При-
пустимо супротивне: вірна умова (1) та існує d∈V
A таке: d∈F(∆A), ( ( ) ),
u
v A
d F R x∈ ∃ Φ
d∉F(ΓA). Але ( , , ( ))
u
v
z nm R x∉ Γ ∆ ∃ Φ та z∈VT, тому для всіх a∈A маємо d∇zaa∈F(∆A),
d∇zaa∉F(ΓA), d∇zaa ( ( ) )
u
v A
F R x∈ ∃ Φ . Із умови d∇zaa ( ( ) )
u
v A
F R x∈ ∃ Φ отримуємо
( )d u d v x a z a∇ ∇ ∇a a a ∈F(ΦA), тому d∇zaa ,
,
( ( ) )
u x
v z A
F R∈ Φ . Але d∇zaa∈F(εzA),
звідки отримуємо d∇zaa∈F(∆A) ,
,
( ( ) ) ( ( ) )
u u x
v A v z A
F R x F R∩ ∃ Φ ∩ Φ ∩ F(εzA). При цьому
d∇zaa∉F(ΓA), тому маємо суперечність із (1).
Наслідок 4. При умові z∈VT та z∉nm(Γ, ∆, ∃хΦ) маємо:
Γ |=∗ ∆, ∃хΦ ⇔ Γ |=∗ ∆, ∃хΦ, ( ),
x
z
R zΦ ε (∗ може бути Cl, Cm, T, F, TF ).
Подібним чином доводяться теореми 7 – 9 та їх наслідки.
Теорема 7. При умові z∈VT та ( , , ( ))
u
v
z nm R x∉ Γ ∆ ∃ Φ маємо:
( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆ ⇔ ,
,
( ), ( ),
u u x
v v z
R x R¬ ∃ Φ ¬ Φ Γ |=∗ ∆, εz (∗ може бути T, F, TF ).
Наслідок 5. При умові z∈VT та z∉nm(Γ, ∆, ∃хΦ) маємо:
¬∃хΦ, Γ |=∗ ∆ ⇔ ¬∃хΦ, ( ),
x
z
R¬ Φ Γ |=∗ ∆, εz (∗ може бути T, F, TF ).
Теорема 8. Γ |=∗ ∆, ( ),
u
v
R x∃ Φ εy ⇔ Γ |=∗ ∆, ,
,
( ), ( ),
u u x
v v y
R x R y∃ Φ Φ ε
(∗може бути Cl, Cm, T, F, TF ).
Наслідок 6. Γ |=∗ ∆, ∃хΦ, εy ⇔ Γ |=∗ ∆, ∃хΦ, ( ),
x
y
R yΦ ε
(∗ може бути Cl, Cm, T, F, TF ).
Теорема 9. ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆, εy ⇔ ( ),
u
v
R x¬ ∃ Φ
,
,
( ),
u x
v y
R¬ Φ Γ |=∗ ∆, εy
(∗ може бути T, F, TF ).
Наслідок 7. ¬∃хΦ, Γ |=∗ ∆, εy ⇔ ¬∃хΦ, ( ),
x
y
R¬ Φ Γ |=∗ ∆, εy (∗ може бути T, F, TF ).
Теорема 10. Γ |=∗ ∆, ( )
u
v
R x∃ Φ ⇔ εy, Γ |=∗ ∆, ( )
u
v
R x∃ Φ та
Γ |=∗ ∆, ( ),
u
v
R x∃ Φ
,
,
( ),
u x
v yR Φ εy (∗ може бути Cl, Cm, T, F, TF ).
Твердження ⇒ вірне згідно з властивістю U. Тому залишається довести ⇐.
Випадок |=Cl . Припустимо супротивне: Γ |=Cl ∆, ,
,
( ), ( ),
u u x
v v y
R x R y∃ Φ Φ ε та
εy, Γ |=Cl ∆, ( )
u
v
R x∃ Φ проте Γ |≠Cl ∆, ( ).
u
v
R x∃ Φ Тоді T(ΓA) ∩ F (∆A) ( ( ) )
u
v A
F R x∩ ∃ Φ ≠ ∅,
звідки існує d∈V
A таке, що d∈T(ΓA) ∩ F(∆A) ( ( ) ).
u
v A
F R x∩ ∃ Φ
Можливі 2 випадки: d(y)↑ та d(y)↓. Якщо d(y)↑, то d∈T(εyA), звідки d∈T(εy) ∩
∩ T(ΓA) ∩ F(∆A) ( ( ) ),
u
v A
F R x∩ ∃ Φ що суперечить умові εy, Γ |=Cl ∆, ( )
u
v
R x∃ Φ . Якщо
d(y)↓, то d∈F(εyA); нехай d(y) = a. Із ( ( ) )
u
v A
d F R x∈ ∃ Φ тоді ( ) ( ).Ad u d v F x∇ ∈ ∃ Φa
Звідси ( ) ( )
A
d u d v x b F∇ ∇ ∈ Φa a для всіх b∈A, це вірно і для d(y) = a, тому
( ) ( ) ( ),
A
d u d v x d y F∇ ∇ ∈ Φa a звідки ,
,
( ( ) )
u x
v y Ad F R∈ Φ . Отже, d∈T(ΓA) ∩ F(∆A) ∩
,
,
( ( ) ) ( ( ) )
u u x
v A v y AF R x F R∩ ∃ Φ ∩ Φ ∩F(εyA), що суперечить Γ |=Cl ∆, ,
,
( ), ( ), .
u u x
v v yR x R y∃ Φ Φ ε
Випадок |=Cm . Доведення проводиться подібно доведенню для |=Cl.
Випадок |=T . Покажемо: T(ΓA) ⊆ T(∆A) ,
,
( ( ) ) ( ( ) ) ( )
u u x
v A v y A AT R x T R T y∪ ∃ Φ ∪ Φ ∪ ε та
T(εyA) ∩T(ΓA) ⊆ T(∆A) ( ( ) )
u
v A
T R x∪ ∃ Φ ⇒ T(ΓA) ⊆ T(∆A) ( ( ) ).
u
v A
T R x∪ ∃ Φ
Шкільняк С.С.
«Искусственный интеллект» 2013 № 1 76
2Ш
Позначимо (1) та (2) умови T(ΓA) ⊆ T(∆A) ,
,
( ( ) ) ( ( ) )
u u x
v A v y AT R x T R∪ ∃ Φ ∪ Φ ∪T(εyA)
та T(εyA) ∩T(ΓA) ⊆ T(∆A) ( ( ) )
u
v A
T R x∪ ∃ Φ . Припустимо супротивне: вірні (1) та (2),
водночас існує d∈V
A таке: d∈T(ΓA), d∉T(∆A), ( ( ) ).
u
v A
d T R x∉ ∃ Φ Можливі 2 випадки:
d∈T(εyA) та d∉T(εyA).
Якщо d∈T(εyA), то маємо d∈T(εyA) ∩T(ΓA); проте d∉T(∆A) та ( ( ) ),
u
v A
d T R x∉ ∃ Φ
тому отримуємо суперечність з (2).
Якщо d∉T(εyA), то, враховуючи d∈T(ΓA), d∉T(∆A) та ( ( ) ),
u
v A
d T R x∉ ∃ Φ із (1)
негайно випливає ,
,
( ( ) ),
u x
v y Ad T R∈ Φ що дає ( ) ( ) ( ).
A
d u d v x d y T∇ ∇ ∈ Φa a Із
d∉T(εyA) маємо d∈F(εyA), тому d(y)↓a для деякого a∈A, звідки отримуємо
( ) ( ).Ad u d v x a T∇ ∇ ∈ Φa a Це дає ( ( ) )
u
v A
d T R x∈ ∃ Φ – суперечність припущенню.
Випадок |=F . Покажемо: F(∆A) ,
,
( ( ) ) ( ( ) )
u x u
v y A v AF R F R x∩ Φ ∩ ∃ Φ ∩F(εyA) ⊆ F(ΓA) та
F(∆A) ( ( ) )
u
v A
F R x∩ ∃ Φ ⊆ F(ΓA) ∪ F(εyA) ⇒ F(∆A) ( ( ) )
u
v A
F R x∩ ∃ Φ ⊆ F(ΓA).
За теоремою 1 маємо ( ( ) )
u
v A
F R x∃ Φ ∩F(εyA) ⊆
,
,
( ( ) ),
u x
v y AF R Φ тому перша умова
набуває вигляду F(∆A) ∩ F ( ( ) )
u
v A
R x∃ Φ ∩ F(εyA) ⊆ F(ΓA), позначимо її (1). Позначимо (2)
умову F(∆A) ( ( ) )
u
v A
F R x∩ ∃ Φ ⊆ F(ΓA) ∪ F(εyA). Припустимо супротивне: вірні (1) та (2),
водночас існує d∈V
A таке: d∈F(∆A), ( ( ) ),
u
v A
d R x∈ ∃ Φ d∉F(ΓA). Можливі 2 випадки:
d∈F(εyA) та d∉F(εyA).
Якщо d∉F(εyA), то згідно з d∉F(ΓA) маємо d∉F(ΓA) ∪ F(εy). Проте d∈F(∆A) та
( ( ) ),
u
v A
d F R x∈ ∃ Φ тому отримуємо суперечність з (2).
Якщо d∈F(εyA), то маємо d∈F(∆A) ( ( ) )
u
v A
F R x∩ ∃ Φ ∩F(εyA); водночас d∉F(ΓA),
тому отримуємо суперечність з (1).
Наслідок 8. Γ |=∗ ∆, ∃хΦ ⇔ εy, Γ |=∗ ∆, ∃хΦ та Γ |= ∆, ∃хΦ, ( ),
x
y
R Φ εy.
(тут ∗ може бути Cl, Cm, T, F, TF ).
Подібним чином доводяться теорема 11 та її наслідок.
Теорема 11. ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆ ⇔
⇔ εy, ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆ та ,
,
( ), ( ),
u u x
v v y
R x R¬ ∃ Φ ¬ Φ Γ |=∗ ∆, εy (∗ може бути T, F, TF ).
Наслідок 9. ¬∃хΦ, Γ |=∗ ∆ ⇔ εy, ¬∃хΦ, Γ |=∗ ∆ та ¬∃хΦ, ( ),
x
y
R¬ Φ Γ |=∗ ∆, εy.
(∗ може бути T, F, TF ).
На основі теорем 4 – 11 та наслідків 2 – 9 маємо властивості елімінації кванторів:
∃R|–) ( ),
u
v
R x∃ Φ Γ |=∗ ∆ ⇔ ,
,
( ),
u x
v z
R Φ Γ |=∗ ∆, εz;
∃|–) ∃хΦ, Γ |=∗ ∆ ⇔ ( ),
x
z
R Φ Γ |=∗ ∆, εz;
¬∃R–|) Γ |=∗ ∆, ( )
u
v
R x¬ ∃ Φ ⇔ Γ |=∗ ∆, ,
,
( ), ;
u x
v z
R z¬ Φ ε
¬∃–|) Γ |=∗ ∆, ¬∃хΦ ⇔ Γ |=∗ ∆, ( ), ;
x
z
R z¬ Φ ε
∃Rf–|) Γ |=∗ ∆, ( )
u
v
R x∃ Φ ⇔ Γ |=∗ ∆, ( ),
u
v
R x∃ Φ
,
,
( ), ( ), ;
u u x
v v z
R x R z∃ Φ Φ ε
∃f–|) Γ |=∗ ∆, ∃хΦ ⇔ Γ |=∗ ∆, ∃хΦ, ( ), ;
x
z
R zΦ ε
Властивості відношень логічного наслідку в логіках квазіарних предикатів
«Штучний інтелект» 2013 № 1 77
2Ш
¬∃Rf|–) ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆ ⇔ ,
,
( ), ( ),
u u x
v v z
R x R¬ ∃ Φ ¬ Φ Γ |=∗ ∆, εz;
¬∃f|–) ¬∃хΦ, Γ |=∗ ∆ ⇔ ¬∃хΦ, ( ),
x
z
R¬ Φ Γ |=∗ ∆, εz.
Для властивостей ∃R|–, ¬∃R–|, ∃Rf–|, ¬∃Rf|– умови: z∈VT та z∉nm ( , , ( ));
u
v
R xΓ ∆ ∃ Φ
для властивостей ∃|–, ¬∃–|, ∃f–|, ¬∃f|– умови: z∈VT та z∉nm(Γ, ∆, ∃хΦ)).
∃Rv–|) Γ |=∗ ∆, ( ),
u
v
R x y∃ Φ ε ⇔ Γ |=∗ ∆, ,
,
( ), ( ), ;
u u x
v v y
R x R y∃ Φ Φ ε
∃v–|) Γ |=∗ ∆, ∃хΦ, εy ⇔ Γ |=∗ ∆, ∃хΦ, ( ), ;
x
y
R yΦ ε
¬∃Rv|–) ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆, εy ⇔ ,
,
( ), ( ),
u u x
v v y
R x R¬ ∃ Φ ¬ Φ Γ |=∗ ∆, εy;
¬∃v|–) ¬∃хΦ, Γ |=∗ ∆, εy ⇔ ¬∃хΦ, ( ),
x
y
R¬ Φ Γ |=∗ ∆, εy;
∃Rd–|) Γ |=∗ ∆, ( )
u
v
R x∃ Φ ⇔ εy, Γ |=∗ ∆, ( )
u
v
R x∃ Φ та Γ |=∗ ∆, ,
,
( ), ( ), ;
u u x
v v y
R x R y∃ Φ Φ ε
∃d–|) Γ |=∗ ∆, ∃хΦ ⇔ εy, Γ |=∗ ∆, ∃хΦ та Γ |=∗ ∆, ∃хΦ, ( ), ;
x
y
R yΦ ε
¬∃Rd|–) ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆ ⇔
⇔ εy, ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆ та ,
,
( ), ( ),
u u x
v v y
R x R¬ ∃ Φ ¬ Φ Γ |=∗ ∆, εy;
¬∃d|–) ¬∃хΦ, Γ |=∗ ∆ ⇔ εy, ¬∃хΦ, Γ |=∗ ∆ та ¬∃хΦ, ( ),
x
y
R¬ Φ Γ |=∗ ∆, εy.
Висновки
У роботі досліджено властивості відношень логічного наслідку для множин
формул у чистих першопорядкових композиційно-номінативних логіках часткових
однозначних, тотальних неоднозначних та часткових неоднозначних квазіарних пре-
дикатів. Основна увага приділена вивченню властивостей цих відношень, пов’язаних
з елімінацією кванторів. Для опису таких властивостей використано спеціальні пре-
дикати, які визначають наявність значення для змінних. Використання цих предика-
тів-індикаторів є характерною особливістю проведеного дослідження.
Властивості відношень логічного наслідку для множин формул є семантичною
основою побудови для зазначених логік відповідних числень секвенційного типу.
Література
1. Eds. Abramsky S. Handbook of Logic in Computer Science: in 5 vol. / [Eds. Abramsky S., Gabbay D.
and Maibaum T.S.E.]. – Oxford : Clarendon Press, 1994 – 2000.
2. Нікітченко М.С. Математична логіка та теорія алгоритмів / М.С. Нікітченко, С.С. Шкільняк. – К. :
ВПЦ Київський університет, 2008. – 528 с.
3. Шкільняк С.С. Відношення логічного наслідку в композиційно-номінативних логіках /
С.С. Шкільняк // Пробл. програмування. – 2010. – № 1 – C. 15-38.
4. Шкильняк С.С. Логики квазиарных предикатов первого порядка / С.С. Шкильняк // Кибернетика и
системный анализ. – 2010. – № 6 – С. 32-49.
5. Нікітченко М.С. Першопорядкові композиційно-номінативні логіки / М.С. Нікітченко, С.С. Шкіль-
няк // Вісник Київського ун-ту. Серія : фіз.-мат. науки. – 2011. – Вип. 4. – С. 176-185.
6. Шкильняк С.С. Логічний наслідок та його формалізації в композиційно-номінативних логіках /
С.С. Шкільняк // Штучний інтелект. – 2012. – № 1. – C. 307-319.
7. Nikitchenko M. Satisfability and Validity Problems in Many-sorted Composition-Nominative Pure Predicate Logics
/ M. Nikitchenko, V. Tymofieiev // Comm. in Comp. and Inf. Science. – Springer, 2012. – V. 347. – P. 89-110.
Literature
1. Handbook of Logic in Computer Science: In 5 vol. / [Eds. Abramsky S., Gabbay D. and Maibaum T.S.E.]. –
Oxford: Clarendon Press, 1994–2000.
Шкільняк С.С.
«Искусственный интеллект» 2013 № 1 78
2Ш
2. Nikitchenko M.S. Matematychna lohika ta teoria algorytmiv. К.: VPC Kyivskyi universytet, 2008. –
528 p.
3. Shkilniak S.S. Vidnoshennia lohichnogo naslidku v komposytsijno-nominatyvnyh lohikah. Probl.
programuvannia. 2010. № 1. S. 15–38.
4. Shkilniak S.S. Kibernetika i systemnyi analiz. 2010. № 6. S. 32-49.
5. Nikitchenko M.S. Visnyk Kyiv. un-tu. Ser.: phiz.-mat. nauky. 2011. Vyp. 4. S. 176-185.
6. Shkilniak S.S. Shtucznyj іntelekt. 2012. № 1. S. 307-319.
7. Nikitchenko M. Satisfability and Validity Problems in Many-sorted Composition-Nominative Pure Predicate
Logics / M. Nikitchenko, V. Tymofieiev // Comm. in Comp. and Inf. Science. Vol. 0137. Springer, 2012.
RESUME
S.S. Shkilniak
Properties of Logical Consequence Relations in Logics of Quasi-Ary Predicates
The apparatus of mathematical logic is effective in solving the wide range of problems in
computer science and programming. Various logical systems are usually based on classical
predicate logic. However, fundamental restrictions of classical logic make necessary introducing
of new program-oriented formalisms. Composition-nominative approach is common for logic
and programming, therefore it is a natural basis for construction of such a formalism –
composition-nominative logics (CNL).
Logical consequence is the central concept of logic. We define the following
relations of logical consequence: «true-valued» |=T, «false-valued» |=F, «strong» |=TF,
«irrefutable» |=Cl, and «saturated» |=Cm.
In this paper logical consequence relations for sets of formulas for pure first-order
CNL of partial single-valued, total and partial multiple-valued predicates are studied. We
focus on the properties of the relations concerned with quantifier elimination. The
characteristic feature of this work is using of the special variable definedness predicates εz
for description of such properties.
We obtained the properties of quantifier elimination under renomination ∃R|–, ¬∃R–|,
∃Rf–|, ¬∃Rf|–, ∃Rv–|, ¬∃Rv|–, ∃Rd–|, ¬∃Rd|– and of exterior quantifiers ∃|–, ¬∃–|, ∃f–|, ¬∃f|–,
∃v–|, ¬∃v|–, ∃d–|, ¬∃d|–. As an example here are some of them (asterisk ∗ substitutes any of
Cl, Cm, T, F, TF).
∃R|–) ( ),
u
v
R x∃ Φ Γ |=∗ ∆ ⇔ ,
,
( ),
u x
v z
R Φ Γ |=∗ ∆, εz (z∈VT and ( , , ( )));
u
v
z nm R x∉ Γ ∆ ∃ Φ
∃Rv–|) Γ |=∗ ∆, ( ),
u
v
R x y∃ Φ ε ⇔ Γ |=∗ ∆, ,
,
( ), ( ), , .
u u x
v v y
R x R y∃ Φ Φ Γ ε
¬∃Rv|–) ( ),
u
v
R x¬ ∃ Φ Γ |=∗ ∆, εy ⇔ ,
,
( ), ( ),
u u x
v v y
R x R¬ ∃ Φ ¬ Φ Γ |=∗ ∆, εy;
∃Rd–|) Γ |=∗ ∆, ( )
u
v
R x∃ Φ ⇔ εy, Γ |=∗ ∆, ( )
u
v
R x∃ Φ and Γ |=∗ ∆, ,
,
( ), ( ), .
u u x
v v y
R x R y∃ Φ Φ ε
¬∃–|) Γ |=∗ ∆, ¬∃хΦ ⇔ Γ |=∗ ∆, ( ),
x
z
R z¬ Φ ε (z∈VT and z∉nm(Γ, ∆, ∃хΦ));
¬∃d|–) ¬∃хΦ, Γ |=∗ ∆ ⇔ εy, ¬∃хΦ, Γ |=∗ ∆ and ¬∃хΦ, ( ),
x
y
R¬ Φ Γ |=∗ ∆, εy.
The properties of logical consequence relations for sets of formulas are a semantic
basis for construction of corresponding sequent calculi for first-order CNL.
Стаття надійшла до редакції 13.11.2012.
|