Логики квазиарных предикатов первого порядка
Досліджуються композиційно-номінативні логіки квазіарних предикатів. Розглянуто спектр композиційно-номінативних логік, описано класи першопорядкових логік квазіарних предикатів. Для загального випадку логік квазіарних предикатів кванторного рівня побудовано числення секвенційного типу, доведені йог...
Saved in:
| Date: | 2010 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Series: | Кибернетика и системный анализ |
| Subjects: | |
| Online Access: | http://dspace.nbuv.gov.ua/handle/123456789/45645 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Логики квазиарных предикатов первого порядка / С.С. Шкильняк // Кибернетика и системный анализ. — 2010. — № 6. — С. 32–50. — Бібліогр.: 15 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-45645 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-456452013-06-18T03:06:40Z Логики квазиарных предикатов первого порядка Шкильняк, С.С. Кибернетика Досліджуються композиційно-номінативні логіки квазіарних предикатів. Розглянуто спектр композиційно-номінативних логік, описано класи першопорядкових логік квазіарних предикатів. Для загального випадку логік квазіарних предикатів кванторного рівня побудовано числення секвенційного типу, доведені його коректність і повнота. Composition nominative logics of quasi-ary predicates are studied in the paper. The spectrum of composition nominative logics is considered and various classes of first-order logics of quasi-ary predicates are specified. Sequent calculi are constructed for the general case of logics of quasi-ary predicates of quantifier level, and soundness and completeness theorems are proved. 2010 Article Логики квазиарных предикатов первого порядка / С.С. Шкильняк // Кибернетика и системный анализ. — 2010. — № 6. — С. 32–50. — Бібліогр.: 15 назв. — рос. 0023-1274 http://dspace.nbuv.gov.ua/handle/123456789/45645 004.4 ru Кибернетика и системный анализ Інститут кібернетики ім. В.М. Глушкова НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Кибернетика Кибернетика |
| spellingShingle |
Кибернетика Кибернетика Шкильняк, С.С. Логики квазиарных предикатов первого порядка Кибернетика и системный анализ |
| description |
Досліджуються композиційно-номінативні логіки квазіарних предикатів. Розглянуто спектр композиційно-номінативних логік, описано класи першопорядкових логік квазіарних предикатів. Для загального випадку логік квазіарних предикатів кванторного рівня побудовано числення секвенційного типу, доведені його коректність і повнота. |
| format |
Article |
| author |
Шкильняк, С.С. |
| author_facet |
Шкильняк, С.С. |
| author_sort |
Шкильняк, С.С. |
| title |
Логики квазиарных предикатов первого порядка |
| title_short |
Логики квазиарных предикатов первого порядка |
| title_full |
Логики квазиарных предикатов первого порядка |
| title_fullStr |
Логики квазиарных предикатов первого порядка |
| title_full_unstemmed |
Логики квазиарных предикатов первого порядка |
| title_sort |
логики квазиарных предикатов первого порядка |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| publishDate |
2010 |
| topic_facet |
Кибернетика |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/45645 |
| citation_txt |
Логики квазиарных предикатов первого порядка / С.С. Шкильняк // Кибернетика и системный анализ. — 2010. — № 6. — С. 32–50. — Бібліогр.: 15 назв. — рос. |
| series |
Кибернетика и системный анализ |
| work_keys_str_mv |
AT škilʹnâkss logikikvaziarnyhpredikatovpervogoporâdka |
| first_indexed |
2025-07-04T04:32:13Z |
| last_indexed |
2025-07-04T04:32:13Z |
| _version_ |
1836689428054016000 |
| fulltext |
ÓÄÊ 004.4
Ñ.Ñ. ØÊÈËÜÍßÊ
ËÎÃÈÊÈ ÊÂÀÇÈÀÐÍÛÕ ÏÐÅÄÈÊÀÒΠÏÅÐÂÎÃÎ ÏÎÐßÄÊÀ
Êëþ÷åâûå ñëîâà: ëîãèêà, ïðîãðàììèðîâàíèå, êîìïîçèöèîííîå ïðîãðàììèðîâàíèå,
êîìïîçèöèîííî-íîìèíàòèâíûé ïîäõîä, ñåìàíòèêà, ñèíòàêñèñ, íîìèíàòèâíîå äàí-
íîå, èìåííîå ìíîæåñòâî, ïðåäèêàò, êîìïîçèöèÿ, îòíîøåíèå ëîãè÷åñêîãî ñëåä-
ñòâèÿ, èñ÷èñëåíèå, ñåêâåíöèÿ, ñåêâåíöèàëüíîå èñ÷èñëåíèå, êîððåêòíîñòü, ïîëíîòà.
ÂÂÅÄÅÍÈÅ
Ïðîáëåìû ïîñòðîåíèÿ ëîãè÷åñêèõ ôîðìàëèçìîâ, îðèåíòèðîâàííûõ íà èññëåäîâà-
íèå ñâîéñòâ ïðîãðàìì, âñåãäà áûëè â öåíòðå âíèìàíèÿ Êèåâñêîé øêîëû êèáåð-
íåòèêè, îñíîâàííîé Â.Ì. Ãëóøêîâûì. Ïðåäëîæåííûå èì àëãåáðàè÷åñêèé ïîäõîä
è àëãîðèòì î÷åâèäíîñòè íàøëè øèðîêîå ïðèìåíåíèå è äàëüíåéøåå ðàçâèòèå
â ðàáîòàõ À.À. Ëåòè÷åâñêîãî è åãî ñîàâòîðîâ, íàïðèìåð, [1–3]. Àëãåáðàè÷åñêèé
ïîäõîä ê ïîñòðîåíèþ ëîãè÷åñêèõ ñèñòåì àêòóàëåí è â íàñòîÿùåå âðåìÿ.  äàí-
íîé ñòàòüå íà îñíîâàíèè ýòîãî ïîäõîäà èññëåäóþòñÿ êîìïîçèöèîííî-íîìèíàòèâ-
íûå ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ. Ïîñòðîåííîå äëÿ òàêèõ ëîãèê èñ÷èñëåíèå
ñåêâåíöèàëüíîãî òèïà ðàçâèâàåò ðÿä èäåé àëãîðèòìà î÷åâèäíîñòè.
Ðàçðàáîòàíî ìíîãî ðàçíîîáðàçíûõ ëîãè÷åñêèõ ñèñòåì, êîòîðûå óñïåøíî èñ-
ïîëüçóþòñÿ â ïðîãðàììèðîâàíèè [4]. Òàêèå ñèñòåìû îáû÷íî áàçèðóþòñÿ íà êëàññè-
÷åñêîé ëîãèêå ïðåäèêàòîâ [5]. Íî êëàññè÷åñêàÿ ëîãèêà, íåñìîòðÿ íà âñå åå ïîëîæè-
òåëüíûå êà÷åñòâà, íå ïîçâîëÿåò àäåêâàòíî âûðàçèòü ïîòðåáíîñòè ïðîãðàììèðîâà-
íèÿ. Ðÿä îãðàíè÷åíèé [6] óñëîæíÿåò åå ïðèìåíåíèå. Íåîáõîäèìîñòü óñèëåíèÿ
êëàññè÷åñêîé ëîãèêè äëÿ ðåøåíèÿ íîâûõ çàäà÷ ïðîãðàììèðîâàíèÿ è ìîäåëèðîâà-
íèÿ ñòàëà ïðåäïîñûëêîé âîçíèêíîâåíèÿ êîìïîçèöèîííî-íîìèíàòèâíûõ ëîãèê. Òà-
êîå íàçâàíèå ïîëó÷èëè ëîãèêè, ñòðîÿùèåñÿ íà îñíîâàíèè êîìïîçèöèîííî-íîìèíà-
òèâíîãî ïîäõîäà [7]. Ïðèìåíåíèå ýòîãî ïîäõîäà ñïîñîáñòâîâàëî ïîëó÷åíèþ [8]
ðÿäà ëîãè÷åñêèõ ìîäåëåé ðàçíîîáðàçíûõ ïðåäìåòíûõ îáëàñòåé, íàõîäÿùèõñÿ íà
ðàçíûõ óðîâíÿõ àáñòðàêòíîñòè è îáùíîñòè.
Êîìïîçèöèîííî-íîìèíàòèâíûé ïîäõîä ê ïîñòðîåíèþ ìîäåëåé ïðîãðàìì è
îðèåíòèðîâàííûõ íà íèõ ëîãèê èñõîäèò èç êîìïîçèöèîííîãî ïðîãðàììèðîâà-
íèÿ [9, 10]. Îí áàçèðóåòñÿ íà ïðèíöèïàõ êîìïîçèöèîííîñòè è íîìèíàòèâíîñòè,
îïèðàåòñÿ íà îáùåìåòîäîëîãè÷åñêèé ïðèíöèï ðàçâèòèÿ êàê âîñõîæäåíèÿ îò
àáñòðàêòíîãî ê êîíêðåòíîìó. Ïðèíöèï êîìïîçèöèîííîñòè òðàêòóåò ñðåäñòâà ïî-
ñòðîåíèÿ ïðîãðàìì (ôóíêöèé, ïðåäèêàòîâ) êàê àëãåáðàè÷åñêèå îïåðàöèè. Äëÿ ëîãè-
êè ýòî îçíà÷àåò ñâåäåíèå ëîãè÷åñêèõ ñâÿçîê è êâàíòîðîâ ê êîìïîçèöèÿì ïðåäèêà-
òîâ. Ïðèíöèï íîìèíàòèâíîñòè áàçèðóåòñÿ íà íåîáõîäèìîñòè èñïîëüçîâàíèÿ îòíî-
øåíèé èìåíîâàíèÿ äëÿ ïîñòðîåíèÿ ñåìàíòè÷åñêèõ ìîäåëåé ëîãèê è ïðîãðàìì.
Ñîãëàñíî êîìïîçèöèîííî-íîìèíàòèâíîìó ïîäõîäó ëîãèêè ñòðîÿòñÿ ïî ñåìàí-
òèêî-ñèíòàêñè÷åñêîé ñõåìå. Ýòî îçíà÷àåò, ÷òî ñíà÷àëà çàäàþòñÿ èíòåíñèîíàëüíûå
(ñîäåðæàòåëüíûå) ìîäåëè ëîãèê. Òàêèå ìîäåëè, â ïåðâóþ î÷åðåäü, îïðåäåëÿþòñÿ
óðîâíÿìè ðàññìîòðåíèÿ äàííûõ, ïîýòîìó äëÿ èõ çàäàíèÿ ôèêñèðóåòñÿ óðîâåíü
àáñòðàêöèè ðàññìîòðåíèÿ. Èíòåíñèîíàëüíûå ìîäåëè èíäóöèðóþò êëàññ ôîðìóë
(ÿçûê ëîãèêè) ñîîòâåòñòâóþùåãî óðîâíÿ (ñèíòàêñè÷åñêèé àñïåêò).
Äàëåå ñòðîÿòñÿ ñîîòâåòñòâóþùèå ðàññìîòðåííîìó óðîâíþ àáñòðàêöèè ýêñòåí-
ñèîíàëüíûå ìîäåëè, êîòîðûå îïðåäåëÿþò ñåìàíòè÷åñêèå àñïåêòû ëîãèê. Ýêñòåíñè-
îíàëüíàÿ ñåìàíòè÷åñêàÿ ìîäåëü çàäàåòñÿ êàê ïðåäèêàòíàÿ êîìïîçèöèîííàÿ ñèñòåìà
32 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
© Ñ.Ñ. Øêèëüíÿê, 2010
( , , )D Pr C . Òàêàÿ ñèñòåìà ôàêòè÷åñêè îïðåäåëÿåò äâå àëãåáðû: àëãåáðó (àëãåáðàè-
÷åñêóþ ñèñòåìó) äàííûõ ( , )D Pr è àëãåáðó ïðåäèêàòîâ ( , )Pr C . Òåðìû àëãåáðû
ïðåäèêàòîâ ìîãóò òðàêòîâàòüñÿ êàê ôîðìóëû ÿçûêà ëîãèêè. Îñíîâíûì çäåñü ÿâëÿ-
åòñÿ ïîíÿòèå êîìïîçèöèè, ïîñêîëüêó èìåííî êîìïîçèöèè îïðåäåëÿþò óíèâåðñàëü-
íûå ìåòîäû ïîñòðîåíèÿ ïðåäèêàòîâ, âûñòóïàÿ ÿäðîì ëîãèêè îïðåäåëåííîãî òèïà.
Íàêîíåö, ñòðîÿòñÿ ôîðìàëüíî-àêñèîìàòè÷åñêèå ëîãè÷åñêèå èñ÷èñëåíèÿ, êîòî-
ðûå çàäàþò ñèíòàêñè÷åñêèå àñïåêòû ëîãèê. Îñíîâíûìè òèïàìè òàêèõ èñ÷èñëåíèé
ÿâëÿþòñÿ ôîðìàëüíûå ñèñòåìû ãèëüáåðòîâñêîãî òèïà è ñèñòåìû ãåíöåíîâñêîãî
òèïà (ñåêâåíöèàëüíûå èñ÷èñëåíèÿ, ñèñòåìû íàòóðàëüíîãî âûâîäà).
 ðàçä. 1 ðàññìîòðåí ñïåêòð êîìïîçèöèîííî-íîìèíàòèâíûõ ëîãèê, â ðàçä. 2
îïèñàíû îñíîâíûå êëàññû ïåðâîïîðÿäêîâûõ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ.
 ðàçä. 3 èçó÷åíî ñïåöèàëüíîå îòíîøåíèå ëîãè÷åñêîãî ñëåäñòâèÿ â òàêèõ ëîãèêàõ,
â ðàçä. 4 ïîñòðîåíî èñ÷èñëåíèå ñåêâåíöèàëüíîãî òèïà äëÿ îáùåãî ñëó÷àÿ ëîãèê
êâàçèàðíûõ ïðåäèêàòîâ êâàíòîðíîãî óðîâíÿ.
Ïîíÿòèÿ, êîòîðûå çäåñü íå óòî÷íÿþòñÿ, áóäåì ïîíèìàòü â ñìûñëå ðàáîòû [8].
1. ÑÏÅÊÒÐ ÊÎÌÏÎÇÈÖÈÎÍÍÎ-ÍÎÌÈÍÀÒÈÂÍÛÕ ËÎÃÈÊ
Èíòåíñèîíàëüíûå ìîäåëè êîìïîçèöèîííî-íîìèíàòèâíûõ ëîãèê (ÊÍË) çàäàþòñÿ
óðîâíÿìè ðàññìîòðåíèÿ äàííûõ. Ðàçâèòèå ïîíÿòèÿ äàííîãî [8] ïðèâîäèò ê òðåì
áàçîâûì óðîâíÿì: D.W (äàííûå êàê öåëûå), D.P (äàííûå êàê ñòðóêòóðèðîâàí-
íûå), D.H (äàííûå êàê èåðàðõè÷åñêèå). Êàæäûé èç íèõ ðàñïàäàåòñÿ íà òðè ïîä-
óðîâíÿ: A (àáñòðàêòíûé), C (êîíêðåòíûé), S (ñèíòåòè÷åñêèé). Îòñþäà èìååì äå-
âÿòü óðîâíåé ðàññìîòðåíèÿ äàííûõ:
D.W.A; D.W.C; D.W.S;
D.P.A; D.P.C; D.P.S;
D.H.A; D.H.C; D.H.S.
Òàêèì îáðàçîì, ïîëó÷àåì ñëåäóþùèå åñòåñòâåííûå óðîâíè ÊÍË:
— ïðîïîçèöèîíàëüíûå (óðîâåíü D.W.A, äàííûå àáñòðàêòíûå);
— ñèíãóëÿðíûå (óðîâåíü D.W.C, äàííûå êàê öåëîñòíûå êîíêðåòíûå);
— ðåíîìèíàòèâíûå è ïåðâîïîðÿäêîâûå (óðîâåíü D.P.S, äàííûå êàê íîìèíàòû);
— ëîãèêè íîìèíàòèâíûõ äàííûõ (óðîâåíü D.H.S, äàííûå êàê èåðàðõè÷åñêèå
íîìèíàòû).
Ëîãèêè äðóãèõ, â îïðåäåëåííîì ñìûñëå âûðîæäåííûõ óðîâíåé, äîâîëüíî ñïå-
öèôè÷åñêèå è òðåáóþò îòäåëüíîãî èññëåäîâàíèÿ.
Íà ïðîïîçèöèîíàëüíîì óðîâíå äàííûå òðàêòóþòñÿ ïðåäåëüíî àáñòðàêòíî, êàê
«÷åðíûå ÿùèêè», ò.å. íè îäíî ñâîéñòâî äàííûõ íå ÿâëÿåòñÿ äîñòóïíûì. Íà ýòîì
óðîâíå ïðåäèêàòû èìåþò âèä A T F� { }, , ãäå A — ìíîæåñòâî àáñòðàêòíûõ äàííûõ,
{ }T F, — ìíîæåñòâî èñòèííîñòíûõ çíà÷åíèé.
Áàçîâûìè êîìïîçèöèÿìè ôèíèòàðíûõ ïðîïîçèöèîíàëüíûõ ëîãèê åñòü êëèíèå-
âû îïåðàöèè � è � , èíôèíèòàðíûõ ïðîïîçèöèîíàëüíûõ ëîãèê — èíôèíèòàðíûå
ìíîæåñòâåííûå îïåðàöèè � K K, & è �K .
Íà ñèíãóëÿðíîì óðîâíå äàííûå òðàêòóþòñÿ ïðåäåëüíî êîíêðåòíî, êàê «áåëûå
ÿùèêè». Íà ýòîì óðîâíå ôèêñèðóåòñÿ åäèíûé êëàññ äàííûõ, êîòîðûé îáúÿñíÿåò åãî
íàçâàíèå. Êîìïîçèöèÿìè ñèíãóëÿðíîãî óðîâíÿ ÿâëÿþòñÿ êîíêðåòíûå àïïëèêàòèâ-
íûå êîìïîçèöèè. Äëÿ ñèíãóëÿðíûõ ëîãèê ïîñòðîåíà [11] èíôèíèòàðíàÿ àëãåáðà
ñèíãóëÿðíûõ êîìïîçèöèé Êëèíè.
Íà ñèíòåòè÷åñêèõ óðîâíÿõ D.P.S è D.H.S äàííûå ñòðîÿòñÿ èç ìíîæåñòâ ïðåäìåò-
íûõ èìåí è ïðåäìåòíûõ çíà÷åíèé. Íà ýòèõ óðîâíÿõ äàííûå ðàññìàòðèâàþòñÿ êàê «ñå-
ðûå ÿùèêè», ïîñòðîåííûå èç «áåëûõ» è «÷åðíûõ». Òàêèå äàííûå íàçûâàþò íîìèíà-
òèâíûìè, èëè íîìèíàòàìè. Îíè ñòðîÿòñÿ èíäóêòèâíî èç ìíîæåñòâà ïðåäìåòíûõ èìåí
è ìíîæåñòâà ïðåäìåòíûõ çíà÷åíèé. Ñèíòåòè÷åñêèå óðîâíè D.P.S è D.H.S íàçûâàþò
íîìèíàòèâíûìè, îíè î÷åíü áîãàòû è ðàñïàäàþòñÿ íà ðÿä ïîäóðîâíåé.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 33
Îäíîóðîâíåâûå îäíîçíà÷íûå íîìèíàòû íàçûâàþò èìåííûìè ìíîæåñòâà-
ìè (ÈÌ).
Ôóíêöèè è ïðåäèêàòû, çàäàííûå íà ÈÌ, íàçûâàþò êâàçèàðíûìè.
V-èìåííîå ìíîæåñòâî (V-ÈÌ) íàä A — ýòî [8] ïðîèçâîëüíàÿ îäíîçíà÷íàÿ
ôóíêöèÿ �: V A� . Ìíîæåñòâà V è A òðàêòóåì êàê ìíîæåñòâà ïðåäìåòíûõ èìåí è
ïðåäìåòíûõ çíà÷åíèé. Ìíîæåñòâî âñåõ V-ÈÌ íàä A îáîçíà÷èì V A .
V-ÈÌ ïðåäñòàâëÿåì â âèäå [ , ... , , ... ]v a v an n1 1� � . Çäåñü v Vi � , a Ai � ,
v vi j� ïðè i j� . Äëÿ V-ÈÌ ââîäèì ôóíêöèþ im AV V: � 2 , îïåðàöèè | | X è �:
im pr v V v a( ) ( ) [ | ]� � �� � � �1 � ;
� �| | [ | ]X v a v X� � �� ;
� � � � �1 2 2 1 2� � ( | | ( \ ( )))V im .
Âìåñòî � | | ( \ )V X áóäåì ïèñàòü � | |
X .  ÷àñòíîñòè, âìåñòî � | | ( \ )V x{ } ïèøåì
� | |
x .
Äëÿ V-ÈÌ îïåðàöèþ ðåíîìèíàöèè r
x x
v v
n
n
1
1
, ...,
, ...,
çàäàäèì òàê:
r v x v x
x x
v v
n n
n
n
1
1
1 1, ...,
, ...,
( ) [ ( ), ... , ( )] ( |� � � �� � � | ( \ , ... , )).V v vn{ }1
Ââåäÿ îáîçíà÷åíèå âèäà y äëÿ y yn1 , ... , , âìåñòî r
x x
v v
n
n
1
1
, ...,
, ...,
áóäåì ïèñàòü rx
v.
Ôóíêöèþ âèäà P A T FV: ,� { } íàçîâåì V-êâàçèàðíûì ïðåäèêàòîì íà A. Ôóíê-
öèþ âèäà f A AV: � íàçîâåì V-êâàçèàðíîé ôóíêöèåé íà A. Ìíîæåñòâà V-êâàçèàð-
íûõ ïðåäèêàòîâ è ôóíêöèé íà A îáîçíà÷èì ñîîòâåòñòâåííî PrA è FnA .
Îáëàñòüþ èñòèííîñòè è îáëàñòüþ ëîæíîñòè V-êâàçèàðíîãî ïðåäèêàòà P íà A
íàçîâåì ìíîæåñòâà T ( ) | ( )P d A P d TV� � �{ } è F( ) | ( )P d A P d FV� � �{ }.
V-êâàçèàðíûé ïðåäèêàò P (÷àñòè÷íî) èñòèííûé, èëè íåîïðîâåðæèìûé, åñëè
F( )P � �. V-êâàçèàðíûé ïðåäèêàò P âûïîëíè' ì, åñëè T ( )P � �.
Äëÿ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ (óðîâåíü D.P.S) âûäåëèì ðåíîìèíàòèâíûé,
êâàíòîðíûé, êâàíòîðíî-ýêâàöèîíàëüíûé, ôóíêöèîíàëüíûé, ôóíêöèîíàëüíî-ýêâà-
öèîíàëüíûé óðîâíè.
Ðàññìîòðèì ïîäðîáíåå ôèíèòàðíûå ëîãèêè óêàçàííûõ óðîâíåé.
Ðåíîìèíàòèâíûå ëîãèêè [8] íàèáîëåå àáñòðàêòíûå ñðåäè ëîãèê íîìèíàòèâ-
íûõ óðîâíåé. Íà÷èíàÿ ñ ðåíîìèíàòèâíîãî óðîâíÿ, ìîæíî ïåðåèìåíîâûâàòü êîìïî-
íåíòû äàííûõ. Ýòî ïîçâîëÿåò ââåñòè êîìïîçèöèþ ðåíîìèíàöèè (ïåðåèìåíîâàíèÿ)
Rx
v A APr Pr: � .
Äàäèì îïðåäåëåíèå ïðåäèêàòà Rx
v P( ) ÷åðåç åãî îáëàñòè èñòèííîñòè è
ëîæíîñòè:
T R T( ( )) ( ( ))x
v
x
vP r P� ; F R F( ( )) ( ( ))x
v
x
vP r P� .
Áàçîâûìè êîìïîçèöèÿìè ðåíîìèíàòèâíûõ ëîãèê åñòü � �, , Rx
v .
Íà êâàíòîðíîì óðîâíå ìîæíî ïðèìåíÿòü êâàçèàðíûå ïðåäèêàòû êî âñåì
ïðåäìåòíûì çíà÷åíèÿì. Ýòî ïîçâîëÿåò ââåñòè êîìïîçèöèè êâàíòèôèêàöèè �x è
x.
Äàäèì îïðåäåëåíèå ïðåäèêàòîâ �x è
x ÷åðåç èõ îáëàñòè èñòèííîñòè è
ëîæíîñòè:
T x( )� �P {d A P d x a TV� � �| ( )� äëÿ íåêîòîðîãî a A� };
F x( )� �P {d A P d x a FV� � �| ( )� äëÿ âñåõ a A� };
T x( )
�P {d A P d x a TV� � �| ( )� äëÿ âñåõ a A� };
F x( )
�P {d A P d x a FV� � �| ( )� äëÿ íåêîòîðîãî a A� }.
34 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
Áàçîâûìè êîìïîçèöèÿìè ëîãèê êâàíòîðíîãî óðîâíÿ åñòü � , � , Rx
v , �x .
Íà êâàíòîðíî-ýêâàöèîíàëüíîì óðîâíå ïîÿâëÿþòñÿ íîâûå âîçìîæíîñòè
îòîæäåñòâëåíèÿ è ðàçëè÷åíèÿ çíà÷åíèé ñ ïîìîùüþ ñïåöèàëüíûõ 0-àðíûõ êîìïîçè-
öèé — ïðåäèêàòîâ ðàâåíñòâà �xy . Áàçîâûìè êîìïîçèöèÿìè ëîãèê êâàíòîðíî-ýêâà-
öèîíàëüíîãî [12] óðîâíÿ åñòü �, � , Rx
v , � �x xy, .
Íà ôóíêöèîíàëüíîì óðîâíå èìååì ðàñøèðåííûå âîçìîæíîñòè ôîðìèðîâàíèÿ
íîâûõ àðãóìåíòîâ äëÿ ôóíêöèé è ïðåäèêàòîâ. Ýòî äàåò âîçìîæíîñòü ââåñòè êîìïî-
çèöèþ ñóïåðïîçèöèè Sx (ñì. [8]). Íà ôóíêöèîíàëüíîì óðîâíå ïðåäñòàâëÿåòñÿ åñ-
òåñòâåííûì ââåäåíèå ñïåöèàëüíûõ 0-àðíûõ êîìïîçèöèé — ôóíêöèé ðàçûìåíîâà-
íèÿ 'x . Ïðè ââåäåíèè òàêèõ ôóíêöèé êîìïîçèöèè ðåíîìèíàöèè ìîæíî ïðîìîäåëè-
ðîâàòü ñ ïîìîùüþ ñóïåðïîçèöèè. Áàçîâûìè êîìïîçèöèÿìè ëîãèê ôóíêöèîíàëüíîãî
óðîâíÿ åñòü � , � , S x , �x , 'x .
Íà ôóíêöèîíàëüíî-ýêâàöèîíàëüíîì óðîâíå ìîæíî äîïîëíèòåëüíî ââåñòè [8]
ñïåöèàëüíóþ êîìïîçèöèþ ðàâåíñòâà = . Áàçîâûìè êîìïîçèöèÿìè ëîãèê ôóíêöèî-
íàëüíî-ýêâàöèîíàëüíîãî óðîâíÿ åñòü � , � , S x , �x , ' x , = .
Íà óðîâíå D.H.S äàííûå ìîæíî ðàññìàòðèâàòü êàê èåðàðõè÷åñêèå íîìèíàòû,
îíè ñòðîÿòñÿ èíäóêòèâíî èç ìíîæåñòâ ïðåäìåòíûõ èìåí è ïðåäìåòíûõ çíà÷åíèé.
Ñîîòâåòñòâóþùèå ëîãèêè íàçâàíû ëîãèêàìè íîìèíàòèâíûõ äàííûõ, îíè èññëåäî-
âàíû, â ÷àñòíîñòè, â [13].
Ðàññìîòðèì òåïåðü êëàññû ïåðâîïîðÿäêîâûõ ÊÍË êâàçèàðíûõ ïðåäèêàòîâ. Õà-
ðàêòåðíûå ñâîéñòâà òàêèõ ëîãèê ïðîÿâëÿþòñÿ óæå íà êâàíòîðîì óðîâíå, ïîýòîìó
îãðàíè÷èìñÿ ðàññìîòðåíèåì ëîãèê êâàçèàðíûõ ïðåäèêàòîâ êâàíòîðíîãî óðîâíÿ.
2. ÊÎÌÏÎÇÈÖÈÎÍÍÎ-ÍÎÌÈÍÀÒÈÂÍÛÅ ËÎÃÈÊÈ ÊÂÀÇÈÀÐÍÛÕ ÏÐÅÄÈÊÀÒÎÂ
Ñåìàíòè÷åñêèìè ìîäåëÿìè ÊÍË êâàíòîðíîãî óðîâíÿ ÿâëÿþòñÿ êîìïîçèöèîííûå
ñèñòåìû êâàçèàðíûõ ïðåäèêàòîâ âèäà ( , , )VA Pr C . Ìíîæåñòâî C çàäàåòñÿ ìíî-
æåñòâîì áàçîâûõ êîìïîçèöèé {� , � , Rx
v , �x} . Ïðè ôèêñèðîâàííîì C ñèñòåìà
( , , )VA Pr C îäíîçíà÷íî îïðåäåëÿåòñÿ îáúåêòîì âèäà ( , )A Pr — íåîêëàññè÷åñêîé
àëãåáðàè÷åñêîé ñèñòåìîé (ÀÑ) [8].
Ðàññìîòðåíèå êîìïîçèöèîííûõ ñèñòåì ïðåäóñìàòðèâàåò íàëè÷èå ÿçûêà ëîãè-
êè, èíäóöèðîâàííîãî ñîîòâåòñòâóþùèìè èíòåíñèîíàëüíûìè ìîäåëÿìè (óðîâíÿìè
ðàññìîòðåíèÿ). Ýòî îçíà÷àåò íåîáõîäèìîñòü îáîçíà÷åíèÿ áàçîâûõ ïðåäèêàòîâ, èç
êîòîðûõ ñ ïîìîùüþ êîìïîçèöèé ñòðîÿòñÿ áîëåå ñëîæíûå ïðåäèêàòû.
Àëôàâèò ÿçûêà ÊÍË êâàíòîðíîãî óðîâíÿ ñîñòîèò èç òàêèõ ñèìâîëîâ: ñèìâîëû
áàçîâûõ êîìïîçèöèé, ìíîæåñòâî Ps ïðåäèêàòíûõ ñèìâîëîâ (ñèãíàòóðà ÿçûêà), ìíî-
æåñòâî V ïðåäìåòíûõ èìåí.
Äàäèì îïðåäåëåíèå ìíîæåñòâà Fr ôîðìóë ÿçûêà ÊÍË êâàíòîðíîãî óðîâíÿ
(ñì. [8]):
1) êàæäûé ïðåäèêàòíûé ñèìâîë (ÏÑ) ÿâëÿåòñÿ ôîðìóëîé, òàêèå ôîðìóëû
àòîìàðíûå;
2) åñëè � è � — ôîðìóëû, òî �� , � �� , Rx
v � , �x � — ôîðìóëû.
Êîíêðåòíàÿ èíòåðïðåòàöèÿ ÿçûêà îïðåäåëÿåòñÿ ÀÑ ( , )A Pr è çíà÷åíèÿìè ÏÑ íà A,
êîòîðûå çàäàåì ñ ïîìîùüþ òîòàëüíîãî îäíîçíà÷íîãî îòîáðàæåíèÿ I : Ps Pr� . Ïîýòî-
ìó ìîäåëÿìè ÿçûêà ÊÍË êâàíòîðíîãî óðîâíÿ áóäåì ñ÷èòàòü [8] ÀÑ ñ ïðèäàííîé ñèã-
íàòóðîé — îáúåêòû âèäà (( , ), )A Pr I , êîòîðûå ñîêðàùåííî îáîçíà÷èì ( , )A I .
Îòîáðàæåíèå èíòåðïðåòàöèè ôîðìóë J : Fr Pr� îïðåäåëÿåòñÿ ñ ïîìîùüþ I òàê:
1) J I( ) ( )p p� äëÿ êàæäîãî p Ps� ;
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 35
2) J ( )� �� � ( ( ))J � , J ( )� ��� �( ( ), ( ))J J� � , J ( )Rx
v � � Rx
v ( ( ))J � , J ( )� �x �
� �x ( ( ))J � .
Çäåñü áàçîâûå êîìïîçèöèè îáîçíà÷åíû ïîëóæèðíûì øðèôòîì, ñèìâîëû áàçî-
âûõ êîìïîçèöèé êàê ýëåìåíòû àëôàâèòà ÿçûêà — îáû÷íûì.
Ïðåäèêàò J ( )� — çíà÷åíèå ôîðìóëû � ïðè èíòåðïðåòàöèè íà A I� ( , )A —
îáîçíà÷èì �A .
Ôîðìóëà � (÷àñòè÷íî) èñòèííàÿ ïðè èíòåðïðåòàöèè íà A I� ( , )A , èëè A-íå-
îïðîâåðæèìàÿ, åñëè �A — íåîïðîâåðæèìûé ïðåäèêàò (îáîçíà÷èì A |� �).
Ôîðìóëà � âñþäó (÷àñòè÷íî) èñòèííàÿ, èëè íåîïðîâåðæèìàÿ, åñëè � A-íå-
îïðîâåðæèìàÿ äëÿ êàæäîé ìîäåëè ÿçûêà A (îáîçíà÷èì |� �).
Ôîðìóëà � — ëîãè÷åñêîå ñëåäñòâèå ôîðìóëû � (îáîçíà÷èì � �|� ), åñëè äëÿ
êàæäîé ìîäåëè ÿçûêà A èìååì T FA A( ) ( )� �� � �.
Ôîðìóëû � è � ëîãè÷åñêè ýêâèâàëåíòíû (îáîçíà÷èì � �� ), åñëè � �|� è
� �|� .
Ôîðìóëà � — ñëàáîå ëîãè÷åñêîå ñëåäñòâèå [8] ôîðìóëû � (îáîçíà÷èì
� �|| ) ,� åñëè äëÿ êàæäîé ìîäåëè ÿçûêà A èç óñëîâèÿ A |� � âûòåêàåò A |� �.
Ïóñòü � � Fr è � � Fr — íåêîòîðûå ìíîæåñòâà ôîðìóë;
� — ëîãè÷åñêîå ñëåäñòâèå � â ÀÑ A (� �A |� ), åñëè
T FA A( ) ( )� �
� � � �� �
� � �� � ;
� — ëîãè÷åñêîå ñëåäñòâèå � (îáîçíà÷èì � �|� ), åñëè � �A |� äëÿ êàæäîé ìî-
äåëè ÿçûêà A.
Êëàññ êâàçèàðíûõ ïðåäèêàòîâ î÷åíü ìîùíûé, äëÿ ëîãèê êâàçèàðíûõ ïðåäèêà-
òîâ íå âûïîëíÿþòñÿ íåêîòîðûå âàæíûå çàêîíû êëàññè÷åñêîé ëîãèêè. Íàïðèìåð,
â îáùåì ñëó÷àå ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ íå âñåãäà âûïîëíÿþòñÿ
�x� �|| ,
|�
�x� �, |� � �� �x .  òî æå âðåìÿ âñåãäà âûïîëíÿþòñÿ � �||�
x ,
| ( )�
�x x� � , | ( )� �
�x x� � , | ( )�
� �x x� � , | ( )� � � �x x� � .
Òàêèì îáðàçîì, äëÿ ñîõðàíåíèÿ îñíîâíûõ ñâîéñòâ êëàññè÷åñêîé ëîãèêè êëàññ
êâàçèàðíûõ ïðåäèêàòîâ ñëåäóåò îãðàíè÷èòü. Åñòåñòâåííîå îãðàíè÷åíèå çàäàåòñÿ
ñâîéñòâîì ýêâèòîííîñòè, êîòîðîå îçíà÷àåò, ÷òî çíà÷åíèå îòîáðàæåíèÿ íå èçìåíÿåò-
ñÿ ïðè ðàñøèðåíèè äàííûõ. Íåôîðìàëüíî ýòî îçíà÷àåò íåèçìåííîñòü óñòàíîâëåí-
íîãî çíàíèÿ.
Ïðåäèêàò P ýêâèòîííûé (ÝÏ), åñëè äëÿ ïðîèçâîëüíûõ d d AV, � � èç d d� � è
P d( )� âûòåêàåò P d P d( ) ( )� � � .
Áëèæàéøèìè ê êëàññè÷åñêîé ëîãèêå ÿâëÿþòñÿ ëîãèêè ïîëíîòîòàëüíûõ ýêâè-
òîííûõ ïðåäèêàòîâ. Ïîëíîòîòàëüíîñòü îçíà÷àåò îïðåäåëåííîñòü ïðåäèêàòà íà
ìàêñèìàëüíûõ äàííûõ — V-ïîëíûõ ÈÌ.
V-ÈÌ �V-ïîëíàÿ, åñëè im V( )� � . Ìíîæåñòâî âñåõ V-ïîëíûõ ÈÌ íàä A îáîçíà-
÷èì AV . Ïðåäèêàò P ïîëíîòîòàëüíûé, åñëè P d( )� äëÿ âñåõ d AV� .
Äëÿ ëîãèê ïîëíîòîòàëüíûõ ÝÏ ñòðîÿòñÿ [8] àêñèîìàòè÷åñêèå ñèñòåìû ãèëüáåð-
òîâñêîãî òèïà, äëÿ íèõ äîêàçûâàþòñÿ òåîðåìû íåïðîòèâîðå÷èâîñòè (êîððåêòíîñòè)
è ïîëíîòû. Ëîãèêè ïîëíîòîòàëüíûõ ÝÏ íàçâàíû íåîêëàññè÷åñêèìè [6], ïîñêîëüêó
ñîõðàíÿþò îñíîâíûå çàêîíû êëàññè÷åñêîé ëîãèêè ïðè ñóùåñòâåííîì ðàñøèðåíèè
êëàññà ìîäåëåé.
Ëîãèêè ýêâèòîííûõ ïðåäèêàòîâ òîæå ìîæíî îòíåñòè ê íåîêëàññè÷åñêèì, îíè
ñîõðàíÿþò îñíîâíûå çàêîíû êëàññè÷åñêîé ëîãèêè, íî äëÿ íèõ óæå íåâåðíû íåêîòî-
ðûå ïðàâèëà âûâîäà (modus ponens è ðîäñòâåííîå ïðàâèëî ñå÷åíèÿ), íàðóøàþòñÿ
íåêîòîðûå ñâîéñòâà êëàññè÷åñêîé ëîãèêè. Íàïðèìåð, äëÿ êîíêðåòíûõ ñåìàíòè÷åñ-
êèõ ìîäåëåé âîçìîæíî A |� P, A |� �P Q, íî A |� Q. Âîçìîæíî òàêæå A |� �P Q,
36 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
A |� �Q S , íî A |� �P S . Äëÿ ëîãèêè ÝÏ íåâåðíî � � � �&( ) ||� � , ïîýòîìó íå
âñåãäà èç � �|� âûòåêàåò � �||� .
Êëàññ ìîäåëåé ëîãèêè ÝÏ ñóùåñòâåííî øèðå êëàññà ìîäåëåé ëîãèêè
ïîëíîòîòàëüíûõ ÝÏ.
Ñåìàíòè÷åñêèå ñâîéñòâà ëîãèêè ÝÏ ôàêòè÷åñêè âîññîçäàþò ñâîéñòâà êîìïîçè-
öèé.  ÷àñòíîñòè, ñâîéñòâà, êîòîðûå íå èñïîëüçóþò ðåíîìèíàöèè è ñóïåðïîçèöèè, ïî-
ëíîñòüþ àíàëîãè÷íû ñîîòâåòñòâóþùèì ñâîéñòâàì êëàññè÷åñêîé ëîãèêè ïðåäèêàòîâ.
Äëÿ ëîãèêè ÝÏ âûïîëíÿþòñÿ [8] òåîðåìû ýêâèâàëåíòîñòè è ðàâåíñòâà, à îòíî-
ñèòåëüíî îòíîøåíèÿ ëîãè÷åñêîãî ñëåäñòâèÿ äëÿ ìíîæåñòâ ôîðìóë — òåîðåìà î çà-
ìåíå ýêâèâàëåíòíûõ. Äëÿ ôîðìóë ëîãèêè ÝÏ îïðåäåëÿþòñÿ ðàçíîêâàíòîðíûå, íîð-
ìàëüíûå, êâàçèçàìêíóòûå ôîðìóëû. Äîêàçûâàåòñÿ [8], ÷òî äëÿ êàæäîé ôîðìóëû
ìîæíî ïîñòðîèòü ýêâèâàëåíòíûå åé ðàçíîêâàíòîðíóþ è íîðìàëüíóþ.
Äëÿ ôîðìóë êëàññè÷åñêîé ëîãèêè ñóùåñòâåííûìè åñòü òîëüêî èõ ñâîáîäíûå
ïðåäìåòíûå èìåíà, îò êîòîðûõ ìîæåò çàâèñåòü çíà÷åíèå ñîîòâåòñòâóþùèõ ïðåäè-
êàòîâ. Äëÿ ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ âàæíà íåñóùåñòâåííîñòü ïðåäìåòíûõ
èìåí. Ïîýòîìó äëÿ áàçîâûõ ïðåäèêàòîâ áóäåì óêàçûâàòü ìíîæåñòâî íåñóùåñòâåí-
íûõ èìåí, îò êîòîðûõ íå çàâèñÿò çíà÷åíèÿ òàêèõ ïðåäèêàòîâ.
Èìÿ x V� ñòðîãî íåñóùåñòâåííîå äëÿ êâàçèàðíîãî ïðåäèêàòà P, åñëè äëÿ ïðî-
èçâîëüíûõ d AV� è a A� èìååì P d x a P d x( ) ( || )� �
� .
Èìÿ x V� íåñóùåñòâåííîå äëÿ êâàçèàðíîãî ïðåäèêàòà P, åñëè äëÿ ïðîèçâîëü-
íûõ d AV� è a b A, � èç P d x a( )� �� è P d x b( )� �� âûòåêàåò P d x a( )� ��
� �P d x b( )� .
Âîçìîæíîñòü âûïîëíåíèÿ ýêâèâàëåíòíûõ ïðåîáðàçîâàíèé ïðîèçâîëüíûõ ôîð-
ìóë òðåáóåò íàëè÷èÿ áåñêîíå÷íîãî ìíîæåñòâà òîòàëüíî íåñóùåñòâåííûõ èìåí, ò.å.
èìåí, íåñóùåñòâåííûõ äëÿ êàæäîãî p Ps� . Òàêèì îáðàçîì, ñåìàíòè÷åñêîé îñíîâîé
ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ ÿâëÿþòñÿ êîìïîçèöèîííûå àëãåáðû ñ äîïîëíèòåëü-
íûì òðåáîâàíèåì íàëè÷èÿ áåñêîíå÷íîãî ìíîæåñòâà òîòàëüíî ñòðîãî íåñóùåñòâåí-
íûõ (òîòàëüíî íåñóùåñòâåííûõ äëÿ ëîãèêè ÝÏ) ïðåäìåòíûõ èìåí.
Êâàçèçàìêíóòûå ôîðìóëû — ñèíòàêñè÷åñêèå àíàëîãè çàìêíóòûõ ôîðìóë êëàñ-
ñè÷åñêîé ëîãèêè, íî ñåìàíòè÷åñêèìè àíàëîãàìè çàìêíóòûõ ôîðìóë èõ ñ÷èòàòü íå-
ëüçÿ. Êâàçèçàìêíóòûå ôîðìóëû íåîáÿçàòåëüíî èíòåðïðåòèðóþòñÿ êàê êîíñòàíòíûå
ïðåäèêàòû, õîòÿ äëÿ êëàññè÷åñêîé ëîãèêè êàæäàÿ çàìêíóòàÿ ôîðìóëà íà êàæäîé
ìîäåëè ÿçûêà âñåãäà èíòåðïðåòèðóåòñÿ êàê òîæäåñòâåííàÿ èñòèíà èëè òîæäåñòâåí-
íàÿ ëîæü. Äåëî â òîì, ÷òî â ñîñòàâ ôîðìóëû ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ ìîãóò
âõîäèòü ïðåäèêàòíûå ñèìâîëû, äëÿ êîòîðûõ ìíîæåñòâà ñóùåñòâåííûõ èìåí áåñêî-
íå÷íû. Âîçìîæíîñòü äëÿ ôîðìóëû áûòü çàâèñèìîé îò áåñêîíå÷íîãî ìíîæåñòâà
ïðåäìåòíûõ èìåí — îïðåäåëÿþùåå ñâîéñòâî ëîãèê êâàçèàðíûõ ïðåäèêàòîâ, êîòî-
ðîå ñóùåñòâåííûì îáðàçîì îòëè÷àåò èõ îò êëàññè÷åñêîé ëîãèêè.
Åñòåñòâåííûì îáîáùåíèåì ÝÏ åñòü ëîêàëüíî-ýêâèòîííûå ïðåäèêà-
òû (ËÝÏ) [8]. Äëÿ ËÝÏ òðåáóåòñÿ ñîõðàíåíèå çíà÷åíèÿ ïðè ðàñøèðåíèè äàííûõ
ëèøü íà êîíå÷íîå ÷èñëî èìåíîâàííûõ êîìïîíåíò.
Ïðåäèêàò P ëîêàëüíî-ýêâèòîííûé, åñëè äëÿ ïðîèçâîëüíûõ d d AV, ,� èç òîãî,
÷òî P d( )�, d d� � è d d� \ êîíå÷íîå, âûòåêàåò P d P d( ) ( )� � � . Òî, ÷òî êëàññ ËÝÏ ÿâ-
ëÿåòñÿ ðàñøèðåíèåì êëàññà ÝÏ, ïîêàçûâàåò ïðèìåð ïðåäèêàòà, èñòèííîãî íà âñåõ
êîíå÷íûõ ÈÌ è ëîæíîãî íà âñåõ áåñêîíå÷íûõ ÈÌ. Òàêîé ïðåäèêàò ëîêàëüíî-ýêâè-
òîííûé, íî íåýêâèòîííûé.
Ñåìàíòè÷åñêèå ñâîéñòâà ËÝÏ àíàëîãè÷íûå ñâîéñòâàì ÝÏ. Êëàññ ìîäåëåé ëî-
ãèêè ËÝÏ — ðàñøèðåíèå êëàññà ìîäåëåé ëîãèêè ÝÏ.
Ëîãèêè, îðèåíòèðîâàííûå íà òàêèå îñîáåííîñòè ïðåäìåòíûõ îáëàñòåé, êàê íå-
îïðåäåëåííîñòü, íåïîëíîòà èìåþùåéñÿ èíôîðìàöèè, áàçèðóþòñÿ íà êëàññàõ ïðåäè-
êàòîâ, îïðåäåëåííûõ íà äàííûõ ñ íåïîëíîé èíôîðìàöèåé, ýòî ýêâèñîâìåñòíûå
ïðåäèêàòû (ÝÑÏ) è ëîêàëüíî-ýêâèñîâìåñòíûå ïðåäèêàòû (ËÝÑÏ) [8].
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 37
Ýêâèñîâìåñòíîñòü ïðåäèêàòà P îçíà÷àåò, ÷òî ïðè âîçìîæíîñòè ðàñøèðåíèÿ
ðàçíûõ äàííûõ (ñîâìåñòíîñòü äàííûõ) îäíèì áîëüøèì äàííûì çíà÷åíèÿ P íà òà-
êèõ äàííûõ äîëæíû ñîâïàäàòü. Äëÿ ËÝÑÏ òðåáóåòñÿ ñîõðàíåíèå çíà÷åíèé ëèøü
äëÿ ðàñøèðåíèé êîíå÷íîé èíôîðìàöèåé.
ÈÌ d è d � ñîâìåñòíûå (îáîçíà÷àåì d d� �), åñëè ôóíêöèÿ d d � îäíîçíà÷íàÿ.
Ïðåäèêàò P ÝÑÏ, åñëè äëÿ ïðîèçâîëüíûõ d d AV, �� èç d d� �, P d( )� è P d( )� �
âûòåêàåò P d P d( ) ( )� � .
Ïðåäèêàò P ËÝÑÏ, åñëè äëÿ ïðîèçâîëüíûõ d d AV, �� òàêèõ, ÷òî
( \ ) ( \ )d d d d� � êîíå÷íîå, èç d d� �, P d( )� è P d( )� � âûòåêàåò P d P d( ) ( )� � .
ÝÑÏ è ËÝÑÏ ÿâëÿþòñÿ îáîáùåíèÿìè ÝÏ è ËÝÏ. Ñâîéñòâà ëîãèê ÝÑÏ è
ËÝÑÏ àíàëîãè÷íû ñîîòâåòñòâóþùèì ñâîéñòâàì ëîãèê ÝÏ è ËÝÏ. Êëàññû ñåìàíòè-
÷åñêèõ ìîäåëåé ëîãèê ÝÑÏ è ËÝÑÏ åùå øèðå, õîòÿ ýòè ëîãèêè ñîõðàíÿþò îñíîâ-
íûå çàêîíû êëàññè÷åñêîé ëîãèêè.
Îòêàç îò modus ponens âåäåò ê íåîáõîäèìîñòè èññëåäîâàíèÿ ñèíòàêñè÷åñêèõ
ñâîéñòâ ëîãèê ÝÏ, ËÝÏ, ÝÑÏ è ËÝÑÏ íà áàçå íå ãèëüáåðòîâñêèõ, à ãåíöåíîâñêèõ
ñèñòåì — ñåêâåíöèàëüíûõ èñ÷èñëåíèé [5]. Òàêèå èñ÷èñëåíèÿ ïîñòðîåíû â [8]. Ñå-
ìàíòè÷åñêîé îñíîâîé èõ ïîñòðîåíèÿ åñòü ñâîéñòâà îòíîøåíèÿ ëîãè÷åñêîãî ñëåä-
ñòâèÿ äëÿ ìíîæåñòâ ôîðìóë. Äëÿ ïîñòðîåííûõ ñåêâåíöèàëüíûõ èñ÷èñëåíèé
äîêàçàíû òåîðåìû êîððåêòíîñòè è ïîëíîòû.
3. ÎÒÍÎØÅÍÈÅ ËÎÃÈ×ÅÑÊÎÃÎ ÑËÅÄÑÒÂÈß
 ËÎÃÈÊÀÕ ÊÂÀÇÈÀÐÍÛÕ ÏÐÅÄÈÊÀÒÎÂ
Äëÿ îáùåãî ñëó÷àÿ ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ çíà÷åíèÿ ïðåäèêàòà P íà äàí-
íîì d ìîãóò áûòü ðàçíûìè, â çàâèñèìîñòè îò òîãî, âõîäèò ëè â d êîìïîíåíòà
ñ íåêîòîðûì ïðåäìåòíûì èìåíåì, âåäü óñëîâèå ýêâèòîííîñòè íå âûïîëíÿåòñÿ.
Ïîýòîìó ïðè èíòåðïðåòàöèÿõ ôîðìóë íà ìîäåëÿõ ÿçûêà íåîáõîäèìî ÿâíûì îá-
ðàçîì óêàçûâàòü ìíîæåñòâà îçíà÷åííûõ è íåîçíà÷åííûõ èìåí, ò.å. èìåí, êîòî-
ðûå èìåþò èëè íå èìåþò çíà÷åíèÿ íà ìíîæåñòâå áàçîâûõ äàííûõ.
Ââåäåì ïîíÿòèå X –Y -çíà÷íîãî èìåííîãî ìíîæåñòâà, X –Y -çíà÷íûõ îáëàñòåé
èñòèííîñòè è ëîæíîñòè êâàçèàðíîãî ïðåäèêàòà, íà ýòîé îñíîâå èññëåäóåì ïîíÿòèå
X –Y -çíà÷íîãî ëîãè÷åñêîãî ñëåäñòâèÿ.
3.1. X–Y-çíà÷íûå èìåííûå ìíîæåñòâà. Ìíîæåñòâà X Y, íàçûâàþò äè-
çúþíêòíûìè, åñëè X Y� � �. Äëÿ ïðîèçâîëüíûõ äèçúþíêòíûõ ìíîæåñòâ X Y V, �
ìíîæåñòâî X –Y -çíà÷íûõ V-ÈÌ çàäàäèì òàê:
V X Y VA d A X im d, | ( )
� � �{ è Y im d� �( ) = } .
Åñëè Y � � , òî ïîëó÷àåì ìíîæåñòâî X -îçíà÷åííûõ V-ÈÌ:
V X VA d A X im d, | ( )� � �{ }.
Äëÿ ñëó÷àÿ X � � ïîëó÷àåì ìíîæåñòâî Y -íåîçíà÷åííûõ V-ÈÌ:
V Y VA d A Y im d, | ( )
� � � � �{ }.
Ïîíÿòíî, ÷òî V X Y V X V YA A A, , ,
� � .
Èç îïðåäåëåíèé ïîëó÷àåì òàêèå ñîîòíîøåíèÿ:
V X Z V X V ZA A A, , , � � ,
V Y Z V Y V ZA A A, ( ) , ,
� � .
38 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
Äëÿ ïðîèçâîëüíûõ äèçúþíêòíûõ ìíîæåñòâ X Y V, � èìååì
V V X Y V X Y V Y X V X YA A A A A�
, , , , ( ) .
Ðàññìîòðèì ñëåäóþùèå ïðåäñòàâëåíèÿ X –Y -çíà÷íûõ V-ÈÌ.
Óòâåðæäåíèå 1. Ïóñòü X , W, U V� — äèçúþíêòíûå ìíîæåñòâà ïðåäìåòíûõ
èìåí. Òîãäà V W U V W Y U X Y
Y X
A A, , ( \ )
�
� � .
Çäåñü W U òðàêòóåì êàê ìíîæåñòâî çàäåéñòâîâàííûõ â äàííûé ìîìåíò èìåí,
ïðè ýòîì W — ìíîæåñòâî îçíà÷åííûõ çàäåéñòâîâàííûõ èìåí, U — ìíîæåñòâî íå-
îçíà÷åííûõ çàäåéñòâîâàííûõ èìåí; X òðàêòóåì êàê ìíîæåñòâî íîâûõ èìåí, êîòî-
ðûå ïðèáàâëÿþòñÿ ê çàäåéñòâîâàííûì.
Óòâåðæäåíèå 2. Ïóñòü Z G V, � — äèçúþíêòíûå ìíîæåñòâà ïðåäìåòíûõ èìåí.
Òîãäà V G V G Y Z Y
Y Z
A A, , \�
�
� .
 ÷àñòíîñòè, ïðè G � � èìååì V V Y Z Y
Y Z
A A�
�
, \
� .
Çäåñü G òðàêòóåì êàê ìíîæåñòâî ãàðàíòèðîâàíî îçíà÷åííûõ çàäåéñòâîâàííûõ
èìåí, Z G — êàê ìíîæåñòâî çàäåéñòâîâàííûõ èìåí.
3.2. X–Y-çíà÷íûå îáëàñòè èñòèííîñòè è ëîæíîñòè êâàçèàðíûõ ïðåäèêà-
òîâ. Îïðåäåëèì X –Y -çíà÷íûå îáëàñòè èñòèííîñòè è ëîæíîñòè êâàçèàðíîãî ïðåäè-
êàòà P, ãäå äèçúþíêòíûå X Y V, � . X –Y -çíà÷íîñòü ñîñòîèò â òîì, ÷òî ïðèíèìàåì âî
âíèìàíèå òîëüêî òå d AV� , äëÿ êîòîðûõ X im d� ( ) è Y im d� � �( ) , ò.å.
d AV X Y�
, .  òàêèõ d èìåíà èç X èìåþò çíà÷åíèå, èìåíà èç Y íå èìåþò çíà÷åíèÿ:
TX Y
V V X YP d A P d T X im d Y im d d A
� � � � � � � � �( ) | ( ) , ( ), ( ) |,{ } { P d T( ) � };
FX Y
V V X YP d A P d F X im d Y im d d A
� � � � � � � � �( ) | ( ) , ( ), ( ) |,{ } { P d F( ) � }.
Åñëè Y � � , ïîëó÷àåì X -îçíà÷åííûå îáëàñòè èñòèííîñòè è ëîæíîñòè ïðåäèêà-
òà P :
TX
V V XP d A P d T X im d d A P d T( ) | ( ) , ( ) | ( ),� � � � � � �{ } { };
FX
V V XP d A P d F X im d d A P d F( ) | ( ) , ( ) | ( ),� � � � � � �{ } { }.
Ïîíÿòíî, ÷òî T T TX Y XP P P
� �( ) ( ) ( ) è F F FX Y XP P P
� �( ) ( ) ( ) .
Òåîðåìà 1. Äëÿ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ âûïîëíÿþòñÿ òàêèå ñîîòíîøå-
íèÿ:
T TY Z y
x
Y ZR P x P
� �( ( )) ( ( )) ïðè óñëîâèè y Y� , (TR�)
F FY Z Y Z y
xxP R P
� �( ) ( ( )) ïðè óñëîâèè y Y� , (FR�)
T TY Z Y Z y
xxP R P
�( ) ( ( )) ïðè óñëîâèè y Y� , (TR
)
F FY Z y
x
Y ZR P xP
�
( ( )) ( ) ïðè óñëîâèè y Y� . (FR
)
Ïóñòü d R PY Z y
x�
T ( ( )) è y Y� , òîãäà y Y� , Y im d� ( ) , Z im d� � �( ) è
R P d Ty
x ( )( ) � , îòêóäà y im d� ( ) , è P d x d y T( ( ))� �� .  ñèëó y im d� ( ) èìååì
d y a( )� äëÿ íåêîòîðîãî a A� . Îòñþäà P d x a T( )� �� äëÿ íåêîòîðîãî a A� è
y Y im d� � ( ) , îòêóäà � �xP d T( ) è y Y im d� � ( ) . Ó÷èòûâàÿ Z im d� � �( ) , ïîëó÷à-
åì d T xPY Z� �
( ) . Èòàê, ïðè óñëîâèè y Y� èìååì T TY Z y
x
Y ZR P xP
� �( ( )) ( ) .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 39
Ïóñòü d xPY Z� �
F ( ) è y Y� , òîãäà y Y� , Y im d� ( ) , Z im d� � �( ) è
P d x b F( )� �� äëÿ âñåõ b A� .  ñèëó y im d� ( ) èìååì d y a( )� äëÿ íåêîòîðîãî
a A� , òîãäà P d x d y F( ( ))� �� . Îòñþäà R P d Fy
x ( )( ) � è y Y im d� � ( ) . Ó÷èòûâàÿ
Z im d� � �( ) , ïîëó÷àåì d R PY Z y
x�
F ( ( )) . Èòàê, ïðè óñëîâèè y Y� èìååì
F FY Z Y Z y
xxP R P
� �( ) ( ( )) .
Ïóñòü d xPY Z�
T ( ) è y Y� , òîãäà y Y� , Y im d� ( ) , Z im d� � �( ) è
P d x b T( )� �� äëÿ âñåõ b A� .  ñèëó y im d� ( ) èìååì d y a( )� äëÿ íåêîòîðîãî
a A� , òîãäà P d x d y T( ( ))� �� . Îòñþäà R P d Ty
x ( )( ) � è y Y im d� � ( ) . Ó÷èòûâàÿ
Z im d� � �( ) , ïîëó÷àåì d R PY Z y
x�
T ( ( )) . Èòàê, ïðè óñëîâèè y Y� èìååì
T TY Z Y Z y
xxP R P
�( ) ( ( )) .
Ïóñòü d R PY Z y
x�
F ( ( )) è y Y� , òîãäà y Y� , Y im d� ( ) , Z im d� � �( ) è
R P d Fy
x ( )( ) � , îòêóäà y im d� ( ) è P d x d y F( ( ))� �� .  ñèëó y im d� ( ) èìååì
d y a( )� äëÿ íåêîòîðîãî a A� . Îòñþäà P d x a F( )� �� äëÿ íåêîòîðîãî a A� è
y Y im d� � ( ) , îòêóäà
�xP d F( ) è y Y im d� � ( ) . Åñëè Z im d� � �( ) , òî
d xPY Z�
F ( ) . Èòàê, ïðè y Y� èìååì F FY Z y
x
Y ZR P xP
�
( ( )) ( ) .
Äëÿ ôîðìóë âèäà Rx
v � ââåäåì ïîíÿòèå Y -íåîçíà÷èâàåìîé ôîðìû. Çäåñü
Y V� — ïðîèçâîëüíîå ìíîæåñòâî ïðåäìåòíûõ èìåí, êîòîðûå áóäåì òðàêòîâàòü
êàê íåîçíà÷åííûå, ò.å. íå èìåþùèå çíà÷åíèé. Ïðè èíòåðïðåòàöèÿõ âñå èìåíà èç Y
íå ìîãóò èìåòü çíà÷åíèé.
Ïóñòü R
s s y y v v
r r x x u u
k n m
k n m
1 1 1
1 1 1
, , , , ,
, , , , ,
� � �
� � � � òàêàÿ, ÷òî âñå r r s s y y Yk k n1 1 1, , , , , , , ,� � � � ,
âñå x x Yn1 , ,� � .
Y -íåîçíà÷èâàåìîé ôîðìîé ôîðìóëû R
s s y y v v
r r x x u u
k n m
k n m
1 1 1
1 1 1
, , , , ,
, , , , ,
� � �
� � � � íàçîâåì âûðàæå-
íèå âèäà R
v v
x x u u
m
n m
� �, , , , ,
, , , ,
� �
� �
1
1 1 �, ãäå � — ñïåöèàëüíûé ñèìâîë, êîòîðûé îáîçíà÷àåò íå-
îïðåäåëåííîå çíà÷åíèå.
Ïóñòü Rx
v � è R y
u � èìåþò îäèíàêîâûå Y -íåîçíà÷èâàåìûå ôîðìû. Òîãäà äëÿ âñåõ
ìîäåëåé ÿçûêà A ïðåäèêàòû Rx
v
A� è R y
u
A� ïðèíèìàþò îäèíàêîâûå çíà÷åíèÿ íà
äàííûõ d AV Y�
, , ãäå âñå èìåíà èç Y íå èìåþò çíà÷åíèé: R d R dx
v
A y
u
A� �( ) ( )� .
3.3. X–Y-çíà÷íûå îòíîøåíèÿ ëîãè÷åñêîãî ñëåäñòâèÿ. Îòíîøåíèå ñëåäñòâèÿ
A |� äëÿ äâóõ ôîðìóë ïðè ôèêñèðîâàííîé ìîäåëè ÿçûêà A ìîæíî îïðåäåëèòü òàê:
� �A |� , åñëè äëÿ âñåõ d AV� íåâåðíî (�A d T( ) � è �A d F( ) � ).
Ýòî îçíà÷àåò, ÷òî T F( ) ( )� �A A� � � .
Äëÿ ïðîèçâîëüíûõ äèçúþíêòíûõ ìíîæåñòâ ïðåäìåòíûõ èìåí X Y V, � îïðåäåëèì
X –Y -çíà÷íîå îòíîøåíèå ñëåäñòâèÿ A, X Y
�| äëÿ äâóõ ôîðìóë ïðè ôèêñèðîâàííîé A :
� �A , |X Y
� , åñëè äëÿ âñåõ d AV X Y�
, íåâåðíî (�A d T( ) � è �A d F( ) � ) .
Åñëè Y � �, òî ïîëó÷àåì X -îçíà÷åííîå îòíîøåíèå ñëåäñòâèÿ A , |X � äëÿ äâóõ
ôîðìóë ïðè ôèêñèðîâàííîé ìîäåëè ÿçûêà A :
� �A , |X � , åñëè äëÿ âñåõ d AV X� , íåâåðíî (�A d T( ) � è �A d F( ) � ) .
Äëÿ ñëó÷àÿ X � � ïîëó÷àåì Y -íåîçíà÷åííîå îòíîøåíèå ñëåäñòâèÿ A , |
�Y äëÿ
äâóõ ôîðìóë ïðè ôèêñèðîâàííîé ìîäåëè ÿçûêà A :
� �A , |
�Y , åñëè äëÿ âñåõ d AV Y�
, íåâåðíî (�A d T( ) � è �A d F( ) � ) .
40 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
Ïîíÿòíî, ÷òî � � � �A A,, | |X X Y� � �
è � � � �A A, ,| |
� � �Y X Y .
Íåïîñðåäñòâåííî èç îïðåäåëåíèé âûòåêàþò ñëåäóþùèå óòâåðæäåíèÿ.
Óòâåðæäåíèå 3. Îòíîøåíèå A, X Y
�| ðåôëåêñèâíîå è òðàíçèòèâíîå.
Óòâåðæäåíèå 4. � � � � � �A A A| | |, ,� � � � �
X X Y ;
� � � � � �A A A| | |, ,� � � � �
Y X Y .
Óòâåðæäåíèå 5. Äëÿ ïðîèçâîëüíîãî W V� âûïîëíÿåòñÿ ñîîòíîøåíèå
� �A |� � äëÿ êàæäîé X V� èìååì � �A , \ |X W X
� .
Óòâåðæäåíèå 6. � � � �A , | ( ) ( )X X A X AT F� � � � � ;
� � � �A , | ( ) ( )X Y X Y A X Y AT F
� � � � � .
Ïðèíèìàÿ âî âíèìàíèå òåîðåìó 1, ïîëó÷àåì ñëåäóþùóþ òåîðåìó.
Òåîðåìà 2. Ïðè óñëîâèè z X� âûïîëíÿþòñÿ R xz
x
X Y( ) |,� �A
� � è
�
x RX Y z
x� �A , | ( ) .
Ðàñïðîñòðàíèì ïîíÿòèå X –Y -çíà÷íîãî ëîãè÷åñêîãî ñëåäñòâèÿ ïðè ôèêñèðî-
âàííîé ìîäåëè ÿçûêà A íà ïðîèçâîëüíûå ìíîæåñòâà ôîðìóë � � Fr è � � Fr.
� åñòü X –Y -çíà÷íûì ëîãè÷åñêèì ñëåäñòâèåì � â ÀÑ A (îáîçíà÷èì
� �A , |X Y
� ), åñëè äëÿ âñåõ d AV X Y�
, íåâåðíî (äëÿ âñåõ � �� �A d T( ) � è äëÿ
âñåõ � �� �A d F( ) � ) .
Èç îïðåäåëåíèé âûòåêàþò ñëåäóþùèå óòâåðæäåíèÿ.
Óòâåðæäåíèå 7. � � � � � �A A A| | |, ,� � � � �
X X Y ;
� �A |� � � A , |
�Y � � �� �
A , |X Y .
Óòâåðæäåíèå 8. � � � �
� � � �
A , | ( ) ( )X X A X AT F� � � � �
� �
� � ;
� � � �
� � � �
A , | ( ) ( )X Y X Y A X Y AT F
�
�
� � � � �� � .
Ó÷èòûâàÿ óòâåðæäåíèÿ 1 è 2, ïîëó÷àåì ñëåäóþùóþ òåîðåìó.
Òåîðåìà 3. 1. Ïóñòü X W U V, , � — äèçúþíêòíûå ìíîæåñòâà ïðåäìåòíûõ
èìåí. Òîãäà
� �A , |W U
� � äëÿ êàæäîé Y X� èìååì � �A , |W Y U (X \Y)
� .
2. Ïóñòü Z G V, � — äèçúþíêòíûå ìíîæåñòâà ïðåäìåòíûõ èìåí. Òîãäà
� �A , |G � � äëÿ êàæäîé Y Z� èìååì � �A , \ |G Y Z Y
� .
Äëÿ óïðîùåíèÿ îáîçíà÷èì TX Y A
�
( )�
� �
� êàê TX Y A
( )� , TX Y A
�
( )�
� �
� êàê
TX Y A
( )� , FX Y A
�
( )�
� �
� êàê FX Y A
( )� , FX Y A
�
( )�
� �
� êàê FX Y A
( )� .
Àíàëîãè÷íî ââîäèì îáîçíà÷åíèÿ T T F FX A X A X A X A( ) , ( ) , ( ) , ( )� � � � .
Òåîðåìà 4. Äëÿ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ ïðè óñëîâèè z X� èìååì:
1) � � � � � � �A A, ,| , , ( ) | ,X Y z
x
X Yx R x
� � � � � ;
2) � � � � � � �, , ( ) | , |, ,
� �
�
x R xz
x
X Y X YA A .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 41
Ñîãëàñíî FR� ïðè óñëîâèè z X� èìååì F FX Y A X Y z
x
Ax R
� �( ) ( ( ) )� � ,
ïîýòîìó F F FX Y z
x
A X Y A X Y AR x x
� � � �( ( ) ) ( ) ( )� � � . Îòñþäà èç TX Y A
�( )�
� FX Y A
( )� � FX Y z
x
AR
( ( ) )� � FX Y Ax
� � �( )� èìååì TX Y A
( )� �
� � � � �
F FX Y A X Y Ax( ) ( ) ,� � ò.å. � � A , |X Y
� �x� R z
x
X Y( ) | ,,� � �� �
A �x� .
Ñîãëàñíî TR
ïðè óñëîâèè z X� èìååì T TX Y A X Y z
x
Ax R
�( ) ( ( ) )� � , ïî-
ýòîìó T T TX Y z
x
A X Y A X Y AR x x
�
�
( ( ) ) ( ) ( )� � � . Îòñþäà èç TX Y A
( )� �
�
TX Y z
x
AR( ( ) )� � TX Y Ax
( )� � FX Y A
� �( )� è ì å å ì TX Y A
( )� �
�
TX Y Ax( )� � FX Y A
� �( )� , ò .å . � ,
x � , R z
x
X Y( ) |,� � �A
� � ,
�
x X Y� �A , | .
Óæå íà ïðîïîçèöèîíàëüíîì óðîâíå âûïîëíÿåòñÿ ñâîéñòâî:
U) ïóñòü � �|� è � !� , òîãäà � !|� ; ïóñòü � �|� è � "� , òîãäà " �|� .
Ó÷èòûâàÿ ýòî ñâîéñòâî, èç òåîðåìû 4 ïîëó÷àåì ñëåäñòâèå.
Ñëåäñòâèå 1. Äëÿ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ ïðè óñëîâèè z X� èìååì:
1) � �A , |X Y
� , �x � , R z
x
X Y( ) |,� � �� �
A , �x � ;
2) � � � � � � �, , ( ) | , |, ,
� �
�
x R xz
x
X Y X YA A .
Òåîðåìà 5. Äëÿ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ ïðè óñëîâèè z X� èìååì:
1) � � � � � �, | , ( ) |, ,� � � �
x RX Y z
x
X YA A ;
2) � � � � #� �A A, ,| , | ),X Y X Y z
xx R
�
� � .
Ñîãëàñíî TR� ïðè óñëîâèè z X� èìååì T TX Y z
x
A X Y AR x
� �( ( ) ) ( )� � .
Îòñþäà èç TX Y A
�( )� TX Y Ax
�( )� � FX Y A
� �( )� èìååì TX Y A
( )� �
� TX Y z
x
AR
( ( ) )� � FX Y A
� �( )� , ò .å . ïîëó÷àåì � , � �
x X Y� �A , | �
� � , R z
x
X Y( ) |,� �A
� .
Ñîãëàñíî FR
ïðè óñëîâèè z X� èìååì F FX Y z
x
A X Y AR x
�
( ( ) ) ( )� � .
Îòñþäà èç T F FX Y A X Y A X Y Ax
�
� � �( ) ( ) ( )� � � èìååì TX Y A
�( )�
� � � �
F FX Y z
x
A X Y AR( ( ) ) ( )� � , ò .å . ïîëó÷àåì � �A , |X Y x
�
, � �
� #�A , | )X Y z
xR
� , � .
Äëÿ îáùåãî ñëó÷àÿ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ âûïîëíÿåòñÿ ñëåäóþùàÿ
òåîðåìà.
Òåîðåìà 6. Ïóñòü z òîòàëüíî ñòðîãî íåñóùåñòâåííîå è z nm� ( , , )� � � . Òîãäà:
1) R xz
x
A A#� � � � � �), | , |� � � � ;
2) � #� � � � �A z
x
AR x| ), | ,� � �
.
Èç òåîðåì 5 è 6 ïîëó÷àåì ñëåäñòâèå.
Ñëåäñòâèå 2. Ïóñòü z òîòàëüíî íåñóùåñòâåííîå è z nm� ( , , )� � � . Òîãäà ïðè
óñëîâèè z X� èìååì:
1) � � � � � �, | , ( ) |, ,� � � �
x RX Y z
x
X YA A ;
2) � � � � #� �A A, ,| , | ),X Y X Y z
xx R
�
� � .
4. ÑÅÊÂÅÍÖÈÀËÜÍÎÅ ÈÑ×ÈÑËÅÍÈÅ ËÎÃÈÊ ÊÂÀÇÈÀÐÍÛÕ ÏÐÅÄÈÊÀÒÎÂ
Ôîðìàëüíî-àêñèîìàòè÷åñêèå ñèñòåìû, êîòîðûå ôîðìàëèçóþò îòíîøåíèå ëîãè÷åñ-
êîãî ñëåäñòâèÿ ìåæäó äâóìÿ ìíîæåñòâàìè ôîðìóë, íàçûâàþò ñåêâåíöèàëüíûìè
èñ÷èñëåíèÿìè. Îñíîâíûå îáúåêòû òàêèõ ñèñòåì — ñåêâåíöèè, ðîëü ïðàâèë
âûâîäà èãðàþò ñåêâåíöèàëüíûå ôîðìû.
42 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
4.1. Èñ÷èñëåíèå ñåêâåíöèé ñïåöèôèöèðîâàííûõ ôîðìóë. Ñåêâåíöèè òðàê-
òóåì (ñì. [14, 15, 8]) êàê ìíîæåñòâà ñïåöèôèöèðîâàííûõ ôîðìóë. Êàæäàÿ ôîðìóëà
ñåêâåíöèè îòìå÷åíà (ñïåöèôèöèðîâàíà) ñëåâà îäíèì èç äâóõ ñèìâîëîâ — |
èëè
| . Ñåêâåíöèè îáîçíà÷àåì â âèäå | |
� � , ãäå âñå ôîðìóëû ìíîæåñòâà � ñïå-
öèôèöèðîâàíû ñèìâîëîì |
, âñå ôîðìóëû ìíîæåñòâà � — ñèìâîëîì
| . Íå äåòà-
ëèçèðóÿ, ñåêâåíöèè ñïåöèôèöèðîâàííûõ ôîðìóë îáîçíà÷àåì ! .
Ñåêâåíöèàëüíîå èñ÷èñëåíèÿ ñòðîèòñÿ òàê, ÷òî ñåêâåíöèÿ | |
� � âûâîäèìà
� �� �| .
Ñåìàíòè÷åñêèì ñâîéñòâàì îòíîøåíèÿ |� (ñì. [8, 15]) ñîïîñòàâëÿþòñÿ èõ ñèíòàêñè-
÷åñêèå àíàëîãè — ñåêâåíöèàëüíûå ôîðìû. Îíè ÿâëÿþòñÿ ïðàâèëàìè âûâîäà ñåê-
âåíöèàëüíûõ èñ÷èñëåíèé. Ñåêâåíöèàëüíûå ôîðìû áóäåì çàïèñûâàòü â âèäå
!
$
èëè
! "
$
. Ðîëü àêñèîì ñåêâåíöèàëüíîãî èñ÷èñëåíèÿ èãðàþò çàìêíóòûå ñåêâåíöèè. Ïî-
íÿòèå çàìêíóòîé ñåêâåíöèè â ðàçíûõ âàðèàíòàõ ñåêâåíöèàëüíîãî èñ÷èñëåíèÿ óòî÷-
íÿåòñÿ ïî-ðàçíîìó. Ïðè ýòîì äîëæíî âûïîëíÿòüñÿ óñëîâèå: åñëè ñåêâåíöèÿ | |
� �
çàìêíóòà, òî � �|� .
Âûâîä â ñåêâåíöèàëüíûõ èñ÷èñëåíèÿõ èìååò âèä äåðåâà, âåðøèíàìè êîòîðîãî
âûñòóïàþò ñåêâåíöèè. Òàêèå äåðåâüÿ íàçûâàþò ñåêâåíöèàëüíèìè. Ñåêâåíöèàëüíîå
äåðåâî çàìêíóòî, åñëè êàæäûé åãî ëèñò (êîíå÷íàÿ âåðøèíà, îòëè÷íàÿ îò êîðíÿ) —
çàìêíóòàÿ ñåêâåíöèÿ. Ñåêâåíöèÿ ! âûâîäèìà, èëè èìååò âûâîä, åñëè ñóùåñòâóåò çà-
ìêíóòîå ñåêâåíöèàëüíîå äåðåâî ñ êîðíåì ! . Òàêîå äåðåâî íàçûâàþò âûâîäîì ñåê-
âåíöèè ! . Ñåêâåíöèÿ X — ïðååìíèê ñåêâåíöèè % â ñåêâåíöèàëüíîì äåðåâå � ñ êîð-
íåì ! , åñëè â � ñóùåñòâóåò ïóòü ! ! ! !� 1 , , , , , ..� �n m . òàêîé, ÷òî X � !n è
% !� m . Òîãäà ñåêâåíöèþ % íàçîâåì ïðåäêîì ñåêâåíöèè X . Òàêàÿ òåðìèíîëîãèÿ
ñîîòâåòñòâóåò ïðîöåññó âûâîäà ñåêâåíöèè ! èç àêñèîì.
Áàçîâîå óñëîâèå çàìêíóòîñòè ñåêâåíöèè [8] äàåòñÿ òàêèì ñâîéñòâîì: ñåêâåí-
öèÿ � çàìêíóòà, åñëè ñóùåñòâóåò ôîðìóëà � òàêàÿ, ÷òî |
�� � è
�| � � . Çàìêíó-
òîñòü ñåêâåíöèè | |
� � îçíà÷àåò, ÷òî � �� � � , íî èç óñëîâèÿ � �� � � âûòåêàåò
� �|� . Èòàê, åñëè ñåêâåíöèÿ | |
� � çàìêíóòà, òî � �|� .
Ââåäåì äîïîëíèòåëüíîå óñëîâèå çàìêíóòîñòè ñåêâåíöèè â äàííîé âåðøèíå
ñåêâåíöèàëüíîãî äåðåâà. Ïóñòü Y — ìíîæåñòâî âñåõ íåîçíà÷åííûõ èìåí â äàííîé
âåðøèíå � . Ñåêâåíöèÿ � Y -çàìêíóòà, åñëè ñóùåñòâóåò ïàðà ôîðìóë |
�R Ax
v � è
�| R Ay
u � òàêèõ, ÷òî R Ax
v è R Ay
u èìåþò îäèíàêîâûå Y -íåîçíà÷èâàåìûå ôîðìû.
Åñëè ñåêâåíöèÿ | |
� � Y -çàìêíóòà, òî � �A Y, |
� äëÿ ïðîèçâîëüíîé A . Â ñà-
ìîì äåëå, ïðè èíòåðïðåòàöèÿõ íà äàííûõ, ãäå âñå èìåíà Y íå èìåþò çíà÷åíèÿ,
ïðåäèêàòû, êîòîðûå åñòü èíòåðïðåòàöèÿìè ôîðìóë ñ îäèíàêîâûìè Y -íåîçíà÷èâàå-
ìûìè ôîðìàìè, ïðèíèìàþò îäèíàêîâûå çíà÷åíèÿ. Îòñþäà ïîëó÷àåì: åñëè ñåêâåí-
öèÿ | |
� � Y -çàìêíóòà, òî � �A X Y, |
� äëÿ ïðîèçâîëüíûõ A è X Y X Y� � � �: .
4.2. Áàçîâûå ñåêâåíöèàëüíûå ôîðìû èñ÷èñëåíèé ëîãèê êâàçèàðíûõ ïðå-
äèêàòîâ. Óêàæåì áàçîâûå ñåêâåíöèàëüíûå ôîðìû ïðîïîçèöèîíàëüíîãî óðîâ-
íÿ (ñì. [8]):
|
|
|
,
,
;
�
�
A
A
!
!
�
�
|
|
|
,
,
;
A
A
!
!
|
| |
|
, ,
,
;
�
�
A B
A B
! !
!
�
�
|
| |
|
, ,
,
.
A B
A B
!
!
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 43
Óêàæåì ñåêâåíöèàëüíûå ôîðìû, êîòîðûå èñïîëüçóþò ðåíîìèíàöèþ:
|
|
| ,
,
( ),
( ),
RT
R A
R A
x
v
z x
z v
!
!
;
|
|
| ,
,
( ),
( ),
RT
R A
R A
x
v
z x
z v
!
!
;
|
|
|
( ),
( ( )),
RR
R A
R R A
x
v
y
w
x
v
y
w
� !
!
;
|
|
|
( ),
( ( )),
RR
R A
R R A
x
v
y
w
x
v
y
w
� !
!
;
|
|
|
( ),
( ),
�
�
�
R
R A
R A
x
v
x
v
!
!
;
�
�
�
|
|
|
( ),
( ),
R
R A
R A
x
v
x
v
!
!
;
|
|
|
( ) ( ),
( ),
�
�
�
R
R A R B
R A B
x
v
x
v
x
v
!
!
;
�
�
�
|
|
|
( ) ( ),
( ),
R
R A R B
R A B
x
v
x
v
x
v
!
!
;
|
|
| ,
,
( ),
( ),
�
!
!
N
R A
R A
u
v
z u
y v
ïðè y A��( ) ;
|
|
| ,
,
( ),
( ),
�
!
!
N
R A
R A
u
v
z u
y v
ïðè y A��( ) ;
|
|
|
( ),
( ),
�
�
�
R
yR A
R yA
x
v
x
v
!
!
ïðè y v x�{ }, ;
�
�
�
|
|
|
( ),
( ),
R
yR A
R yA
x
v
x
v
!
!
ïðè y v x�{ }, ;
|
|
|
( ),
( ),
�
�
�
R S
zR A
R yA
x
v
z
y
x
v
� !
!
;
�
�
|
|
|
( ),
( ),
R S
zR A
R yA
x
v
z
y
x
v
� !
!
.
Äëÿ ôîðì |
�R S è
�| R S óñëîâèÿ: y v x�{ }, , z òîòàëüíî ñòðîãî íåñóùåñòâåí-
íî, z nm R Ax
v� ( ( )) .
Óêàæåì ñåêâåíöèàëüíûå ôîðìû äëÿ ýëèìèíàöèè êâàíòîðîâ:
|
|
|
( ),
,
�
�
R A
xA
y
x !
!
;
�
�
�
|
| | |( ), , ( ), ,
,
R A R A xA
xA
z
x
z
x
m1
� !
!|
.
Äëÿ ôîðìû |
� èìÿ y òîòàëüíî ñòðîãî íåñóùåñòâåííî è y nm A� ( , )! ; òàêîå y
ãàðàíòèðîâàíî îçíà÷åííîå.
Äëÿ ôîðìû
�| { }z zm1 , ,� — ýòî ìíîæåñòâî îçíà÷åííûõ èìåí (âñåõ îçíà÷åí-
íûõ ïðè ïåðâîì ïðèìåíåíèè ôîðìû
�| , íîâûõ îçíà÷åííûõ ïðè åå ñëåäóþùèõ
ïðèìåíåíèÿõ) ìíîæåñòâà äîñòóïíûõ ôîðìóë ñåêâåíöèè
�| ,xA ! è åå ïðååìíèêîâ.
Äëÿ ïðîèçâîäíûõ êîìïîçèöèé �
, ,& x ìîæíî äîïîëíèòåëüíî ââåñòè ïðî-
èçâîäíûå ñåêâåíöèàëüíûå ôîðìû |
� ,
�| , |
& ,
|& , |
R ,
| R , |
R S ,
| R S , |
,
| .
Ñåêâåíöèàëüíîå èñ÷èñëåíèå ëîãèê êâàçèàðíûõ ïðåäèêàòîâ ñ ïðèâåäåííûìè
âûøå áàçîâûìè ñåêâåíöèàëüíèìè ôîðìàìè íàçîâåì QG-èñ÷èñëåíèåì.
4.3. Ïðîöåäóðà ïîñòðîåíèÿ ñåêâåíöèàëüíîãî äåðåâà. Ðàññìîòðèì ïðîöåäóðó
ïîñòðîåíèÿ ñåêâåíöèàëüíîãî äåðåâà äëÿ çàäàííîé ñåêâåíöèè � .
Äëÿ îáùåãî ñëó÷àÿ ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ ïðîöåäóðà ïîñòðîåíèÿ ñåê-
âåíöèàëüíîãî äåðåâà ñóùåñòâåííûì îáðàçîì óñëîæíÿåòñÿ ïî ñðàâíåíèþ ñî ñëó÷àåì
ëîãèêè ÝÏ [8]. Êàê óæå îòìå÷àëîñü, ýòî ñâÿçàíî ñ òåì, ÷òî çíà÷åíèå ïðåäèêàòà P d( )
ìîæåò áûòü ðàçíûì â çàâèñèìîñòè îò òîãî, âõîäèò ëè â d êîìïîíåíòà ñ íåêîòîðûì
ïðåäìåòíûì èìåíåì. Ïîýòîìó ïðè èíòåðïðåòàöèÿõ ôîðìóë íåîáõîäèìî ÿâíûì îáðà-
çîì óêàçûâàòü ìíîæåñòâà îçíà÷åííûõ è íåîçíà÷åííûõ èìåí. Òàêàÿ îñîáåííîñòü ïðî-
ÿâëÿåòñÿ ïðè ïîñòðîåíèè ÷àñòíûõ ñëó÷àåâ ôîðìóë âèäà
�| u� ñ ïîìîùüþ
�| -ôîðì:
÷àñòíûå ñëó÷àè ìîãóò èìåòü òîëüêî âèä
| )R y
u #� , ãäå èìÿ y îçíà÷åííîå.
Òàêèì îáðàçîì, ïðè ïðèìåíåíèè
�| -ôîðìû íàäî ïåðåáðàòü âñå âîçìîæíûå ñëó-
÷àè ðàñïðåäåëåíèÿ çàäåéñòâîâàííûõ ïðåäìåòíûõ èìåí íà îçíà÷åííûå è íåîçíà÷åííûå.
44 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
Ýòî ìîæíî ðåàëèçîâàòü ñ ïîìîùüþ ïîñòðîåíèÿ ñîîòâåòñòâóþùèõ ðàçâåòâëåíèé ñåê-
âåíöèàëüíîãî äåðåâà. Íåôîðìàëüíî ãîâîðÿ, åñëè â âåðøèíå � ê ôîðìóëå âèäà
�| u�
ïðèìåíÿåòñÿ
�| -ôîðìà, òî äëÿ � ñòðîèòñÿ íå îäíà, à ìíîãî âåðøèí-«ñåñòåð», êîòîðûå
ÿâëÿþòñÿ íåïîñðåäñòâåííûìè ïðåäêàìè � , èìåþò îäíî è òî æå ìíîæåñòâî çàäåéñòâî-
âàííûõ èìåí è îòëè÷àþòñÿ ëèøü ðàçíûìè ìíîæåñòâàìè îçíà÷åííûõ èìåí è ñîîòâå-
òñòâóþùèìè ìíîæåñòâàìè ÷àñòíûõ ñëó÷àåâ âèäà
| )R y
u #� .
Ïðîöåäóðà ïîñòðîåíèÿ äåðåâà äëÿ ñåêâåíöèè ! íà÷èíàåòñÿ èç êîðíÿ äåðåâà. Òà-
êóþ ïðîöåäóðó ðàçîáüåì íà ýòàïû. Êàæäîå ïðèìåíåíèå ñåêâåíöèàëüíîé ôîðìû
ïðîâîäèòñÿ ê êîíå÷íîìó ìíîæåñòâó äîñòóïíûõ íà äàííûé ìîìåíò ôîðìóë.
 íà÷àëå êàæäîãî ýòàïà âûïîëíÿåòñÿ øàã äîñòóïà: ê ñïèñêó äîñòóïíûõ ôîðìóë
ïðèáàâëÿåì ïî îäíîé ôîðìóëå ñî ñïèñêà |
-ôîðìóë è ñïèñêà
|-ôîðìóë. Åñëè íåäîñ-
òóïíûõ |
-ôîðìóë èëè
|-ôîðìóë íåò (ñîîòâåòñòâóþùèé ñïèñîê èñ÷åðïàí), òî íà
äàëüíåéøèõ øàãàõ äîñòóïà ïðèáàâëÿåì ïî îäíîé ôîðìóëå íåèñ÷åðïàííîãî ñïèñêà.
 íà÷àëå ïîñòðîåíèÿ äåðåâà äîñòóïíà ëèøü ïàðà ïåðâûõ ôîðìóë ñïèñêîâ (åäè-
íñòâåííàÿ |
-ôîðìóëà èëè
|-ôîðìóëà, åñëè îäèí èç ñïèñêîâ ïóñòîé).
 íà÷àëå ïîñòðîåíèÿ ñåêâåíöèàëüíîãî äåðåâà äëÿ ñåêâåíöèè ! çàôèêñèðóåì
íåêîòîðûé ñïèñîê TN (áåñêîíå÷íûé) òîòàëüíî ñòðîãî íåñóùåñòâåííûõ èìåí («íî-
âûõ» èìåí) òàêîé, ÷òî èìåíà èç TN íå âñòðå÷àþòñÿ â ôîðìóëàõ ñåêâåíöèè ! .
Ñ êàæäîé âåðøèíîé äåðåâà ñâÿçûâàåì ìíîæåñòâî çàäåéñòâîâàííûõ è ìíîæå-
ñòâî îçíà÷åííûõ ïðåäìåòíûõ èìåí. Ìíîæåñòâî îçíà÷åííûõ èìåí ÿâíûì îáðàçîì
âûäåëÿåòñÿ ëèøü íà ïóòÿõ, ãäå õîòÿ áû ðàç ïðèìåíÿëèñü
�| -ôîðìû (äî òàêîãî ïðè-
ìåíåíèÿ ÿâíîå âûäåëåíèå ìíîæåñòâà îçíà÷åííûõ èìåí íå íóæíî). Ìíîæåñòâî çà-
äåéñòâîâàííûõ èìåí — ýòî ìíîæåñòâî èìåí âñåõ äîñòóïíûõ â äàííîé âåðøèíå
ôîðìóë. Âñå òîòàëüíî ñòðîãî íåñóùåñòâåííûå èìåíà, ôèãóðèðóþùèå ïðè ïðèìåíå-
íèè |
�-ôîðì, â äàííîì âûâîäå ãàðàíòèðîâàíî îçíà÷åííûå.
Ïóñòü âûïîëíåíî k ýòàïîâ ïðîöåäóðû. Íà ýòàïå k & 1ïðîâåðÿåì, áóäåò ëè êàæ-
äûé èç ëèñòüåâ äåðåâà çàìêíóòîé ñåêâåíöèåé. Åñëè âñå ëèñòüÿ çàìêíóòûå, òî ïðîöå-
äóðà çàâåðøåíà ïîëîæèòåëüíî, ïîëó÷åíî çàìêíóòîå ñåêâåíöèàëüíîå äåðåâî. Åñëè
íåò, òî äëÿ êàæäîãî íåçàìêíóòîãî ëèñòà � äåëàåì ñëåäóþùèé øàã äîñòóïà, çàòåì
äîñòðàèâàåì êîíå÷íîå ïîääåðåâî ñ âåðøèíîé � ñëåäóþùèì îáðàçîì:
1) àêòèâèçèðóåì âñå äîñòóïíûå íåïðèìèòèâíûå ôîðìóëû � ;
2) ïîî÷åðåäíî ê êàæäîé àêòèâíîé ôîðìóëå ïðèìåíÿåì ñîîòâåòñòâóþùóþ ñåê-
âåíöèàëüíóþ ôîðìó.
Ñåêâåíöèàëüíûå ôîðìû |
RT è
| RT âñïîìîãàòåëüíûå: ïåðåä ïðèìåíåíèåì îä-
íîé èç ôîðì òèïà �N RR R R R R S, , , , ,� � � � óäàëÿåì, â ñëó÷àå íàëè÷èÿ, òîæäåñ-
òâåííûå ïåðåèìåíîâàíèÿ, ïðèìåíÿÿ íàäëåæàùåå êîëè÷åñòâî ðàç |
RT èëè
| RT .
Ñíà÷àëà âûïîëíÿåì âñå |
�-ôîðìû. Ïðèìåíåíèå |
�-ôîðìû ïðèáàâëÿåò íîâîå
òîòàëüíî ñòðîãî íåñóùåñòâåííîå èìÿ y ê ìíîæåñòâó îçíà÷åííûõ èìåí âåðøèíû, òà-
êîå y áåðåì êàê ïåðâîå íåâñòðå÷åííîå íà äàííîì ïóòè îò êîðíÿ èìÿ ñî ñïèñêà TN .
Èìÿ y ïðèáàâëÿåì ê ìíîæåñòâàì çàäåéñòâîâàííûõ è îçíà÷åííûõ èìåí, äàëüøå äëÿ
êàæäîé äîñòóïíîé ôîðìóëû âèäà
�| u� ïðèáàâëÿåì åå ÷àñòíûé ñëó÷àé
| )R y
u #� .
Òàêîå èìÿ y ãàðàíòèðîâàíî îçíà÷åííîå. Çàòåì âûïîëíÿåì R S� -ôîðìû, ïðè ýòîì áå-
ðåì z nm R xx
v� �( ( ))� èç âñòðå÷àâøèõñÿ íà äàííîì ïóòè îò êîðíÿ èìåí ñïèñêà TN ,
åñëè òàêèå åñòü, èíà÷å áåðåì z êàê ïåðâîå èìÿ ñïèñêà TN .  ïîñëåäíåì ñëó÷àå z
ïðèáàâëÿåì ê ìíîæåñòâàì çàäåéñòâîâàííûõ è îçíà÷åííûõ èìåí, äàëüøå äëÿ êàæ-
äîé äîñòóïíîé ôîðìóëû âèäà
�| u� ïðèáàâëÿåì åå ÷àñòíûé ñëó÷àé
| ( )R z
u � . Çà-
òåì ê êàæäîé èç îñòàâøèõñÿ àêòèâíûõ ôîðìóë ïðèìåíÿåì ñîîòâåòñòâóþùóþ ôîð-
ìó — îäíó èç |
� ,
�| , |
� ,
�| , |
�N ,
| �N , |
RR ,
| RR , |
�R ,
�| R ,
| |,
� �R R , |
�R ,
�| R .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 45
Çàòåì ïðèìåíÿåì
�| -ôîðìû. Òàêîå ïðèìåíåíèå âûïîëíÿåì ñëåäóþùèì
îáðàçîì.
Åñëè
�| -ôîðìà âïåðâûå ïðèìåíÿåòñÿ íà ïóòè îò êîðíÿ äåðåâà, òî èç äàííîé
âåðøèíû ñòðîèì ðàçâåòâëåíèå äåðåâà. Äëÿ êàæäîé âåðøèíû, ÷òî ÿâëÿåòñÿ íå-
ïîñðåäñòâåííûì ïðåäêîì äàííîé, çàäàåì ìíîæåñòâî îçíà÷åííûõ èìåí êàê îïðåäå-
ëåííîå ïîäìíîæåñòâî çàäåéñòâîâàííûõ, ïðè ýòîì â íåå äîëæíû âõîäèòü âñå òî-
òàëüíî ñòðîãî íåñóùåñòâåííûå èìåíà, ôèãóðèðóþùèå â ïðåäûäóùèõ ïðèìåíåíèÿõ
|
�-ôîðì íà ïóòè îò êîðíÿ ê äàííîé âåðøèíå.
Ïóñòü â äàííîé âåðøèíå ! ñ ìíîæåñòâîì çàäåéñòâîâàííûõ èìåí Z
�| -ôîðìà
ïðèìåíÿåòñÿ âïåðâûå íà ïóòè îò êîðíÿ ê !. Ýòî îçíà÷àåò, ÷òî íà ýòîì ïóòè åùå íå
áûëî ÿâíîãî âûäåëåíèÿ ìíîæåñòâ îçíà÷åííûõ è íåîçíà÷åííûõ èìåí, êðîìå, âîç-
ìîæíî, âûäåëåíèÿ ãàðàíòèðîâàíî îçíà÷åííûõ ïðè ïðåäûäóùèõ ïðèìåíåíèÿõ
|
�-ôîðì. Ïóñòü G — ìíîæåñòâî ãàðàíòèðîâàíî îçíà÷åííûõ èìåí, ôèãóðèðóþùèõ
ïðè ïðèìåíåíèÿõ |
�-ôîðì íà ïóòè îò êîðíÿ ê äàííîé âåðøèíå ! , ïóñòü
�| x� —
òà ñïåöèôèöèðîâàííàÿ ôîðìóëà, ê êîòîðîé ïðèìåíÿåòñÿ
�| -ôîðìà. Äîñòðàèâàåì
íåïîñðåäñòâåííûõ ïðåäêîâ ! äëÿ êàæäîãî X Z G� \ , òîãäà X G è Z X G\ ( ) —
ýòî ìíîæåñòâà îçíà÷åííûõ è íåîçíà÷åííûõ èìåí ñîîòâåòñòâóþùåé âåðøèíû-ïðåä-
êà.  êàæäîé òàêîé âåðøèíå-ïðåäêå ïðèáàâëÿåì ÷àñòíûé ñëó÷àé
| ( )R z
x � ôîðìóëû
�| x� äëÿ êàæäîãî z X G� , â äàëüíåéøåì âî âñåõ ïóòÿõ èç ýòîé âåðøèíû-ïðåäêà
èìåíà èç X G îçíà÷åííûå.
Ïóñòü â âåðøèíå ! ñ ìíîæåñòâàìè çàäåéñòâîâàííûõ èìåí Z è îçíà÷åííûõ èìåí
W ê
�| x� âïåðâûå ïðèìåíÿåòñÿ
�| -ôîðìà, íî ïðèìåíåíèÿ
�| -ôîðì íà ïóòè îò
êîðíÿ ê âåðøèíå ! óæå áûëè, ïîýòîìó äëÿ ! ìíîæåñòâà îçíà÷åííûõ è íåîçíà÷åí-
íûõ èìåí óæå âûäåëåíû. Òîãäà äëÿ êàæäîãî z W� ïðèáàâëÿåì ÷àñòíûé ñëó÷àé
| )R z
x#� .
Ðàñøèðåíèå ìíîæåñòâà çàäåéñòâîâàííûõ èìåí ïðè ïîÿâëåíèè íîâûõ äîñòóï-
íûõ ôîðìóë ïîñëå âûïîëíåíèÿ øàãà äîñòóïà âåäåò ê ïîâòîðíîìó ïðèìåíåíèþ
�| -ôîðì ê ñòàðûì äîñòóïíûì ôîðìóëàì âèäà
�| x�. Ïóñòü X — ìíîæåñòâî äî-
áàâëåííûõ íîâûõ èìåí ïîñëå âûïîëíåíèÿ øàãà äîñòóïà â âåðøèíå ñ ìíîæåñòâàìè
çàäåéñòâîâàííûõ èìåí Z è îçíà÷åííûõ èìåí W . Ïîâòîðíîå ïðèìåíåíèå
�| -ôîðìû
ê
�| x� äàåò ðàçâåòâëåíèå äëÿ êàæäîé Y X� , â êàæäîé òàêîé âåðøèíå-ïðåäêå
ïðèáàâëÿåì
| ( )R z
x � äëÿ êàæäîãî z Y� , ïðè ýòîì ìíîæåñòâîì çàäåéñòâîâàííûõ
èìåí âåðøèíû-ïðåäêà áóäåò Z X , ìíîæåñòâîì îçíà÷åííûõ èìåí áóäåò W Y .
Âñå ïîâòîðû ôîðìóë â ñåêâåíöèè óäàëÿåì. Ïîñëå âûïîëíåíèÿ íåâñïîìîãàòåëü-
íîé ñåêâåíöèàëüíîé ôîðìû ôîðìóëà ïàññèâíàÿ. Ê ïàññèâíûì è îáðàçîâàííûì íà
äàííîì ýòàïå ôîðìóëàì ñåêâåíöèàëüíûå ôîðìû íå ïðèìåíÿþòñÿ.
Ïðè ïîñòðîåíèè ñåêâåíöèàëüíîãî äåðåâà âîçìîæíû òàêèå ñëó÷àè:
1) ïðîöåäóðà çàâåðøåíà ïîëîæèòåëüíî, èìååì êîíå÷íîå çàìêíóòîå äåðåâî;
2) ïðîöåäóðà çàâåðøåíà îòðèöàòåëüíî, èìååì êîíå÷íîå íåçàìêíóòîå äåðåâî;
3) ïðîöåäóðà íå çàâåðøàåòñÿ, èìååì áåñêîíå÷íîå ñåêâåíöèàëüíå äåðåâî.
 ñèëó ëåììû Êåíèãà [5] òàêîå äåðåâî èìååò õîòÿ áû îäèí áåñêîíå÷íûé ïóòü ' .
Âåðøèíû ïóòè ' íå ìîãóò áûòü çàìêíóòûìè ñåêâåíöèÿìè, âåäü ïðè ïîÿâëåíèè çà-
ìêíóòîé ñåêâåíöèè ïðîöåññ ïîñòðîåíèÿ äëÿ ýòîãî ïóòè îáðûâàåòñÿ. Êàæäàÿ èç ôîð-
ìóë ñåêâåíöèè ! âñòðåòèòñÿ íà ïóòè ' è ñòàíåò äîñòóïíîé.
Èòàê, â ñëó÷àÿõ 2) è 3) â äåðåâå ñóùåñòâóåò êîíå÷íûé èëè áåñêîíå÷íûé ïóòü, âñå
âåðøèíû êîòîðîãî — íåçàìêíóòûå ñåêâåíöèè. Òàêîé ïóòü íàçîâåì íåçàìêíóòûì.
4.4. Êîððåêòíîñòü è ïîëíîòà QG-èñ÷èñëåíèé. Ïóñòü äëÿ ñåêâåíöèè | |
� �
ïîñòðîåíî çàìêíóòîå äåðåâî. Èç ïðèâåäåííîé âûøå ïðîöåäóðû ïîñòðîåíèÿ ñåêâåí-
öèàëüíîãî äåðåâà âûòåêàåò, ÷òî äëÿ êàæäîé åãî âåðøèíû | |
" ( ñ ìíîæåñòâàìè
46 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
îçíà÷åííûõ èìåí W è íåîçíà÷åííûõ èìåí U äëÿ êàæäîé ìîäåëè ÿçûêà A âûïîëíÿ-
åòñÿ " (A , |W U
� . Óòâåðæäåíèå î÷åâèäíî äëÿ âñåõ ôîðì, êðîìå |
� è
�| . Äëÿ
|
�-ôîðì ýòî âûòåêàåò èç ñëåäñòâèÿ 2, äëÿ
�| -ôîðì — èç òåîðåìû 3 è ñëåäñòâèÿ 1.
Ââåäåííûå |
�-ôîðìàìè íîâûå òîòàëüíî ñòðîãî íåñóùåñòâåííûå èìåíà ãàðàíòèðî-
âàíî îçíà÷åííûå â äàííîì âûâîäå ñåêâåíöèè | |
� � , ïîýòîìó ðàññìàòðèâàåì òîëü-
êî ìîäåëè ÿçûêà A èç G-îçíà÷åííûìè äàííûìè, ãäå G — ìíîæåñòâî òàêèõ ãàðàíòèðî-
âàíî îçíà÷åííûõ èìåí. Íåôîðìàëüíî ãîâîðÿ, ãàðàíòèðîâàíî îçíà÷åííûå èìåíà âåäóò
ñåáÿ ïîäîáíî êîíñòàíòíûì ñèìâîëàì êëàññè÷åñêîé ëîãèêè ïðåäèêàòîâ. Èòàê, � �|� �
äëÿ êàæäîé A èìååì � �A G, |� , ãäå G — ìíîæåñòâî ãàðàíòèðîâàíî îçíà÷åííûõ èìåí.
Òàêèì îáðàçîì, äëÿ ïîñòðîåííîãî QG-èñ÷èñëåíèÿ âûïîëíÿåòñÿ ñëåäóþùàÿ
òåîðåìà.
Òåîðåìà 7 (êîððåêòíîñòè). Ïóñòü ñåêâåíöèÿ | |
� � âûâîäèìà. Òîãäà � �|� .
Äëÿ äîêàçàòåëüñòâà ïîëíîòû QG-èñ÷èñëåíèé áóäåì îïèðàòüñÿ íà èçâåñòíûé
(ñì., íàïðèìåð, [15, 8]) ìåòîä ìîäåëüíûõ ìíîæåñòâ.
Ïóñòü Í — ìíîæåñòâî ñïåöèôèöèðîâàííûõ ôîðìóë ñ âûäåëåííûì ìíîæå-
ñòâîì W nm� ( )Í îçíà÷åííûõ èìåí; òîãäàU nm W� ( ) \Í — ìíîæåñòâî åãî íåîçíà-
÷åííûõ èìåí.
Ìíîæåñòâî H ìîäåëüíî, åñëè âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ.
ÍÑ) Íå ñóùåñòâóåò ôîðìóëû � òàêîé, ÷òî |
�� H è
�| � H.
ÍU) Íå ñóùåñòâóåò ïàðû ôîðìóë âèäà |
�R Ax
v
H è
�| R Ay
u
H òàêèõ, ÷òî
R Ax
v è R Ay
u èìåþò îäèíàêîâûå U-íåîçíà÷èâàåìûå ôîðìû.
Í�) Åñëè |
� �� H , òî
�| � H;
åñëè
� �| � H , òî |
�� H.
Í�) Åñëè |
� �� � H , òî |
�� H èëè |
�� H;
åñëè
� �| � � H, òî
�| � H è
�|� H.
ÍRT) Åñëè | ,
, ( )
�R
z x
z v � H , òî | ( )
�Rx
v � H;
åñëè
�| ,
, ( )R
z x
z v � H , òî
�| ( )Rx
v � H.
ÍRR) Åñëè | ( ( ))
�R Rx
v
y
w � H , òî | ( )
�Rx
v
y
w
� � H;
åñëè
�| ( ( ))R Rx
v
y
w � H , òî
�| ( )Rx
v
y
w
� � H.
ÍR�) Åñëè | ( )
� �Rx
v � H, òî | ( )
� �Rx
v � H;
åñëè
� �| ( )Rx
v � H , òî
� �| ( )Rx
v � H.
ÍR�) Åñëè | ( )
� �Rx
v � � H , òî | ( ) ( )
� �R Rx
v
x
v� � H;
åñëè
� �| ( )Rx
v � � H , òî
� �| ( ) ( )R Rx
v
x
v� � H.
Í�N) Åñëè | ,
, ( )
�R
z x
y v � H è y ��( )� , òî | ( )
�Rx
v � H;
åñëè
�| ,
, ( )R
z x
y v � H è y ��( )� , òî
�| ( )Rx
v � H.
ÍR�) Åñëè | ( )
� �R yx
v � H è y v x�{ }, , òî | ( )
� �yRx
v � H;
åñëè
� �| ( )R yx
v � H è y v x�{ }, , òî
� �| ( )yRx
v � H.
ÍR�S) Åñëè | ( )
� �R yx
v � H è y v x�{ }, , òî | ( )
� �z Rx
v
z
y
� � H;
åñëè
� �| ( )R yx
v � H è y v x�{ }, , òî
� �| ( )z Rx
v
z
y
� � H.
Çäåñü z ñòðîãî òîòàëüíî íåñóùåñòâåííîå è z nm R yx
v� �( ( ))� .
Í�) Åñëè |
� �x� H , òî ñóùåñòâóåò y W� òàêîå, ÷òî | ( )
�R y
x � H ;
åñëè
� �| x� H , òî äëÿ âñåõ y W� èìååì
�| ( )R y
x � H.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 47
Òåîðåìà 8. Ïóñòü '— íåçàìêíóòûé ïóòü â ñåêâåíöèàëüíîì äåðåâå, H — ìíî-
æåñòâî âñåõ åãî ñïåöèôèöèðîâàííûõ ôîðìóë. Òîãäà ñóùåñòâóþò ÀÑ
A I� ( , )A è � � VA òàêèå, ÷òî:
• èç óñëîâèÿ |
�� H âûòåêàåò � �T ( )�A ;
• èç óñëîâèÿ
�| � H âûòåêàåò � �F( )�A .
Ïóñòü'— íåçàìêíóòûé ïóòü â ñåêâåíöèàëüíîì äåðåâå. Òîãäà H — ìîäåëüíîå
ìíîæåñòâî. Â ñàìîì äåëå, äëÿ ïåðåõîäà îò íèçøåé âåðøèíû ïóòè ê âûñøåé èñïîëü-
çóåòñÿ îäíà èç áàçîâûõ ñåêâåíöèàëüíûõ ôîðì. Ïåðåõîäû, âûïîëíåííûå ñîãëàñíî
òàêèì ôîðìàì, â òî÷íîñòè îòâå÷àþò ïóíêòàì îïðåäåëåíèÿ ìîäåëüíîãî ìíîæåñòâà.
Êàæäàÿ íåïðèìèòèâíàÿ ôîðìóëà [8], êîòîðàÿ âñòðå÷àåòñÿ íà ïóòè ' , áóäåò ðàçëî-
æåíà èëè óïðîùåíà ñîãëàñíî ñîîòâåòñòâóþùåé ñåêâåíöèàëüíîé ôîðìå. Âñå ñåêâåí-
öèè ïóòè ' íåçàìêíóòûå, ïîýòîìó âûïîëíÿþòñÿ ñîîòâåòñòâóþùèå óñëîâèÿ êîððåê-
òíîñòè ìîäåëüíîãî ìíîæåñòâà.
Ïóñòü W — ìíîæåñòâî âñåõ îçíà÷åííûõ ïðåäìåòíûõ èìåí, êîòîðûå ôèãóðèðó-
þò â H. Âîçüìåì íåêîòîðîå ìíîæåñòâî A òàêîå, ÷òî | | | |A W= , è íåêîòîðóþ èíúåê-
òèâíóþ � � VA ñ im W( )� � . Òàêàÿ A äóáëèðóåò ìíîæåñòâî W.
Äîêàçàòåëüñòâî ïðîâåäåì èíäóêöèåé ïî ñëîæíîñòè ôîðìóëû ñîãëàñíî ïîñòðî-
åíèþ ìîäåëüíîãî ìíîæåñòâà.
Ñíà÷àëà çàäàäèì çíà÷åíèå áàçîâûõ ïðåäèêàòîâ íà � è íà ÈÌ âèäà r x
v ( )� .
Åñëè |
�p H , òî ïîëîæèì � �T ( )pA ; åñëè
�| p H, òî ïîëîæèì � �F( )pA .
Åñëè | ( )
�R px
v
H, òî ïîëîæèì r px
v
A( ) ( )� �T ; åñëè
�| ( )R px
v
H , òî ïîëî-
æèì r px
v
A( ) ( )� �F .
Çàäàííûå òàêèì îáðàçîì çíà÷åíèÿ áàçîâûõ ïðåäèêàòîâ ïðîäîëæèì, ó÷èòûâàÿ
óñëîâèÿ ñòðîãî íåñóùåñòâåííîñòè èìåí, íà ñîîòâåòñòâóþùèå h AV� . Âî âñåõ äðó-
ãèõ ñëó÷àÿõ d AV� çíà÷åíèå p dA ( ) ìîæíî çàäàâàòü ïðîèçâîëüíî, ó÷èòûâàÿ åñòåñò-
âåííîå îãðàíè÷åíèå îòíîñèòåëüíî ñòðîãî íåñóùåñòâåííîñòè: äëÿ âñåõ d , h AV� òà-
êèõ, ÷òî d p h p|| ( ) || ( )
�
� � , íåîáõîäèìî p d p hA A( ) ( )� . Òàêèì îáðàçîì, çíà÷å-
íèå áàçîâûõ ïðåäèêàòîâ çàäàíû îäíîçíà÷íî, ïðè÷åì ó÷òåíî, ÷òî èìåíà y p��( )
ñòðîãî íåñóùåñòâåííûå äëÿ p .
Äëÿ àòîìàðíûõ ôîðìóë è ôîðìóë âèäà R px
v ( ) óòâåðæäåíèÿ 1) è 2) òåîðåìû
âûòåêàþò ñ ïðèâåäåííîãî âûøå îïðåäåëåíèÿ çíà÷åíèé áàçîâûõ ïðåäèêàòîâ.
Äîêàæåì øàã èíäóêöèè äëÿ óòâåðæäåíèé 1) è 2).
Ïóñòü |
� �� H. Ñîãëàñíî Í� èìååì
�| � H. Ïî ïðåäïîëîæåíèþ èíäóêöèè
� �F( )�A , îòêóäà � � �T ( )�A .
Ïóñòü
� �| � H . Ñîãëàñíî Í� èìååì |
�� H . Ïî ïðåäïîëîæåíèþ èíäóêöèè
� �T ( )�A , îòêóäà � � �F( )�A .
Ïóñòü |
� �� � H. Ñîãëàñíî Í� èìååì |
�� H èëè |
�� H. Ïî ïðåäïîëîæå-
íèþ èíäóêöèè � �T ( )�A èëè � �T ( )�A , îòêóäà � � �T T( ) ( )� �A A
� �T ( )� �A .
Ïóñòü
� �| � � H. Ñîãëàñíî Í� èìååì
�| � H è
�|� H . Ïî ïðåäïîëîæå-
íèþ èíäóêöèè � �F( )�A è � �F( )�A , îòêóäà � � � �F F( ) ( )� �A A F( )� �� A .
Ïóñòü | ,
, ( )
�R
z x
z v � H. Ñîãëàñíî ÍRT èìååì | ( )
�Rx
v � H. Ïî ïðåäïîëîæåíèþ
èíäóêöèè � �T ( ( ) )Rx
v
A� , îòêóäà � �T ( ( ) )
,
,
R
z x
z v
A� .
Ïóñòü
�| ,
, ( )R
z x
z v � H. Ñîãëàñíî ÍRT èìååì
�| ( )Rx
v � H. Ïî ïðåäïîëîæåíèþ
èíäóêöèè � �F( ( ) )Rx
v
A� , îòêóäà � �F( ( ) )
,
,
R
z x
z v
A� .
48 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
Ïóñòü | ( ( ))
�R Rx
v
y
w � H. Ñîãëàñíî ÍRR èìååì | ( )
�Rx
v
y
w
� � H. Ïî ïðåäïî-
ëîæåíèþ èíäóêöèè � �T ( ( ) )Rx
v
y
w
A� � , îòêóäà � �T ( ( ( )) )R Rx
v
y
w
A� . Ïóñòü
�| ( ( ))R Rx
v
y
w � H . Ñîãëàñíî ÍRR èìååì
�| ( )Rx
v
y
w
� � H. Ïî ïðåäïîëîæåíèþ
èíäóêöèè � �F( ( ) )Rx
v
y
w
A� � , îòêóäà � �F( ( ( )) )R Rx
v
y
w
A� .
Ïóñòü | ( )
� �Rx
v � H. Ñîãëàñíî ÍR� èìååì | ( )
� �Rx
v � H. Ïî ïðåäïîëîæå-
íèþ èíäóêöèè � � �T ( ( ) )Rx
v
A� , îòêóäà � � �T ( ( ) )Rx
v
A� .
Ïóñòü
� �| ( )Rx
v � H. Ñîãëàñíî ÍR� èìååì
� �| ( )Rx
v � H. Ïî ïðåäïîëîæå-
íèþ èíäóêöèè � � �F( ( ) )Rx
v
A� , îòêóäà � � �F( ( ) )Rx
v
A� .
Ïóñòü | ( )
� �Rx
v � � H. Ñîãëàñíî ÍR� èìååì | ( ) ( )
� �R Rx
v
x
v� � H .
Ïî ïðåäïîëîæåíèþ èíäóêöèè � � �T ( ( ) ( ) )R Rx
v
x
v
A� � , îòêóäà � � �T ( ( ) )Rx
v
A� � .
Ïóñòü
� �| ( )Rx
v � � H. Ñîãëàñíî ÍR� èìååì | ( ) ( )
� ) �Rx
v
x
v� � H. Ïî ïðåä-
ïîëîæåíèþ èíäóêöèè � � �F( ( ) ( ) )R Rx
v
x
v
A� � , îòêóäà � � �F( ( ) )Rx
v
A� � .
Ïóñòü | ,
, ( )
�R
z x
y v � H è y ��( )� . Ñîãëàñíî Í�N èìååì | ( )
�Rx
v � H.
Ïî ïðåäïîëîæåíèþ èíäóêöèè � �T ( ( ) )Rx
v
A� , îòêóäà � �T ( ( ) )
,
,
R
z x
y v
A� .
Ïóñòü
�| ,
, ( )R
z x
y v � H è y ��( )� . Ñîãëàñíî Í�N èìååì
�| ( )Rx
v � H.
Ïî ïðåäïîëîæåíèþ èíäóêöèè � �F( ( ) )Rx
v
A� , îòêóäà � �F( ( ) )
,
,
R
z x
y v
A� .
Ïóñòü | ( )
� �R yx
v � H è y v x�{ }, . Ñîãëàñíî ÍR� èìååì | ( )
� �yRx
v � H.
Ïî ïðåäïîëîæåíèþ èíäóêöèè � � �T ( ( ) )y Rx
v
A� , îòêóäà � � �T ( ( ) )R yx
v
A� .
Ïóñòü
� �| ( )R yx
v � H è y v x�{ }, . Ñîãëàñíî ÍR� èìååì
� �| ( )yRx
v � H.
Ïî ïðåäïîëîæåíèþ èíäóêöèè � � �F( ( ) )y Rx
v
A� , îòêóäà � � �F( ( ) )R yx
v
A� .
Ïóñòü | ( )
� �R yx
v � H è y v x�{ }, . Ñîãëàñíî ÍR�S èìååì | ( )
� �z Rx
v
z
y
� � H
äëÿ íåêîòîðîãî ñòðîãî òîòàëüíî íåñóùåñòâåííîãî z nm R yx
v� �( ( ))� . Ïî ïðåäïîëî-
æåíèþ èíäóêöèè èìååì � � �T ( ( ) )z Rx
v
z
y
A� � , îòêóäà � � �T ( ( ) )R yx
v
A� .
Ïóñòü
� �| ( )R yx
v � H è y v x�{ }, . Ñîãëàñíî ÍR�S èìååì
�| ( )z Rx
v
z
y
� � H
äëÿ íåêîòîðîãî ñòðîãî òîòàëüíî íåñóùåñòâåííîãî z nm R yx
v� �( ( ))� . Ïî ïðåäïîëî-
æåíèþ èíäóêöèè èìååì � � �F( ( ) )z Rx
v
z
y
A� � , îòêóäà � � �F( ( ) )R yx
v
A� .
Ïóñòü |
� �x� H. Ñîãëàñíî Í� ñóùåñòâóåò y W� òàêîå, ÷òî | ( )
�R y
x � H.
Ïî ïðåäïîëîæåíèþ èíäóêöèè � �T ( ( ) )R y
x
A� . Îòñþäà � �� �x y A� ( ) ( )T � .
Îäíàêî �( )y � ñîãëàñíî y W� , ïîýòîìó äëÿ a y� �( ) èìååì �� �x a A� T ( )� , îò-
êóäà � � �T ( )x A� .
Ïóñòü
� �| x� H. Ñîãëàñíî Í� äëÿ âñåõ y W� èìååì
�| ( )R y
x � H. Ïî ïðåäïî-
ëîæåíèþ èíäóêöèè � �F( ( ) )R y
x
A� äëÿ âñåõ y W� . Îòñþäà � �� �x y A� ( ) ( )T �
äëÿ âñåõ y W� . Ñîãëàñíî � � WA èìååì �( )y � äëÿ âñåõ y W� . Ïîñêîëüêó � — áè-
åêöèÿ W A� , òî êàæäîå b A� èìååò âèä b y� �( ) äëÿ íåêîòîðîãî y W� . Èòàê,
�� �x b A� F( )� , îòêóäà � � �F( )x A� .
Òåîðåìà 9 (ïîëíîòû). Ïóñòü � �|� . Òîãäà ñåêâåíöèÿ | |
� � âûâîäèìà.
Äëÿ äîêàçàòåëüñòâà ïðåäïîëîæèì ïðîòèâíîå: � �|� è ñåêâåíöèÿ | |
� � íåâû-
âîäèìà. Åñëè ! � ��
| | íåâûâîäèìà, òî â ñåêâåíöèàëüíîì äåðåâå äëÿ ! ñóùåñòâó-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6 49
åò íåçàìêíóòûé ïóòü. Ìíîæåñòâî H âñåõ ñïåöèôèöèðîâàííûõ ôîðìóë ñåêâåíöèé
ýòîãî ïóòè ìîäåëüíîå. Çàìåòèì, ÷òî | |
�� � H . Ñîãëàñíî òåîðåìå 8 ñóùåñòâóþò
ÀÑ A I� ( , )A è � � V A òàêèå: | ( )
� � �� �H T� A è
� � �| ( )� �H F� A . Ñîã-
ëàñíî | |
�� � H äëÿ âñåõ � �� èìååì � �T A( )� , äëÿ âñåõ � �� èìååì
� �F( )�A . Îòñþäà � � �T F( ) ( )� � , îòêóäà T F( ) ( )� �� � � . Ýòî ïðîòèâîðå÷èò
� �|� .
ÇÀÊËÞ×ÅÍÈÅ
 íàñòîÿùåé ðàáîòå èññëåäóþòñÿ ñåìàíòèêî-ñèíòàêñè÷åñêèå ñâîéñòâà êîìïîçè-
öèîííî-íîìèíàòèâíûõ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ. Òàêèå ëîãèêè ñòðîÿòñÿ
â ñåìàíòèêî-ñèíòàêñè÷åñêîì ñòèëå íà îñíîâå êîìïîçèöèîííî-íîìèíàòèâíîãî
ïîäõîäà. Ðàññìîòðåí ñïåêòð êîìïîçèöèîííî-íîìèíàòèâíûõ ëîãèê, îïèñàíû âàæ-
íûå êëàññû ïåðâîïîðÿäêîâûõ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ — ëîãèêè ïîëíîòî-
òàëüíûõ ýêâèòîííûõ, ýêâèòîííûõ, ýêâèñîâìåñòíûõ è ëîêàëüíî-ýêâèñîâìåñòíûõ
ïðåäèêàòîâ. Äëÿ îáùåãî ñëó÷àÿ ëîãèê êâàçèàðíûõ ïðåäèêàòîâ êâàíòîðíîãî óðîâíÿ
ïîñòðîåíî èñ÷èñëåíèå ñåêâåíöèàëüíîãî òèïà, äîêàçàíû åãî êîððåêòíîñòü è ïîëíîòà.
Êîìïîçèöèîííî-íîìèíàòèâíûå ëîãèêè êâàçèàðíûõ ïðåäèêàòîâ íàèáîëåå áëèç-
êè ê êëàññè÷åñêèì, îíè ñîõðàíÿþò îñíîâíûå ñâîéñòâà êëàññè÷åñêèõ ëîãèê ïðè ñó-
ùåñòâåííîì ðàñøèðåíèè êëàññà ñåìàíòè÷åñêèõ ìîäåëåé. Òàêèå ëîãèêè, ñ îäíîé
ñòîðîíû, ïîçâîëÿþò èñïîëüçîâàòü êàê òåîðåòè÷åñêèå ðåçóëüòàòû, òàê è áîãàòûé
îïûò ïðèìåíåíèÿ êëàññè÷åñêîé ëîãèêè, à ñ äðóãîé ñòîðîíû, îíè áîëüøå àäàïòèðî-
âàíû ê ïîòðåáíîñòÿì ïðîãðàììèðîâàíèÿ.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. Ê à ï è ò î í î â à Þ .  . , Ë å ò è ÷ å â ñ ê è é À . À . Ìàòåìàòè÷åñêàÿ òåîðèÿ ïðîåêòèðîâàíèÿ âû÷èñ-
ëèòåëüíûõ ñèñòåì. — Ì.: Íàóêà, 1988. — 295 ñ.
2. Ê à ï ³ ò î í î â à Þ .  . , Ë å ò è ÷ å â ñ ü ê è é Î . À . Äîâåäåííÿ òåîðåì â ìàòåìàòè÷íîìó ³íôîðìàö³é-
íîìó ñåðåäîâèù³ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1998. — ¹ 4. — Ñ. 3–12.
3. Ê à ï è ò î í î â à Þ . Â . , Ë å ò è ÷ å â ñ ê è é À . À . , Â î ë ê î â Â . À . Äåäóêòèâíûå ñðåäñòâà ñèñòåìû
àëãåáðàè÷åñêîãî ïðîãðàììèðîâàíèÿ // Òàì æå. — 2000. — ¹ 1. — Ñ. 17–34.
4. H a n d b o o k of logic in Computer Science / Ed. by S. Abramsky, Dov M. Gabbay and T.S.E. Maibaum.
— Oxford: Oxford Univ. Press, 1993–2000.
5. Ê ë è í è Ñ . Ìàòåìàòè÷åñêàÿ ëîãèêà. — Ì.: Ìèð, 1973. — 480 ñ.
6. Í è ê è ò ÷ å í ê î Í . Ñ . , Ø ê è ë ü í ÿ ê Ñ . Ñ . Íåîêëàññè÷åñêèå ëîãèêè ïðåäèêàòîâ // Ïðîáëåìû ïðî-
ãðàììèðîâàíèÿ. — 2000. — ¹ 3–4. — C. 3–17.
7. Í è ê è ò ÷ å í ê î Í . Ñ . Êîìïîçèöèîííî-íîìèíàòèâíûé ïîäõîä ê óòî÷íåíèþ ïîíÿòèÿ ïðîãðàììû //
Òàì æå. — 1999.— ¹ 1. — C. 16–31.
8. Í ³ ê ³ ò ÷ å í ê î Ì . Ñ . , Ø ê ³ ë ü í ÿ ê Ñ . Ñ . Ìàòåìàòè÷íà ëîã³êà òà òåîð³ÿ àëãîðèòì³â. — Ê.: ÂÏÖ
Êè¿â. óí-òó, 2008. — 528 ñ.
9. Ð å ä ü ê î Â . Í . Êîìïîçèöèè ïðîãðàìì è êîìïîçèöèîííîå ïðîãðàììèðîâàíèå // Ïðîãðàììèðî-
âàíèå. — 1978. — ¹ 5. — Ñ. 3–24.
10. Ð å ä ü ê î Â . Í . Îñíîâàíèÿ êîìïîçèöèîííîãî ïðîãðàììèðîâàíèÿ // Òàì æå. — 1979. — ¹ 3. —
Ñ. 3–13.
11. Í è ê è ò ÷ å í ê î Í . Ñ . Àïïëèêàòèâíûå êîìïîçèöèè ÷àñòè÷íûõ ïðåäèêàòîâ // Êèáåðíåòèêà è ñèñòåì-
íûé àíàëèç. — 2001. — ¹ 2. — C. 14–33.
12. Ø ê ³ ë ü í ÿ ê Ñ . Ñ . Íåîêëàñè÷í³ êâàíòîðí³ ëîã³êè ç ð³âí³ñòþ // ³ñí. Êè¿â. óí-òó. Ñåð.: Ô³ç.-ìàò.
íàóêè. — 2003. — Âèï. 1. — C. 222–225.
13. Í ³ ê ³ ò ÷ å í ê î Ì . Ñ . , Ø ê ³ ë ü í ÿ ê Ñ . Ñ . Êîìïîçèö³éí³ ëîã³êè íîì³íàòèâíèõ äàíèõ // Ïðîáëåìû
ïðîãðàììèðîâàíèÿ. — 2003. — ¹ 3. — C. 29–40.
14. Í å ï å é â î ä à Í . Í . Ïðèêëàäíàÿ ëîãèêà. — Íîâîñèáèðñê: Èçä-âî Íîâîñèá. óí-òà, 2000. — 521 ñ.
15. Ñ ì è ð í î â à Å . Ä . Ëîãèêà è ôèëîñîôèÿ. — Ì.: ÐÎÑÑÏÝÍ, 1996. — 304 ñ.
Ïîñòóïèëà 15.03.2010
50 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 6
|