Доказательство теорем в нечеткой логике на основе структурной резолюции

Рассмотрен подход к доказательству теорем с нечеткой и не вполне истинной аргументаяцией. В качестве правила доказательного рассуждения используется композиционное правило вывода Л. Заде, а его процедурная реализация осуществляется механизмом опровержения. В качестве такого механизма предложена стру...

Full description

Saved in:
Bibliographic Details
Published in:Кибернетика и системный анализ
Date:2019
Main Author: Самохвалов, Ю.Я.
Format: Article
Language:Russian
Published: Інститут кібернетики ім. В.М. Глушкова НАН України 2019
Subjects:
Online Access:https://nasplib.isofts.kiev.ua/handle/123456789/180847
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:Доказательство теорем в нечеткой логике на основе структурной резолюции / Ю.Я. Самохвалов // Кибернетика и системный анализ. — 2019. — Т. 55, № 2. — С. 44-58. — Бібліогр.: 22 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-180847
record_format dspace
spelling Самохвалов, Ю.Я.
2021-10-22T14:49:02Z
2021-10-22T14:49:02Z
2019
Доказательство теорем в нечеткой логике на основе структурной резолюции / Ю.Я. Самохвалов // Кибернетика и системный анализ. — 2019. — Т. 55, № 2. — С. 44-58. — Бібліогр.: 22 назв. — рос.
1019-5262
https://nasplib.isofts.kiev.ua/handle/123456789/180847
681.61
Рассмотрен подход к доказательству теорем с нечеткой и не вполне истинной аргументаяцией. В качестве правила доказательного рассуждения используется композиционное правило вывода Л. Заде, а его процедурная реализация осуществляется механизмом опровержения. В качестве такого механизма предложена структурная резолюция (S -резолюция), которая является обобщением принципа резолюций на нечеткие утверждения. S -резолюция основана на семантических индексах литер и их сходстве. Семантические индексы являются существенным моментом S -резолюции. Они содержат информацию, которая используется в качестве управляющей в процессе вывода. А сходство заключается в поиске литер для получения S -резольвенты. Комплексирование композиционного правила вывода Л. Заде и S -резолюции позволяет, с одной стороны, снять проблему корректности резольвент в нечеткой логике, а с другой — обеспечить регулярность процесса доказательства как в двузначной, так и в нечеткой логике. Ключевые слова: автоматическое доказательство теорем, нечеткая теорема, принцип резолюций, нечеткая логика, приближенные рассуждения, обобщенное правило modus ponens, композиционное правило, нечеткие предикаты, нечеткие и лингвистические переменные.
Розглянуто підхід до доведення теорем у нечіткій логіці і не цілком істинною аргументацією. Як правило доказового міркування використовують композиційне правило виведення Л. Заде, а його процедурна реалізація здійснюється механізмом спростування. Структурна резолюція (S -резолюція), яка є узагальненням принципу резолюцій на нечіткі твердження, запропонована як такий механізм. S -резолюція базується на семантичних індексах літер і їхній схожості. Семантичні індекси є істотним моментом S -резолюції. Вони містять інформацію, яка використовується як керівна у процесі виводу, а схожість полягає у пошуку літер для отримання S -резольвенти. Комплексування композиційного правила виводу Л. Заде і S -резолюції дозволяє, з одного боку, зняти проблему коректності резольвент в нечіткій логіці, а з іншого — забезпечити регулярність процесу доведення як в двозначній, так і в нечіткій логіці.
The author considers the approach to proof of theorems with fuzzy and not quite true argumentation. In this approach, the Zadeh composition rule of correctness is used as a rule of evidence, and its procedural implementation is carried out by refutation mechanism. As such a mechanism, a structural resolution (S -resolution) is proposed, which is a generalization of the principle of resolutions to fuzzy statements. S -resolution is based on semantic indices of letters and their similarity. Semantic indices are a key point of S-resolution. They contain information that is used as a control for the derivation process. And similarity implies finding letters to get S-resolvent. Combining the Zadeh compositional derivation rule and S-resolution allows, on the one hand, solving the problem of correctness of resolvents in fuzzy logic, and on the other hand, ensuring the regularity of the proof process in both two-valued and fuzzy logic.
ru
Інститут кібернетики ім. В.М. Глушкова НАН України
Кибернетика и системный анализ
Кібернетика
Доказательство теорем в нечеткой логике на основе структурной резолюции
Доведення теорем у нечіткій логіці на основі структурної резолюції
Proof of theorems in fuzzy logic on the basis of structural resolution
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Доказательство теорем в нечеткой логике на основе структурной резолюции
spellingShingle Доказательство теорем в нечеткой логике на основе структурной резолюции
Самохвалов, Ю.Я.
Кібернетика
title_short Доказательство теорем в нечеткой логике на основе структурной резолюции
title_full Доказательство теорем в нечеткой логике на основе структурной резолюции
title_fullStr Доказательство теорем в нечеткой логике на основе структурной резолюции
title_full_unstemmed Доказательство теорем в нечеткой логике на основе структурной резолюции
title_sort доказательство теорем в нечеткой логике на основе структурной резолюции
author Самохвалов, Ю.Я.
author_facet Самохвалов, Ю.Я.
topic Кібернетика
topic_facet Кібернетика
publishDate 2019
language Russian
container_title Кибернетика и системный анализ
publisher Інститут кібернетики ім. В.М. Глушкова НАН України
format Article
title_alt Доведення теорем у нечіткій логіці на основі структурної резолюції
Proof of theorems in fuzzy logic on the basis of structural resolution
description Рассмотрен подход к доказательству теорем с нечеткой и не вполне истинной аргументаяцией. В качестве правила доказательного рассуждения используется композиционное правило вывода Л. Заде, а его процедурная реализация осуществляется механизмом опровержения. В качестве такого механизма предложена структурная резолюция (S -резолюция), которая является обобщением принципа резолюций на нечеткие утверждения. S -резолюция основана на семантических индексах литер и их сходстве. Семантические индексы являются существенным моментом S -резолюции. Они содержат информацию, которая используется в качестве управляющей в процессе вывода. А сходство заключается в поиске литер для получения S -резольвенты. Комплексирование композиционного правила вывода Л. Заде и S -резолюции позволяет, с одной стороны, снять проблему корректности резольвент в нечеткой логике, а с другой — обеспечить регулярность процесса доказательства как в двузначной, так и в нечеткой логике. Ключевые слова: автоматическое доказательство теорем, нечеткая теорема, принцип резолюций, нечеткая логика, приближенные рассуждения, обобщенное правило modus ponens, композиционное правило, нечеткие предикаты, нечеткие и лингвистические переменные. Розглянуто підхід до доведення теорем у нечіткій логіці і не цілком істинною аргументацією. Як правило доказового міркування використовують композиційне правило виведення Л. Заде, а його процедурна реалізація здійснюється механізмом спростування. Структурна резолюція (S -резолюція), яка є узагальненням принципу резолюцій на нечіткі твердження, запропонована як такий механізм. S -резолюція базується на семантичних індексах літер і їхній схожості. Семантичні індекси є істотним моментом S -резолюції. Вони містять інформацію, яка використовується як керівна у процесі виводу, а схожість полягає у пошуку літер для отримання S -резольвенти. Комплексування композиційного правила виводу Л. Заде і S -резолюції дозволяє, з одного боку, зняти проблему коректності резольвент в нечіткій логіці, а з іншого — забезпечити регулярність процесу доведення як в двозначній, так і в нечіткій логіці. The author considers the approach to proof of theorems with fuzzy and not quite true argumentation. In this approach, the Zadeh composition rule of correctness is used as a rule of evidence, and its procedural implementation is carried out by refutation mechanism. As such a mechanism, a structural resolution (S -resolution) is proposed, which is a generalization of the principle of resolutions to fuzzy statements. S -resolution is based on semantic indices of letters and their similarity. Semantic indices are a key point of S-resolution. They contain information that is used as a control for the derivation process. And similarity implies finding letters to get S-resolvent. Combining the Zadeh compositional derivation rule and S-resolution allows, on the one hand, solving the problem of correctness of resolvents in fuzzy logic, and on the other hand, ensuring the regularity of the proof process in both two-valued and fuzzy logic.
issn 1019-5262
url https://nasplib.isofts.kiev.ua/handle/123456789/180847
citation_txt Доказательство теорем в нечеткой логике на основе структурной резолюции / Ю.Я. Самохвалов // Кибернетика и системный анализ. — 2019. — Т. 55, № 2. — С. 44-58. — Бібліогр.: 22 назв. — рос.
work_keys_str_mv AT samohvalovûâ dokazatelʹstvoteoremvnečetkoilogikenaosnovestrukturnoirezolûcii
AT samohvalovûâ dovedennâteoremunečítkíilogícínaosnovístrukturnoírezolûcíí
AT samohvalovûâ proofoftheoremsinfuzzylogiconthebasisofstructuralresolution
first_indexed 2025-11-25T21:29:36Z
last_indexed 2025-11-25T21:29:36Z
_version_ 1850551672170872832
fulltext ÓÄÊ 681.61 Þ.ß. ÑÀÌÎÕÂÀËΠÄÎÊÀÇÀÒÅËÜÑÒÂÎ ÒÅÎÐÅÌ Â ÍÅ×ÅÒÊÎÉ ËÎÃÈÊÅ ÍÀ ÎÑÍÎÂÅ ÑÒÐÓÊÒÓÐÍÎÉ ÐÅÇÎËÞÖÈÈ Àííîòàöèÿ. Ðàññìîòðåí ïîäõîä ê äîêàçàòåëüñòâó òåîðåì ñ íå÷åòêîé è íå âïîëíå èñòèííîé àðãóìåíòàöèåé.  êà÷åñòâå ïðàâèëà äîêàçàòåëüíîãî ðàñ- ñóæäåíèÿ èñïîëüçóåòñÿ êîìïîçèöèîííîå ïðàâèëî âûâîäà Ë. Çàäå, à åãî ïðîöåäóðíàÿ ðåàëèçàöèÿ îñóùåñòâëÿåòñÿ ìåõàíèçìîì îïðîâåðæåíèÿ.  êà- ÷åñòâå òàêîãî ìåõàíèçìà ïðåäëîæåíà ñòðóêòóðíàÿ ðåçîëþöèÿ (S-ðåçîëþ- öèÿ), êîòîðàÿ ÿâëÿåòñÿ îáîáùåíèåì ïðèíöèïà ðåçîëþöèé íà íå÷åòêèå óòâåðæäåíèÿ. S-ðåçîëþöèÿ îñíîâàíà íà ñåìàíòè÷åñêèõ èíäåêñàõ ëèòåð è èõ ñõîäñòâå. Ñåìàíòè÷åñêèå èíäåêñû ÿâëÿþòñÿ ñóùåñòâåííûì ìîìåíòîì S-ðåçîëþöèè. Îíè ñîäåðæàò èíôîðìàöèþ, êîòîðàÿ èñïîëüçóåòñÿ â êà÷åñòâå óïðàâëÿþùåé â ïðîöåññå âûâîäà. À ñõîäñòâî çàêëþ÷àåòñÿ â ïîèñêå ëèòåð äëÿ ïîëó÷åíèÿ S-ðåçîëüâåíòû. Êîìïëåêñèðîâàíèå êîìïîçèöèîííîãî ïðàâèëà âû- âîäà Ë. Çàäå è S-ðåçîëþöèè ïîçâîëÿåò, ñ îäíîé ñòîðîíû, ñíÿòü ïðîáëåìó êîððåêòíîñòè ðåçîëüâåíò â íå÷åòêîé ëîãèêå, à ñ äðóãîé — îáåñïå÷èòü ðåãó- ëÿðíîñòü ïðîöåññà äîêàçàòåëüñòâà êàê â äâóçíà÷íîé, òàê è â íå÷åòêîé ëîãèêå. Êëþ÷åâûå ñëîâà: àâòîìàòè÷åñêîå äîêàçàòåëüñòâî òåîðåì, íå÷åòêàÿ òåîðåìà, ïðèíöèï ðåçîëþöèé, íå÷åòêàÿ ëîãèêà, ïðèáëèæåííûå ðàññóæäåíèÿ, îáîá- ùåííîå ïðàâèëî modus ponens, êîìïîçèöèîííîå ïðàâèëî, íå÷åòêèå ïðåäèêà- òû, íå÷åòêèå è ëèíãâèñòè÷åñêèå ïåðåìåííûå. ÀÍÀËÈÇ ÏÐÎÁËÅÌÛ È ÏÓÒÈ ÐÅØÅÍÈß Óñòàíîâëåíèå îòíîøåíèé ëîãè÷åñêîãî ñëåäñòâèÿ èëè, ÷òî òî æå ñàìîå, äîêàçà- òåëüñòâî òåîðåì ÿâëÿåòñÿ îäíîé èç ãëàâíûõ çàäà÷ ëîãèêè è ïðåäñòàâëÿåò íå òîëü- êî òåîðåòè÷åñêèé, íî è ïðàêòè÷åñêèé èíòåðåñ äëÿ ìíîãèõ íàó÷íûõ è òåõíè÷åñêèõ îáëàñòåé. Ðàçíîîáðàçíûå ïðîáëåìû ìîæíî ïîïûòàòüñÿ ðåøèòü, ïðåäñòàâëÿÿ îïè- ñàíèå çàäà÷è è îòíîñÿùóþñÿ ê íåé èíôîðìàöèþ â âèäå ëîãè÷åñêèõ àêñèîì è ðàññìàòðèâàÿ ðàçëè÷íûå ñëó÷àè çàäà÷è êàê òåîðåìû, êîòîðûå íóæíî äîêàçàòü.  íàñòîÿùåå âðåìÿ ðåçîëþöèîííûé ïðèíöèï ââèäó âûñîêîé ýôôåêòèâíîñòè ìàøèííîé ðåàëèçàöèè ñîñòàâëÿåò îñíîâó àâòîìàòè÷åñêîãî äîêàçàòåëüñòâà òåîðåì â äâóçíà÷íîé ëîãèêå. Îäíàêî äâóçíà÷íàÿ ëîãèêà íåïðèãîäíà äëÿ îáðàáîòêè íå÷åò- êîé àðãóìåíòàöèè è âûâîäîâ, õàðàêòåðíûõ äëÿ ïðèáëèæåííûõ ðàññóæäåíèé.  íå- ÷åòêèõ óñëîâèÿõ èñïîëüçîâàíèå ðåçîëþöèîííîãî ïðèíöèïà äëÿ äîêàçàòåëüñòâà òå- îðåì äîëæíî áàçèðîâàòüñÿ íå íà äâóçíà÷íîé, à íà íå÷åòêîé ëîãèêå. Âìåñòå ñ òåì â íå÷åòêîé ëîãèêå âûâîä ðåçîëþöèîííîãî òèïà ìîæåò èñïîëüçîâàòüñÿ òîëüêî ñ ñó- ùåñòâåííûìè îãðàíè÷åíèÿìè, òàê êàê îí íå âñåãäà ïðèâîäèò ê ïîëåçíûì ðåçóëüòà- òàì. Ýòî îáîñíîâàíî òåì, ÷òî â íå÷åòêîé ëîãèêå ëîãè÷åñêîå ñëåäñòâèå D èç ïîñûë- êè C çíà÷èìî òîëüêî òîãäà, êîãäà äëÿ âñåõ èíòåðïðåòàöèé âûïîëíåíî óñëîâèå T C T D( ) ( )� , (1) ãäå T C( ) è T D( ) — çíà÷åíèÿ èñòèííîñòè âûñêàçûâàíèé C è D ñîîòâåòñòâåí- íî.  [1] ïîêàçàíî, ÷òî ïðèìåíèòåëüíî ê ìåòîäó ðåçîëþöèé ýòî óñëîâèå âû- ïîëíÿåòñÿ, åñëè ñïðàâåäëèâî íåðàâåíñòâî T C C T R C C( , ) ( ( , ))1 2 1 2� èëè T L L T R C C( ) ( ( , ))�� � 1 2 , (2) ãäå R C C( , )1 2 — ðåçîëüâåíòà ïîñûëîê C1 è C2 , à L è �L — îòðåçàåìûå ëèòåðû â ýòèõ ïîñûëêàõ. Òàêèì îáðàçîì, â íå÷åòêîé ëîãèêå ðåçîëüâåíòó ìîæíî ïðèíÿòü â êà- ÷åñòâå âûâîäà ëèøü òîãäà, êîãäà îòðåçàåìûå ëèòåðû óäîâëåòâîðÿþò óñëîâèþ (2). 44 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 © Þ.ß. Ñàìîõâàëîâ, 2019 Ïðåäëàãàëîñü íåñêîëüêî ïîäõîäîâ ê îáîáùåíèþ ïðèíöèïà ðåçîëþöèé íà ñëó- ÷àé íå÷åòêîé ëîãèêè [2–7]. Òàê, â [2] ïðåäëîæåí ïðèíöèï íå÷åòêîé ðåçîëþöèè äëÿ ñëó÷àÿ íåîïðåäåëåííûõ ïðåäëîæåíèé.  [3] ââåäåíà íå÷åòêàÿ ãèïåððåçîëþöèÿ íà îñíîâå àíòîíèìîâ è äîêàçàíà åå ïîëíîòà. Íå÷åòêàÿ ðåçîëþöèÿ íà îñíîâå ïîíÿòèÿ ñõîäñòâà ñ ðàñøèðåííûì àëãîðèòìîì óíèôèêàöèè ðàññìîòðåíà â ðàáîòå [4].  ñòàòüå [5] ïîëó÷èë îáîáùåíèå ïðèíöèï ðåçîëþöèé, êîòîðûé ïðèìåíèì êàê äëÿ ÷åòêî îïðåäåëåííûõ, òàê è äëÿ íåîïðåäåëåííûõ ïðåäëîæåíèé.  ðàáîòàõ [6, 7] ðàñ- ñìîòðåíû ìåòîä è ñòðàòåãèè äîêàçàòåëüñòâà â íå÷åòêîé ëîãèêå ïðåäèêàòîâ íà îñíîâå îïðîâåðæåíèÿ ñ èñïîëüçîâàíèåì îáùåãî (non-clausal) ïðàâèëà ðåçîëþöèé.  öåëîì ïðåäëîæåííûå â ýòèõ ðàáîòàõ ïîäõîäû íå íàøëè øèðîêîãî ïðèìå- íåíèÿ ïðè ðåøåíèè ïðèêëàäíûõ çàäà÷, òàê êàê ðàçëè÷íûå ñåìàíòè÷åñêèå ïðåäïî- ëîæåíèÿ â òàêèõ ïîäõîäàõ îãðàíè÷èâàþò ìåõàíèçìû âûâîäà è äåëàþò èõ íåäîñòàòî÷íî ãèáêèìè.  íàñòîÿùåå âðåìÿ, ó÷èòûâàÿ ýôôåêòèâíîå ïðèìåíåíèå ñèñòåì íå÷åòêîãî âûâîäà ïðè ðåøåíèè øèðîêîãî êëàññà çàäà÷ óïðàâëåíèÿ [8], ïðåäïðèíèìàþòñÿ ïîïûòêè èñïîëüçîâàòü ìåòîäîëîãèþ ïðèáëèæåííûõ ðàññóæäåíèé è ïðè íå÷åò- êîì âûâîäå ðåçîëþöèîííîãî òèïà [9–12]. Îñíîâíàÿ èäåÿ ýòèõ èññëåäîâàíèé çà- êëþ÷àåòñÿ â òîì, ÷òîáû ïîëó÷èòü íåêîòîðîå îáîáùåíèå ïðèíöèïà ðåçîëþöèé ñ ó÷åòîì ïîëîæåíèé è ïîäõîäîâ ê ðåàëèçàöèè íå÷åòêèõ ðàññóæäåíèé. Òàê, â ðà- áîòå [12] ðàññìîòðåí ïðèíöèï ðåçîëþöèé äëÿ íå÷åòêèõ ôîðìóë, îñíîâàííûé íà ïîäîáèè è îáðàòíîì ïðèáëèæåííîì ðàññóæäåíèè. Ïîäîáèå ÿâëÿåòñÿ ñóùåñò- âåííûì ìîìåíòîì ðåçîëþöèè äâóõ äèçúþíêòîâ è çàêëþ÷àåòñÿ â ïîèñêå â ýòèõ äèçúþíêòàõ ïî÷òè êîìïëåìåíòàðíûõ ëèòåð. À ïðèìåíåíèå ïðèáëèæåííûõ ðàñ- ñóæäåíèé çàêëþ÷àåòñÿ â ïðåîáðàçîâàíèè íå÷åòêèõ äèçúþíêöèé â íå÷åòêèå èì- ïëèêàöèè (íå÷åòêèå ïðàâèëà), êîòîðûå çàòåì âûïîëíÿþòñÿ ìåòîäîì îáðàòíîãî ïðèáëèæåííîãî ðàññóæäåíèÿ. Ïðè ýòîì ïðåäïîëàãàåòñÿ, ÷òî íå÷åòêèå ðàññóæ- äåíèÿ âïîëíå èñòèííû. Òàêîå îáîáùåíèå ïðèíöèïà ðåçîëþöèé ÿâëÿåòñÿ åñòåñò- âåííûì, îäíàêî ïðîáëåìà îáåñïå÷åíèÿ çíà÷èìîñòè ðåçîëþöèîííûõ âûâîäîâ â ñìûñëå (1) îñòàåòñÿ îòêðûòîé è òðåáóåò èñïîëüçîâàíèÿ äîïîëíèòåëüíûõ ìåõà- íèçìîâ ñ öåëüþ ïîëó÷èòü êîððåêòíûå çàêëþ÷åíèÿ. Íàñòîÿùàÿ ñòàòüÿ ÿâëÿåòñÿ ðàçâèòèåì ðàññìîòðåííûõ â ðàáîòå [13] èäåé è ìå- õàíèçìîâ èñïîëüçîâàíèÿ ïðèíöèïà ðåçîëþöèé ïðè äîêàçàòåëüñòâå òåîðåì ñ íå- îïðåäåëåííîé àðãóìåíòàöèåé è ïðåäëàãàåò àëüòåðíàòèâíûé ïîäõîä ê äîêàçà- òåëüñòâó â íå÷åòêîé ëîãèêå. Åãî îñíîâíàÿ èäåÿ ñîñòîèò â èñïîëüçîâàíèè êîìïîçè- öèîííîãî ïðàâèëà íå÷åòêîãî âûâîäà Ë. Çàäå (äàëåå — êîìïîçèöèîííîå ïðàâèëî) â êà÷åñòâå ïðàâèëà äîêàçàòåëüíîãî ðàññóæäåíèÿ, à ïðèíöèïà ðåçîëþöèé — êàê ìå- õàíèçìà åãî ðåàëèçàöèè. Òàêîé ñèíåðãèçì ïîçâîëÿåò ñíÿòü ïðîáëåìó çíà÷èìîñòè ðåçîëüâåíò â ñìûñëå (1) è îáåñïå÷èòü ðåãóëÿðíîñòü ïðîöåññà äîêàçàòåëüñòâà. ËÎÃÈÊÀ ÍÅ×ÅÒÊÎÃÎ ÂÛÂÎÄÀ Èñõîäÿ èç òåîðèè äîêàçàòåëüñòâ, êàê ðàçäåëà ìàòåìàòè÷åñêîé ëîãèêè, óñòàíîâëåíèå èñòèííîñòè òåîðåìû íåïîñðåäñòâåííî çàâèñèò îò èñïîëüçóåìûõ ïðàâèë ëîãè÷åñêîãî âûâîäà. Òàêèå ïðàâèëà äîëæíû îáåñïå÷èâàòü ïðè÷èííî-ñëåäñòâåííóþ íàïðàâëåí- íîñòü ïðîöåññà äîêàçàòåëüñòâà è ó÷èòûâàòü ôîðìó ïðåäñòàâëåíèÿ òåîðåìû. Òåîðèÿ äîêàçàòåëüñòâ ðàññìàòðèâàåò òåîðåìû êàê óòâåðæäåíèÿ ôîðìàëüíîãî ÿçûêà. Ïóñòü F1, F2 , …, Fn , G – ôîðìóëû òåîðèè � . Òîãäà òåîðåìó ìîæíî ïðåä- ñòàâèòü â âèäå F1, F2 , …, F Gn |�� � , à åå äîêàçàòåëüñòâî ñâîäèòñÿ ê äîêàçàòåëüñòâó òîãî, ÷òî ôîðìóëà G âûâîäèìà èç ôîðìóë F1, F2 , …, Fn â òåîðèè �, ÷òî ðàâíî- ñèëüíî äîêàçàòåëüñòâó òîãî, ÷òî ôîðìóëà G ÿâëÿåòñÿ ëîãè÷åñêèì ñëåäñòâèåì ìíî- æåñòâà ôîðìóë F1, F2 , …, Fn . Ïîýòîìó òåîðåìó ìîæíî ïðåäñòàâèòü òàêæå â âèäå (F1 , F2 , ..., F Gn )� (3) è ñôîðìóëèðîâàòü åå ïðàâèëîì ïðîäóêöèè: «Åñëè F1, F2 , …, Fn èñòèííû Òî èñòèííà è G». Çäåñü ôîðìóëû F1, F2 , …, Fn ÿâëÿþòñÿ àêñèîìàìè, à G — çà- êëþ÷åíèåì òåîðåìû. ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 45 Åñëè ôîðìàëüíîé òåîðèåé � ÿâëÿåòñÿ íå÷åòêàÿ ëîãèêà, òî ôîðìóëû F1, F2 ,... …, Fn , G (èëè èõ ÷àñòü) â (3) ÿâëÿþòñÿ íå÷åòêèìè [14, 15]. Ïðè ýòîì, ñîãëàñíî Ë. Çàäå çíà÷åíèå èñòèííîñòè çàêëþ÷åíèÿ G åñòü èñòèííûì â ïðèáëèæåííîì ñìûñëå è åãî ìîæíî âûâåñòè èç ñèñòåìû àêñèîì, èñïîëüçóÿ ïðèáëèæåííûå ðàññóæäåíèÿ. Ïîä ïðèáëèæåííûìè ðàññóæäåíèÿìè ïîíèìàåòñÿ ïðîöåññ ïîëó÷åíèÿ èç íå- ÷åòêèõ ïîñûëîê íåêîòîðûõ ñëåäñòâèé, âîçìîæíî òàêæå íå÷åòêèõ. Ïðèáëèæåííûå ðàññóæäåíèÿ ýêñïëèöèðóþòñÿ ïðàâèëàìè íå÷åòêèõ ïðîäóêöèé, êîòîðûå íå òîëü- êî ïîçâîëÿþò àäåêâàòíî ïðåäñòàâèòü ïðàêòè÷åñêèå çíàíèÿ ýêñïåðòîâ â òîé èëè èíîé ïðîáëåìíîé îáëàñòè, íî, ÷òî î÷åíü âàæíî, ïðîäóêöèîííîå ïðåäñòàâëåíèå çíàíèé ñ òî÷êè çðåíèÿ ÷åëîâåêà ÿâëÿåòñÿ ïðÿìûì îïèñàíèåì ëîãè÷åñêèõ âûâî- äîâ ïðè ðåøåíèè êîíêðåòíûõ çàäà÷. Êðîìå ýòîãî, ïðàâèëà íå÷åòêèõ ïðîäóêöèé ïîëíîñòüþ êîððåñïîíäèðóþòñÿ ñ ïðåäñòàâëåíèåì òåîðåìû â ôîðìå (3). Êîíöåïòóàëüíîé îñíîâîé ôîðìàëèçàöèè ïðàâèë íå÷åòêèõ ïðîäóêöèé ÿâëÿåò- ñÿ îáîáùåííûé modus ponens A A B B *, � , ãäå A * , A, B — íå÷åòêèå âûñêàçûâà- íèÿ, êîòîðûå ìîãóò áûòü íå÷åòêèìè ìíîæåñòâàìè. Ýòî ïðàâèëî óòâåðæäàåò ñëå- äóþùåå: åñëè A B� èñòèííî è èìååò ìåñòî A * , ãäå A * — â íåêîòîðîì ñìûñëå ïðèáëèæåíèå A , òî îòñþäà ñëåäóåò, ÷òî B ïðèáëèæåííî èñòèííî. Ìåòîäîëîãè÷åñêèì áàçèñîì òàêîé ôîðìàëèçàöèè ÿâëÿåòñÿ êîìïîçèöèîííîå ïðàâèëî B A A B� �* ( )� , ãäå çíàê � — îïåðàöèÿ ìàêñèìèííîé ñâåðòêè A * è A B� . Ïóñòü U — íåêîòîðîå ìíîæåñòâî ýëåìåíòàðíûõ íå÷åòêèõ âûñêàçûâà- íèé, à T U: [ , ]� 0 1 — îòîáðàæåíèå èñòèííîñòè âûñêàçûâàíèé èç U â èíòåð- âàë [0, 1]. Îáîçíà÷èì T C( ) çíà÷åíèå èñòèííîñòè íå÷åòêîãî âûñêàçûâàíèÿ C U . Òîãäà â îáùåì ñëó÷àå èñòèííîñòü âûñêàçûâàíèÿ B îïðåäåëÿåòñÿ ñëåäóþùèì îá- ðàçîì: T B( ) maxmin� (T(A Ai| * ), (T A B( � )), i n�1, , (4) ãäå T(A Ai| * ) — ñòåïåíü èñòèííîñòè ïîñûëêè A ïðè íàëè÷èè âûñêàçûâàíèÿ Ai * . Ïðè ýòîì åñëè íå÷åòêîå âûñêàçûâàíèå A ÿâëÿåòñÿ ñîñòàâíûì, òî åãî èñòèííîñòü T A( ) âû÷èñëÿåòñÿ ïî êëàññè÷åñêèì ôîðìóëàì min-êîíúþíêöèè è màõ-äèçúþíêöèè. Êðîìå òîãî, âû÷èñëåíèå èñòèííîñòè T A B( )� â (4) ïî èçâåñòíûì ôîðìóëàì íå÷åòêîé èìïëèêàöèè íå ïðåäñòàâëÿåòñÿ âîçìîæíûì, òàê êàê äëÿ ýòîãî íåîáõîäè- ìî çíà÷åíèå T B( ) . Ïîýòîìó âìåñòî êëàññè÷åñêîé èìïëèêàöèè A B� èñïîëüçóåì èìïëèêàöèþ âèäà A B� ( )� , êîòîðàÿ ÿâëÿåòñÿ îñíîâíîé â ñèñòåìàõ íå÷åòêîãî âûâîäà. Çäåñü � — êîýôôèöèåíò óâåðåííîñòè (âåñîâîé êîýôôèöèåíò), âûðàæàþ- ùèé îöåíêó ñòåïåíè èñòèííîñòè èëè îòíîñèòåëüíûé âåñ íå÷åòêîé ïðîäóêöèè. Ýòîò êîýôôèöèåíò ÿâëÿåòñÿ çíà÷åíèåì T A B( )� . Ñ ó÷åòîì ýòîãî ëîãè÷åñêîå ñëåäñòâèå B íå÷åòêîãî ïðàâèëà modus ponens âñåãäà çíà÷èìî â ñìûñëå (1). Äàëåå, ïîíÿòèå èñòèííîñòè â íå÷åòêîé ëîãèêå èìååò «ðàçìûòûé»» õàðàêòåð, ïðè ýòîì èíòåðâàë [0, 1] èñïîëüçóåòñÿ êàê óíèâåðñàëüíîå ìíîæåñòâî äëÿ çàäàíèÿ ëèíãâèñòè÷åñêîé ïåðåìåííîé «èñòèííîñòü». Íå÷åòêàÿ èñòèííîñòü îïðåäåëÿåòñÿ àêñèîìàòè÷åñêè, ïðè÷åì ðàçíûå àâòîðû îáîñíîâûâàþò ýòî ïî-ðàçíîìó. Åñëè âñå çíà÷åíèÿ èç èíòåðâàëà [0, 1] äîïóñòèìû â êà÷åñòâå çíà÷åíèé «èñòèííî» èëè «ëîæíî», òî íàèáîëåå èíòóèòèâíî ïîíÿòíûìè ÿâëÿþòñÿ ôóíêöèè ïðèíàäëåæíî- ñòè Áàëäâèíà äëÿ òåðìîâ «èñòèííî» è «ëîæíî»: � «èñòèííî» ( )x x� , � «ëîæíî» ( )x x� �1 , êîòîðûå êîëè÷åñòâåííî ãðàäóèðóþò ïðèíàäëåæíîñòü çíà÷åíèé èñòèííîñòè x [ , ]0 1 íå÷åòêèì ìíîæåñòâàì èñòèííî è ëîæíî.  ñëó÷àÿõ, êîãäà öåëåñîîáðàçíî ðàçäåëèòü èíòåðâàë [0, 1] íà çíà÷åíèÿ èñòèí- íî è ëîæíî, òîãäà äëÿ ýòèõ òåðìîâ ñëåäóåò èñïîëüçîâàòü ïðåäëîæåííûå Ë. Çàäå 46 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 ñëåäóþùèå ôóíêöèè ïðèíàäëåæíîñòè: � «èñòèííî» ( ) , , , ,x x a x a a a x a x a � � � � � � � � � � � � � � � � � � 0 0 2 1 1 2 1 2 1 1 2 � � � � � � � � � � � � � � � 2 1 2 1, , a x � «ëîæíî» ( )x � � «èñòèííî» ( )1� x , ãäå a [ , ]0 1 — ïàðàìåòð, îïðåäåëÿþùèé íîñèòåëè íå÷åòêèõ ìíîæåñòâ èñòèííî è ëîæíî. Íîñèòåëåì äëÿ íå÷åòêîãî ìíîæåñòâà èñòèííî ÿâëÿåòñÿ èíòåð- âàë ( , ]a 1 , à äëÿ íå÷åòêîãî ìíîæåñòâà ëîæíî — èíòåðâàë [ , )0 a . Òàêèì îáðàçîì, èñïîëüçîâàíèå íå÷åòêèõ ïðàâèë ïðîäóêöèé ïîçâîëÿåò ôîðìèðî- âàòü åñòåñòâåííûå âûâîäû, êîòîðûå áëèçêè ê ñîäåðæàòåëüíîìó ðàññóæäåíèþ ÷åëîâå- êà, è îáåñïå÷èâàòü ïðè÷èííî-ñëåäñòâåííóþ íàïðàâëåííîñòü ïðîöåññà äîêàçàòåëüñòâà. Âìåñòå ñ òåì ïðèìåíåíèå íå÷åòêèõ ïðàâèë ïðîäóêöèé äëÿ àâòîìàòè÷åñêîãî äîêàçàòåëüñòâà òåîðåì íåäîñòàòî÷íî ñîñòîÿòåëüíî. Ýòî ñâÿçàíî ñ òåì, ÷òî â ïðî- äóêöèîííûõ ìîäåëÿõ ñóùåñòâåííûì ìîìåíòîì ÿâëÿåòñÿ ïðîâåðêà ïðèìåíèìîñòè ïðàâèë, êîòîðàÿ ïðåäïîëàãàåò èñïîëüçîâàíèå (âîçìîæíî, çíà÷èòåëüíîãî êîëè÷åñòâà) ñîîòâåòñòâóþùèõ ïðàâèë âûâîäà. À ïîñêîëüêó âûáîð òàêèõ ïðàâèë îòíîñèòñÿ ê êîìïåòåíöèè ÷åëîâåêà, ýòî ñóùåñòâåííî çàòðóäíÿåò, à â íåêîòîðûõ ñëó÷àÿõ äåëàåò íåâîçìîæíûì ìåõàíèçàöèþ ïðîöåññà äîêàçàòåëüñòâà. Òàêèì îáðàçîì, èäåÿ çàêëþ÷àåòñÿ â ðåàëèçàöèè íå÷åòêîãî ïðîäóêöèîííîãî âûâîäà åäèíñòâåííûì ïðàâèëîì — ïðàâèëîì ðåçîëþöèé. Ïóñòü çàäàíî ïðàâèëî A A B B *, ( )� � . Ïðåäñòàâèì èìïëèêàöèþ ýòîãî ïðàâè- ëà â âèäå � �A B è ïîëîæèì C A1 � * è C A B2 �� � . Ïóñòü òàêæå � — ìåðà ñõîä- ñòâà ìåæäó A è A * , êîòîðàÿ áóäåò ïðåäñòàâëÿòü çíà÷åíèå T(A A| * ). Åñëè ïðèìå- íèòü ïðàâèëî ðåçîëþöèé ê äèçúþíêòàì C1 è C2 , òî ïîëó÷èì ðåçîëüâåíòó B, ñòå- ïåíü èñòèííîñòè êîòîðîé ñîãëàñíî (4) ìîæíî ïîëó÷èòü ïî ôîðìóëå T B( ) min ( ,� � ��. Äàëåå, ïóñòü ïîñûëêà A ÿâëÿåòñÿ ñîñòàâíûì âûñêàçûâàíèåì. Áåç ïîòåðè îá- ùíîñòè ïóñòü A A An� � �1 � è èìåþò ìåñòî óòâåðæäåíèÿ A An1 * *, ..., . Òîãäà, ïî- ñëåäîâàòåëüíî îòðåçàÿ ëèòåðû �Ai â äèçúþíêòå � �� � �� �A A A Bn1 2 ... , ïîëó÷èì çàêëþ÷åíèå B, èñòèííîñòü êîòîðîãî âû÷èñëÿåòñÿ ïî ôîðìóëå T B( ) = min (T(A), �), ãäå T A n( ) min( , ..., )� � �1 , à � i — ìåðà ñõîäñòâà ìåæäó Ai è Ai * . Ïðè ýòîì, ÷òî î÷åíü âàæíî, íåîáõîäèìîñòü ïðîâåðêè ðåçîëþöèîííûõ âûâîäîâ (ðåçîëüâåíò) íà çíà- ÷èìîñòü èõ â ñìûñëå (2) îòïàäàåò.  öåëîì ýòè ïîëîæåíèÿ áóäåì ðàññìàòðèâàòü êàê ïðîöåäóðíûé áàçèñ íå÷åòêîãî âûâîäà ïðè äîêàçàòåëüñòâå òåîðåì â íå÷åòêîé ëîãèêå. ÑÅÌÀÍÒÈ×ÅÑÊÈÅ ÈÍÄÅÊÑÛ ×òîáû ðåàëèçîâàòü ïðîöåäóðíûé áàçèñ, ðàññìîòðåííûé âûøå, íåîáõîäèìî ðàç- ëè÷àòü äèçúþíêòû ôàêòîâ, ïðàâèë è çàêëþ÷åíèÿ òåîðåìû. Äëÿ èõ èäåíòèôèêà- öèè èñïîëüçóåì ñåìàíòè÷åñêèå èíäåêñû [13], êîòîðûå ïîçâîëÿþò ñòðóêòóðèðî- âàòü ìíîæåñòâî äèçúþíêòîâ è ïðèäàòü åìó îñìûñëåííûé õàðàêòåð. Ñåìàíòè÷åñêèé èíäåêñ ïðèñâàèâàåòñÿ êàæäîé ëèòåðå è ìîæåò áûòü ôîðìàëèçî- âàí ðàçëè÷íûì ñïîñîáîì. Ïðåäñòàâèì åãî ôðåéìîì — êîðòåæåì âèäà � �N S S S, , ,1 2 3 , ãäå N – èìÿ (ñåìàíòè÷åñêèé èíäåêñ ëèòåðû); S1 — ìíîæåñòâî ñëîòîâ, ñîäåðæàùèõ ôàêòû, êîòîðûå îïðåäåëÿþò äåêëàðàòèâíóþ ñåìàíòèêó ëèòåðû; ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 47 S 2 — ìíîæåñòâî ñëîòîâ, êîòîðûå îáåñïå÷èâàþò ñâÿçè ñ äðóãèìè ëèòåðàìè òåîðåìû (êàóçàëüíûå, ñåìàíòè÷åñêèå è ò.ä.); S 3 — ìíîæåñòâî ñëîòîâ, îáåñïå÷èâàþùèõ ïðåîáðàçîâàíèÿ è îïðåäåëÿþùèå ïðîöåäóðíóþ ñåìàíòèêó ëèòåðû. Çäåñü ñëîòû ìíî- æåñòâà S1 ÿâëÿþòñÿ îáÿçàòåëüíûìè, à ñëîòû ìíîæåñòâ S 2 è S 3 — äîïîëíèòåëüíûìè. Ê îáÿçàòåëüíûì ñëîòàì îòíîñÿòñÿ ñòàòóñ è èñòèííîñòü. Ñòàòóñ ëèòåðû îïðåäåëÿåò åå ïðèíàäëåæíîñòü ê ýëåìåíòàì òåîðåìû è ìîæåò ïðèíèìàòü ñëåäóþ- ùèå çíà÷åíèÿ: ô — ëèòåðà-ôàêò, à(ê) — ëèòåðà-àíòåöåäåíò (êîíñåêâåíò) ïðàâèëà, ç — ëèòåðà-çàêëþ÷åíèå òåîðåìû. Ñòàòóñ òàêæå ìîæåò ïðèíèìàòü çíà÷åíèå î — îòðåçàííàÿ ëèòåðà â ðåçóëüòàòå ïðèìåíåíèÿ ðåçîëþöèè. Çíà÷åíèåì ñëîòà èñòèííîñòü äëÿ ëèòåð-ôàêòîâ, àíòåöåäåíòîâ è çàêëþ÷åíèÿ òåîðåìû ÿâëÿåòñÿ ñòåïåíü èõ èñòèííîñòè; äëÿ ëèòåð-êîíñåêâåíòîâ — êîýôôèöèåíò óâåðåííîñòè ñîîòâåòñòâóþùèõ ïðàâèë. Çàìåòèì, ÷òî ïðè èçìåíåíèè ñòàòóñà ëè- òåðû èëè åå èñòèííîñòè ñîîòâåòñòâóþùèå çíà÷åíèÿ èíäåêñà òàêæå èçìåíÿþòñÿ. Äîïîëíèòåëüíûå ñëîòû èç ñîîòâåòñòâóþùèõ ìíîæåñòâ ìîãóò îòðàæàòü ïðè- êëàäíûå îñîáåííîñòè òåîðåìû, ñâÿçàííûå, íàïðèìåð, ñ ad hoc ñòðàòåãèÿìè, êîòî- ðûå èñïîëüçóþòñÿ ïðè ðåøåíèè ðàçëè÷íûõ çàäà÷. Òàê, â êà÷åñòâå ñëîòà ìíîæåñò- âà S 2 ìîæåò áûòü ñëîò ñâÿçü, îáåñïå÷èâàþùèé äåäóêòèâíóþ ñâÿçü ïðàâèë. Çíà÷å- íèåì ýòîãî ñëîòà ìîæåò áûòü ñèìâîë «ñ». Íàïðèìåð, ïóñòü ïðàâèëî âûâîäà çàäàíî â ñëåäóþùåì âèäå: R x y z u w P x y u P y z P u z:( )( )( )( )( )( )( ( , , ) ( , , ) ( ,� � � � � � � �� � , )w � � � � � � � � � �P x w x y z u w P x y u P y( , , )) ( )( )( )( )( )( )( ( , , ) ( ,� � z, )� � � �P x w P u z w( , , ) ( , , ))� .  êëàóçàëüíîì âèäå ýòî ïðàâèëî ïðåäñòàâëåíî äâóìÿ äåäóêòèâíî-ñâÿçàííûìè äèçúþíêòàìè-ïðàâèëàìè: 1) � �� �� �P x y u P y z P u z w P x w1 2 3 4( , , ) ( , , ) ( , , ) ( , , )� � , 2) � �� �� �P x y u P y z P x w P u z w5 6 7 3( , , ) ( , , ) ( , , ) ( , , )� � . Ëèòåðû äèçúþíêòîâ ïðîèíäåêñèðîâàíû äëÿ èõ óñëîâíîé èäåíòèôèêàöèè.  ýòèõ ïðàâèëàõ ëèòåðû P x w4 ( , , )� è �P x w7 ( , , )� îáåñïå÷èâàþò èõ äåäóêòèâíóþ ñâÿçü. Ýòî îçíà÷àåò, ÷òî ïîñëå ñðàáàòûâàíèÿ ïðàâèëà ï. 1), ò.å. ïîëó÷åíèÿ ëèòåðû P x w4 ( , , )� â êà÷åñòâå ðåçîëüâåíòû, ýòà ëèòåðà áóäåò ðåçîëüâèðîâàòü ñ ëèòåðîé �P x w7 ( , , )� ïðàâèëà ï. 2). Êðîìå ýòîãî, â êà÷åñòâå ñëîòà ìíîæåñòâà S 3 ìîæåò áûòü ñëîò ïîðÿäîê, êîòîðûé óêàçûâàåò íà ïîñëåäîâàòåëüíîñòü îòðåçàíèÿ ëèòåð àíòåöåäåíòà ïðàâèëà â ñëó÷àå íà- ëè÷èÿ âîçìîæíûõ âàðèàíòîâ. Äëÿ ïðàâèëà ï. 1), íàïðèìåð, âîçìîæíà òàêàÿ ïîñëåäî- âàòåëüíîñòü îòðåçàíèÿ ëèòåð: 3, 1, 2. Ýòè ÷èñëà áóäóò çíà÷åíèÿìè ñëîòà ïîðÿäîê ñå- ìàíòè÷åñêèõ èíäåêñîâ ëèòåð àíòåöåäåíòà ýòîãî ïðàâèëà.  öåëîì ñåìàíòè÷åñêèå èí- äåêñû ìîæíî ðàññìàòðèâàòü, êàê óïðàâëÿþùóþ èíôîðìàöèþ è èñïîëüçîâàòü åå â ïðîöåññå äîêàçàòåëüñòâà äëÿ ñîêðàùåíèÿ ïðîñòðàíñòâà ïîèñêà ðåøåíèÿ. Ïîä ñòðóêòóðèðîâàííûì ìíîæåñòâîì äèçúþíêòîâ áóäåì ïîíèìàòü òàêîå ìíîæåñòâî, â êîòîðîì êàæäîé ëèòåðå ïðèñâîåí ñåìàíòè÷åñêèé èíäåêñ.  äàëü- íåéøåì (åñëè íå îãîâîðåíî ïðîòèâíîå) áóäåì ñ÷èòàòü, ÷òî ðàññìàòðèâàåìîå ìíî- æåñòâî äèçúþíêòîâ ÿâëÿåòñÿ ñòðóêòóðèðîâàííûì. ÀÊÑÈÎÌÀÒÈÇÀÖÈß ÒÅÎÐÅÌÛ Êàê áûëî îòìå÷åíî, ëþáóþ çàäà÷ó ïðàêòèêè ìîæíî ïîïûòàòüñÿ ðåøèòü, ïðåä- ñòàâëÿÿ åå îïèñàíèå è îòíîñÿùóþñÿ ê íåé èíôîðìàöèþ â âèäå ëîãè÷åñêèõ àê- ñèîì è ðàññìàòðèâàÿ ðàçëè÷íûå ïîñòàíîâêè çàäà÷è êàê òåîðåìû, òðåáóþùèå äî- êàçàòåëüñòâà. Ïîýòîìó â äàëüíåéøåì ïîíÿòèÿ «çàäà÷à» è «òåîðåìà», à òàêæå «ðåøåíèå çàäà÷è» è «äîêàçàòåëüñòâî òåîðåìû» áóäåì ñ÷èòàòü ñèíîíèìàìè. Ïðîöåññó äîêàçàòåëüñòâà â ëîãèêå ïðåäèêàòîâ ïðåäøåñòâóåò ïîäãîòîâèòåëüíûé ýòàï, êîòîðûé ñîñòîèò â àêñèîìàòèçàöèè ïîñûëîê è çàêëþ÷åíèè òåîðåìû, çàäàííîé íà åñòåñòâåííîì ÿçûêå. Ê îïåðàöèÿì ýòîãî ýòàïà îòíîñÿòñÿ ïîñòðîåíèå ôîðìóë ÿçû- 48 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 êà ïðåäèêàòîâ, ïðèâåäåíèå èõ â ïðåäâàðåííóþ íîðìàëüíóþ ôîðìó è çàòåì â ñêóëå- ìîâñêóþ ñòàíäàðòíóþ ôîðìó èëè ïðîñòî â ñòàíäàðòíóþ ôîðìó (êîíúþíêòèâíóþ íîðìàëüíóþ ôîðìó).  ðåçóëüòàòå òåîðåìà áóäåò ïðåäñòàâëåíà â êëàóçàëüíîì âèäå.  ïðåäëàãàåìîì ïîäõîäå óêàçàííûå ïîäãîòîâèòåëüíûå îïåðàöèè òàêæå èìå- þò ìåñòî. Ñíà÷àëà òåîðåìà ïðåäñòàâëÿåòñÿ íà åñòåñòâåííîì ÿçûêå. Îñíîâó âåð- áàëüíîãî îïèñàíèÿ åå ôàêòîâ è çàêëþ÷åíèÿ ñîñòàâëÿþò ÷åòêèå è íå÷åòêèå ýëå- ìåíòàðíûå âûñêàçûâàíèÿ (óòâåðæäåíèÿ), êîòîðûå ìîãóò áûòü äâóõ òèïîâ. 1. Âûñêàçûâàíèå «a åñòü b». Åñëè âûñêàçûâàíèå ÷åòêîå, òî a — ýòî íàèìåíî- âàíèå ñóùíîñòè, à b — íàèìåíîâàíèå åå ñâîéñòâà. Åñëè âûñêàçûâàíèå íå÷åòêîå, òîãäà a è b ÿâëÿþòñÿ íàèìåíîâàíèåì ëèíãâèñòè÷åñêîé ïåðåìåííîé è åå çíà÷åíè- åì ñîîòâåòñòâåííî. 2. Âûñêàçûâàíèå «a R b», ãäå a, b — ýëåìåíòû ìíîæåñòâ A è B, à R — íàèìåíî- âàíèå îòíîøåíèÿ ìåæäó a è b. Åñëè îòíîøåíèå íå÷åòêîå, òî R — íå÷åòêàÿ ïåðåìåí- íàÿ. Áóäåì ðàññìàòðèâàòü òîëüêî áèíàðíûå îòíîøåíèÿ, òàê êàê n-àðíûå îòíîøåíèÿ, âî-ïåðâûõ, ñëîæíû äëÿ âîñïðèÿòèÿ è îáðàáîòêè, à âî-âòîðûõ, ïðè íåîáõîäèìîñòè èõ ìîæíî ïðåäñòàâèòü â âèäå åñòåñòâåííîãî ñîåäèíåíèÿ áèíàðíûõ îòíîøåíèé. Âåðáàëèçàöèÿ ïðàâèë âûâîäà òåîðåìû îñóùåñòâëÿåòñÿ âûñêàçûâàíèÿìè â ôîðìå ñòðóêòóðèðîâàííîãî òåêñòà: «Åñëè óñëîâèå Òî çàêëþ÷åíèå (�)». Çäåñü � ÿâëÿåòñÿ êîýôôèöèåíòîì óâåðåííîñòè ïðàâèëà. Îñíîâó âåðáàëüíîãî îïèñàíèÿ óñëîâèé è çàêëþ÷åíèé ïðàâèë òàêæå ñîñòàâëÿþò ÷åòêèå è íå÷åòêèå ýëåìåíòàð- íûå âûñêàçûâàíèÿ, êîòîðûå ìîãóò ñîäåðæàòü ïðåäìåòíûå ïåðåìåííûå. Îòíîñèòåëüíî ïðàêòè÷åñêîé íàïðàâëåííîñòè òåîðåì ñäåëàåì íåñêîëüêî óòî÷íåíèé.  êà÷åñòâå ôàêòîâ è çàêëþ÷åíèÿ òåîðåìû áóäåì èñïîëüçîâàòü òîëüêî ýëåìåíòàðíûå âûñêàçûâàíèÿ. Ïîñêîëüêó ôàêòû ìîãóò áûòü íå âïîëíå äîñòîâåð- íûìè (íàïðèìåð, ðàçâåääàííûå), êàæäîìó èç íèõ ñîîòâåòñòâóåò êîýôôèöèåíò äîñòîâåðíîñòè r. Ïîä äîñòîâåðíîñòüþ ôàêòà áóäåì ïîíèìàòü ñâîéñòâî ñîäåðæà- ùåéñÿ â íåì èíôîðìàöèè îòðàæàòü îáúåêòèâíóþ ðåàëüíîñòü ñ íåîáõîäèìîé òî÷- íîñòüþ. Ïðè ýòîì èñòî÷íèêîì ôàêòîâ ìîæåò áûòü êàê ÷åëîâåê, òàê è òåõíè÷åñêîå óñòðîéñòâî. Âîïðîñû îöåíêè äîñòîâåðíîñòè èíôîðìàöèè ðàññìîòðåíû â ðàáîòàõ ìíîãèõ àâòîðîâ, íàïðèìåð â [16, 17], ïîýòîìó äëÿ ñîêðàùåíèÿ îáúåìà ñòàòüè èõ îïóñêàåì. Çàìåòèì òîëüêî, ÷òî êîýôôèöèåíòû äîñòîâåðíîñòè è óâåðåííîñòè ïðèíàäëåæàò èíòåðâàëó [ , ]0 1 è ïî óìîë÷àíèþ ðàâíû åäèíèöå. Óñëîâèÿ ïðàâèë ïðîäóêöèé ìîãóò èìåòü ñëîæíóþ ëîãè÷åñêóþ ñòðóêòóðó è ïðåäñòàâëÿòü ñîáîé âûñêàçûâàíèÿ, ñîñòàâëåííûå èç ýëåìåíòàðíûõ ñ ïîìîùüþ îïåðàöèé È, ÈËÈ, ÍÅ.  êà÷åñòâå çàêëþ÷åíèé ïðàâèë áóäåì ðàññìàòðèâàòü òîëüêî ýëåìåíòàðíûå âûñêàçûâàíèÿ. Òåîðåìà, çàäàííàÿ íà åñòåñòâåííîì ÿçûêå, îòîáðàæàåòñÿ íà íåêîòîðûé ôîð- ìàëüíûé ÿçûê. Ïóñòü ST — ìíîæåñòâî îáúåêòîâ òåîðåìû T (ïîñûëêè è çàêëþ÷å- íèå), S L — ìíîæåñòâî îáúåêòîâ (ôîðìóë) ÿçûêà L, DT — òåðìèíîëîãè÷åñêèé ñëîâàðü ïîíÿòèé è îòíîøåíèé ïðåäìåòíîé îáëàñòè òåîðåìû T . Íåîáõîäèìî ïî- ñòðîèòü îòîáðàæåíèå� �: S ST D L T , êîòîðîå ïåðåâîäèò âåðáàëüíîå îïèñàíèå òåîðå- ìû T â åå ôîðìàëüíîå ïðåäñòàâëåíèå íåêîòîðîãî ÿçûêà L . Ýòî îòîáðàæåíèå ñòðîèòñÿ íà îñíîâå ñëîâàðÿ DT , êîòîðûé ïîçâîëÿåò îäíîçíà÷íî ïîíèìàòü è îáî- çíà÷àòü òåðìèíû äàííîé çàäà÷è. Ïðè ýòîì â êà÷åñòâå ÿçûêà L áóäåì èñïîëüçîâàòü ðàñøèðåííûé ÿçûê ëîãèêè ïðåäèêàòîâ. Òàêîå ðàñøèðåíèå îñóùåñòâëÿåòñÿ ïóòåì ïðèñîåäèíåíèÿ ê àëôàâèòó ÿçûêà ïðåäèêàòîâ ñïåöèàëüíûõ êîíñòàíò è ïðåäèêàòíûõ ñèìâîëîâ. Ñïåöèàëüíóþ êîí- ñòàíòó — íàçâàíèå òåðìà ëèíãâèñòè÷åñêîé ïåðåìåííîé îáîçíà÷èì ñòðî÷íîé áóê- âîé ñ òèëüäîé, à ñïåöèàëüíûé ïðåäèêàòíûé ñèìâîë — íàçâàíèå íå÷åòêîãî îòíî- øåíèÿ îáîçíà÷èì ïðîïèñíîé áóêâîé ñ òèëüäîé. ×åòêèå âûñêàçûâàíèÿ ïðåîáðàçóþòñÿ â ëîãè÷åñêèå ôîðìóëû ñòàíäàðòíûì ñïîñîáîì, ïîýòîìó ñîîòâåòñòâóþùèå ìåõàíèçìû çäåñü îïóñêàåì. Íå÷åòêèå âû- ñêàçûâàíèÿ ïåðâîãî òèïà ïðåäñòàâèì ïðåäèêàòîì P a(~ ) , â êîòîðîì ïðåäèêàòíûé ñèìâîë P îáîçíà÷àåò íàçâàíèå ëèíãâèñòè÷åñêîé ïåðåìåííîé, à òåðì ~a — åå çíà- ÷åíèå. Ýòî çíà÷åíèå ÿâëÿåòñÿ íå÷åòêîé ïåðåìåííîé, äëÿ êîòîðîé ñòðîèòñÿ ôóíê- ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 49 öèÿ ïðèíàäëåæíîñòè (ÔÏ) � ~ ( )a x (x X , ãäå X — áàçîâîå ìíîæåñòâî ïåðåìåí- íîé ~a ). Çàòåì ôîðìèðóåòñÿ ñåìàíòè÷åñêèé èíäåêñ ëèòåðû P a(~ ) . Íàïðèìåð, âû- ñêàçûâàíèå «ìóæ÷èíà ìîëîäîãî âîçðàñòà» ìîæíî ïðåäñòàâèòü ïðåäèêàòîì P a(~ ) , ãäå P� «âîçðàñò ìóæ÷èíû», à ~a� «ìîëîäîé». Íå÷åòêèå âûñêàçûâàíèÿ âòîðîãî òèïà ýêñïëèöèðóþòñÿ ïðåäèêàòàìè ~ ( , )R x y1 1 è ~ ( , )R x y , ãäå ~ R — íàçâàíèå íå÷åòêîãî îòíîøåíèÿ; x X1 , y Y1 — ïðåäìåòíûå êîíñòàíòû; x y, — ïðåäìåòíûå ïåðåìåííûå, îïðåäåëåííûå íà ìíî- æåñòâàõ X è Y . Ïðè ýòîì ïðåäèêàòû ~ ( , )R x y1 1 îïèñûâàþò ôàêòû è çàêëþ÷åíèå òå- îðåìû, à ïðåäèêàòû ~ ( , )R x y âõîäÿò â îïèñàíèÿ óñëîâèé è çàêëþ÷åíèé ïðàâèë âû- âîäà.  ýòîì ñëó÷àå äëÿ íå÷åòêîãî îòíîøåíèÿ ~ R ñòðîèòñÿ ôóíêöèÿ ïðèíàäëåæíî- ñòè � ~ ( , ) R x y (( , ) )x y X Y � . Íàïðèìåð, âûñêàçûâàíèå «x çíà÷èòåëüíî áîëüøå y» ìîæíî ïðåäñòàâèòü ïðåäèêàòîì ~ ( , )R x y , ãäå ~ R� «çíà÷èòåëüíî áîëüøå», à x y R, . Èñõîäÿ èç ïðàêòèêè âîçìîæíû ñèòóàöèè, êîãäà ïðåäñòàâèòü ôàêòû áèíàðíûìè íå÷åòêèìè ïðåäèêàòàìè çàòðóäíèòåëüíî, à â íåêîòîðûõ ñëó÷àÿõ íåâîçìîæíî (íàïðè- ìåð, êîãäà ìåõàíèçìû äîêàçàòåëüñòâà òåîðåì âñòðîåíû â ñèñòåìó àâòîìàòè÷åñêîãî óïðàâëåíèÿ è â êà÷åñòâå ôàêòîâ âûñòóïàþò òåëåìåòðè÷åñêèå äàííûå). Ïîýòîìó â òà- êèõ ñèòóàöèÿõ ïðåäëàãàåòñÿ ôîðìèðîâàòü íå÷åòêèå ïðåäèêàòû ïðîöåäóðíî. À èìåí- íî, ïðåäñòàâëåíèå íå÷åòêîãî îòíîøåíèÿ ïðåäèêàòîì ~ ( , )R x y ïîçâîëÿåò óòâåðæäàòü: åñëè x Xi , y Yj , òî ýëåìåíòû xi è y j íàõîäÿòñÿ â îòíîøåíèè ~ R , ò.å. åñëè èìåþò ìåñòî ôàêòû Q xi( )� «x Xi » è S y j( )� « y Yj », òî èìååò ìåñòî è ôàêò ~ ( , )R x yi j . Ïðè ýòîì ïðåäèêàòû Q xi( ) è S y j( ) áóäåì íàçûâàòü àôôèëèðîâàííûìè ñ ïðåäèêàòîì ~ ( , )R x y è îáîçíà÷àòü èõ â ñåìàíòè÷åñêîì èíäåêñå ëèòåðû ~ ( , )R x y . È, íàêîíåö, ïðàâèëà íå÷åòêèõ ïðîäóêöèé ïðåäñòàâëÿþòñÿ èìïëèêàöèÿìè âèäà A B� ( )� , àíòåöåäåíòû è êîíñåêâåíòû êîòîðûõ ôîðìàëèçóþòñÿ âûøå îïèñàííûì ñïîñîáîì. Îïåðàöèè ïðèâåäåíèÿ ôîðìóë â ïðåäâàðåííóþ íîðìàëüíóþ ôîðìó è ñêóëå- ìåçàöèè àíàëîãè÷íû îïåðàöèÿì â ëîãèêå ïðåäèêàòîâ, ïîýòîìó äëÿ èõ ðåàëèçàöèè ìîãóò áûòü èñïîëüçîâàíû ñòàíäàðòíûå àëãîðèòìû.  çàêëþ÷åíèå ñäåëàåì íåñêîëüêî çàìå÷àíèé. Ìû ðàññìîòðåëè âîïðîñû ïðåîá- ðàçîâàíèÿ ýëåìåíòîâ òåîðåìû â êëàóçàëüíûé âèä êàê òàêîâûå, ò.å. áåçîòíîñèòåëüíî ê åå ïðàêòè÷åñêîìó ïðèìåíåíèþ. Ïîñêîëüêó áîëüøèíñòâî çàäà÷ ïðàêòèêè ðàçðàáà- òûâàþòñÿ ñ ó÷åòîì èõ ìíîãîêðàòíîãî àâòîìàòèçèðîâàííîãî ðåøåíèÿ, öåëåñîîáðàçíî ïðàâèëà íå÷åòêèõ ïðîäóêöèé, ñåìàíòè÷åñêèå èíäåêñû èõ ëèòåð è îïèñàíèÿ âñåõ ëèíãâèñòè÷åñêèõ è íå÷åòêèõ ïåðåìåííûõ, èñïîëüçóåìûõ â ýòèõ ïðàâèëàõ, õðàíèòü â áàçå çíàíèé. Òîãäà ïðîöåññ äîêàçàòåëüñòâà òåîðåìû áóäåò âêëþ÷àòü äâà ýòàïà: — ôîðìèðîâàíèå òåîðåìû, ò.å. àêñèîìàòèçàöèÿ èñõîäíûõ äàííûõ (ôàêòîâ) è çà- êëþ÷åíèå òåîðåìû, à òàêæå çàãðóçêà èç áàçû çíàíèé ñîîòâåòñòâóþùèõ ïðàâèë è ÔÏ; — íåïîñðåäñòâåííî äîêàçàòåëüñòâî òåîðåìû. ÑÒÐÓÊÒÓÐÍÀß ÐÅÇÎËÞÖÈß Ââåäåì ïîíÿòèå ñòðóêòóðíîé ðåçîëþöèè. Ñòðóêòóðíàÿ ðåçîëþöèÿ (S-ðåçîëþ- öèÿ) — ýòî óòî÷íåíèå åäèíè÷íîé ðåçîëþöèè, èñïîëüçóþùåå ïîíÿòèå, àíàëî- ãè÷íîå ïîíÿòèþ óïîðÿäî÷åííîãî äèçúþíêòà. S-ðåçîëþöèÿ îñíîâàíà íà ñåìàí- òè÷åñêèõ èíäåêñàõ ëèòåð è èõ ñõîäñòâå. Ñåìàíòè÷åñêèå èíäåêñû ÿâëÿþòñÿ êëþ÷åâûì ïîíÿòèåì S-ðåçîëþöèè è èñïîëüçóþòñÿ äëÿ óïîðÿäî÷åíèÿ ëèòåð â äèçúþíêòàõ è èõ èäåíòèôèêàöèè. Ïðè ýòîì S-ðåçîëþöèþ ðàçðåøàåòñÿ ïðè- ìåíÿòü ê ïîñûëêàì, îäíà è òîëüêî îäíà èç êîòîðûõ ÿâëÿåòñÿ äèçúþíòêîì-ôàê- òîì, à â äèçúþíêòàõ-ïðàâèëàõ ðàçðåøåíî îòðåçàòü òîëüêî ëèòåðû-àíòåöåäåíòû. À ñõîäñòâî çàêëþ÷àåòñÿ â ïîèñêå ëèòåðû-ôàêòà, êîòîðàÿ ëèáî ïî÷òè äîïîëíÿåò ëè- òåðó â äðóãîé ïîñûëêå, ëèáî ìåæäó ýòèìè ëèòåðàìè ìîæíî óñòàíîâèòü îòíîøåíèå ñõîäñòâà, èñïîëüçóåìîå ïðè ôàççèôèêàöèè â ñèñòåìàõ íå÷åòêîãî âûâîäà. Ïðåæäå ÷åì äàòü ôîðìàëüíîå îïðåäåëåíèå S-ðåçîëþöèè, ðàññìîòðèì ñëåäóþùèé ïðèìåð. 50 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 Ïóñòü òåîðåìà ïðåäñòàâëåíà ñòðóêòóðèðîâàííûì ìíîæåñòâîì äèçúþíêòîâ, êîòîðûå ÿâëÿþòñÿ ïðîïîçèöèîíàëüíûìè ôîðìóëàìè: C A1 0 8: . ô, C B2 0 2: . � ô, C A Ba 3 07: ( . )� � ê , C B Da 4 09: ( . )� � ê , C A5 : � ç, ãäå C C1 2, — äèçúþíêòû-ôàêòû; C C3 4, — äèçúþíêòû-ïðàâèëà A B� �( . )� 0 7 è B D� ( . )� � 0 9 ; C5 — îòðèöàíèå çàêëþ÷åíèÿ òåîðåìû. Äëÿ íàãëÿäíîñòè â ýòèõ äèçúþíêòàõ íèæíèå èíäåêñû ÿâëÿþòñÿ çíà÷åíèÿìè èñòèííîñòè ëèòåð, âåðõíèå — ïðèíàäëåæíîñòü ëèòåð ê ýëåìåíòàì òåîðåìû, à ÷èñëà â ñêîáêàõ — âåñîâûå êîýôôèöèåíòû ïðàâèë.  äàííîì ñëó÷àå S-ðåçîëþöèÿ íå ïðèìåíèìà ê äèçúþíêòàì C2 , C3 è C3 , C4 . Ïðè ýòîì ðåçîëüâåíòîé äèçúþíêòîâ C1 è C3 åñòü äèçúþíêò B ê , à ðåçîëüâåíòîé äèçúþíêòîâ C1 è C5 — ïóñòîé äèçúþíêò. Òåïåðü äàäèì ôîðìàëüíîå îïðåäåëåíèå S-ðåçîëþöèè. Ñëåäóåò ðàçëè÷àòü ÷åòêèå è íå÷åòêèå ëèòåðû. ×åòêàÿ ëèòåðà – ýòî ëèòåðà ëîãèêè ïðåäèêàòîâ, à íå- ÷åòêàÿ ëèòåðà îïðåäåëÿåò ëèáî íå÷åòêîå îòíîøåíèå, ëèáî åå òåðìîì ÿâëÿåòñÿ íå÷åòêàÿ ïåðåìåííàÿ. Ïóñòü C Lr1 11 � ô — äèçúþíêò-ôàêò, à Ñ2 — äèçúþíêò-ïðàâèëî. Åñëè ëèòåðû r L 1 1 ô è L Ña 2 2 — ÷åòêèå è r L 1 1 ô, �La 2 èìåþò íàèáîëåå îáùèé óíèôèêàòîð � , òî äèçúþíêò ( )Ñ Lr a 2 1 21 � �� � íàçîâåì S-ðåçîëüâåíòîé C1 è Ñ2 . Ïðåäïîëîæèì, ÷òî ëèòåðû r L 1 1 ô è L Ña 2 2 — íå÷åòêèå. Ðàññìîòðèì äâà ñëó÷àÿ. Ñëó÷àé 1. Ïóñòü ýòè ëèòåðû ÿâëÿþòñÿ óíàðíûìè ïðåäèêàòàìè: r L 1 1 ô � � r P a 1 (~ )* è L P aa 2 �� (~ ) , ãäå P — íàçâàíèå ëèíãâèñòè÷åñêîé ïåðåìåííîé, ~ *a è ~a — åå çíà÷åíèÿ (íå÷åòêèå ïåðåìåííûå), çàäàííûå íå÷åòêèìè ìíîæåñòâàìè, êî- òîðûå îïðåäåëåíû íà îäíîì è òîì æå áàçîâîì ìíîæåñòâå X . Ïóñòü òàêæå �1 ( ),x x X , è �2 ( ),x x X , — ôóíêöèè ïðèíàäëåæíîñòè íå÷åòêèõ ìíîæåñòâ ~ *a è ~a ñîîòâåòñòâåííî. Ââåäåì ìåðó � [ , ]0 1 ñõîäñòâà ìåæäó íå÷åòêèìè ìíîæåñòâà- ìè ~ *a è ~a . Òîãäà S-ðåçîëüâåíòîé C1 è Ñ2 áóäåò äèçúþíêò ( (~ ))C P ar2 1� �� , ãäå r r� �� 1 — èñòèííîñòü âûñêàçûâàíèÿ P a(~ ) ïðè íàëè÷èè âûñêàçûâàíèÿ P a(~ )* . Êîãäà ïðåäúÿâëÿþòñÿ òðåáîâàíèÿ ê óðîâíþ èñòèííîñòè çàêëþ÷åíèÿ òåîðåìû, ìîæíî çàäàòü ïîðîãîâîå çíà÷åíèå � è ðàçðåøàòü S-ðåçîëþöèþ òîãäà è òîëüêî òîãäà, êîãäà çíà÷åíèå � áîëüøå ýòîãî ïîðîãà.  íàñòîÿùåå âðåìÿ ñóùåñòâóåò ìíîãî ìåòîäîâ, ïîçâîëÿþùèõ îïðåäåëèòü ìåðó ñõîäñòâà (ðàçëè÷èÿ) ìåæäó äâóìÿ íå÷åòêèìè ìíîæåñòâàìè [18]. Ïðîâåäåí- íûé â äàííîé ðàáîòå àíàëèç ðàçëè÷íûõ ìåð ñõîäñòâà ïîêàçûâàåò, ÷òî íåâîçìîæ- íî âûäåëèòü åäèíóþ êîíêðåòíóþ ìåðó ïîäîáèÿ, êîòîðàÿ îäèíàêîâî õîðîøî «ïîäõîäèò» äëÿ ëþáîé ïðîáëåìû. Ñ ó÷åòîì ýòîãî â [19] ïðåäëîæåí ïîêàçàòåëü ïîäîáèÿ, îñíîâàííûé íà ïàðàìåòðè÷åñêîé ìåòðèêå Ìèíêîâñêîãî ( p-ìåòðèêå). Âàðüèðóÿ ïàðàìåòðîì p, ìîæíî ïîëó÷èòü ðàçëè÷íûå ôóíêöèè ðàññòîÿíèÿ â åâ- êëèäîâîì ïðîñòðàíñòâå, à ñëåäîâàòåëüíî, è ðàçëè÷íûå ìåðû ñõîäñòâà, îðèåíòè- ðîâàííûå íà êîíêðåòíóþ ïðîáëåìó. Ýòî ïîçâîëÿåò îáåñïå÷èòü ãèáêîñòü òàêîé ìåðû è â íåêîòîðîì ñìûñëå åå óíèâåðñàëüíîñòü. Ïóñòü ~ ( )A x è ~ ( )B x , x X , — íå÷åòêèå ìíîæåñòâà. Òîãäà ïîêàçàòåëü ïîäîáèÿ îïðåäåëÿåòñÿ ôîðìóëîé � �S A B n x x A i B i p i n p ( ~ , ~ ) ( ) ( )~ ~� � � � � � � � � � �1 1 1 1 � � , ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 51 ãäå n — ìîùíîñòü ìíîæåñòâà X è p � 1 — ïàðàìåòð (âåùåñòâåííîå ÷èñëî), ïðè÷åì ÷åì áîëüøå p , òåì áîëüøå ìåðà ïîäîáèÿ. Ýòîò ïàðàìåòð îïðåäåëÿåòñÿ äëÿ êàæäîé òåîðåìû. Ñ ó÷åòîì ñêàçàííîãî òàêîé ïîêàçàòåëü ïîäîáèÿ áóäåì èñïîëüçîâàòü â êà÷åñòâå ìåðû ñõîäñòâà íå÷åòêèõ ìíîæåñòâ. Ïóñòü òåïåðü ~ *a x X� 1 .  ýòîì ñëó÷àå ìåðîé ñõîäñòâà ïðåäèêàòîâ P a(~ ) è P a(~ )* ÿâëÿåòñÿ ñòåïåíü ñîîòâåòñòâèÿ (ïðèíàäëåæíîñòè) ýëåìåíòà x1 íå÷åòêîìó ìíîæåñòâó ~a , ò.å. � �� 2 1( )x . Ñëó÷àé 2. Ïóñòü ëèòåðû r L 1 1 ô è L Ña 2 2 ÿâëÿþòñÿ áèíàðíûìè ïðåäèêàòàìè: r rL R x y 1 11 1 1 ô � ~ ( , ) , L R x ya 2 �� ~ ( ) , ãäå ~ R — íå÷åòêîå îòíîøåíèå ìåæäó ïðåäìåò- íûìè ïåðåìåííûìè x y, , êîòîðûå îïðåäåëåíû íà ìíîæåñòâàõ èíäèâèäíûõ êîí- ñòàíò X è Y , à � ~ ( , ) R x y — ôóíêöèÿ ïðèíàäëåæíîñòè íå÷åòêîãî îòíîøåíèÿ ~ R .  ýòîì ñëó÷àå ìåðîé ñõîäñòâà ýòèõ ïðåäèêàòîâ ÿâëÿåòñÿ ñòåïåíü � �� ~ ( , ) R x y1 1 ñîîòâåòñòâèÿ (ïðèíàäëåæíîñòè) ïàðû ( , )x y1 1 íå÷åòêîìó îòíîøåíèþ ~ R , à S-ðåçîëüâåíòîé áóäåò äèçúþíêò ( ~ ( ) )C R x yr2 1� �� �� , ãäå � � { / , / }x x y y1 1 , r r� �� 1.  ñëó÷àå îòñóòñòâèÿ ôàêòà ~ ( , )R x y1 1 âûïîëíÿåòñÿ ïîèñê ëèòåð-ôàêòîâ, àô- ôèëèðîâàííûõ ñ ïðåäèêàòîì ~ ( , )R x y . Ïóñòü r Q x 1 1 ô ( ) è r S y 2 1 ô ( ) ÿâëÿþòñÿ òà- êèìè ëèòåðàìè.  ýòîì ñëó÷àå ôîðìèðóåòñÿ ôàêò r R x y ~ ( , )1 1 , ãäå r r r� min( , )1 2 , è àíàëîãè÷íî âû÷èñëÿåòñÿ S-ðåçîëüâåíòà. Òåïåðü ðàññìîòðèì ñëó÷àé, êîãäà C Lr1 11 � ô — äèçúþíêò-ôàêò, à C L2 2 � ç — äèçúþíêò-çàêëþ÷åíèå. Åñëè ëèòåðû r L 1 1 ô è L 2 ç ÷åòêèå è êîíòðàðíûå, òî S-ðåçîëü- âåíòîé C1 è Ñ2 áóäåò ïóñòîé äèçúþíêò � . Ïðè ýòîì èñòèííîñòü çàêëþ÷åíèÿ L 2 ç áóäåò ðàâíà r1 . Åñëè äèçúþíêòû C1 è C2 íå÷åòêèå è ïî÷òè êîìïëåìåíòàðíûå, òî S-ðåçîëüâåíòîé ýòèõ äèçúþíêòîâ òàêæå áóäåò ïóñòîé äèçúþíêò, à èñòèííîñòü çà- êëþ÷åíèÿ L 2 ç áóäåò âû÷èñëåíà ñîãëàñíî ñëó÷àÿì 1 è 2. Ìû ðàññìîòðåëè ðàçëè÷íûå âàðèàíòû âîçìîæíîãî ïðèìåíåíèÿ S-ðåçîëþ- öèè. Òåïåðü ðàññìîòðèì ñëó÷àé, êîãäà S-ðåçîëüâåíòîé ÿâëÿåòñÿ çàêëþ÷åíèå íåêîòîðîãî ïðàâèëà. Ïóñòü â ïðîöåññå âûâîäà â êà÷åñòâå S-ðåçîëüâåíòû ïîëó÷åíà ëèòåðà-êîíñåê- âåíò Ln ê ïðàâèëà � �� �L La a 1 2 ,..., �� ��L L n a n1 ê , ÷òî ðàâíîñèëüíî «ñðàáàòûâàíèþ» ïðîäóêöèîííîãî ïðàâèëà ( , , ..., ) ( )L L L L n n1 2 1� � � .  ýòîì ñëó÷àå ñòåïåíü èñ- òèííîñòè ëèòåðû Ln ê âû÷èñëÿåòñÿ ñîãëàñíî (4): r ri� �min (( max ), )1 � , (5) ãäå ri — èñòèííîñòü îòðåçàííîé ëèòåðû �Li a àíòåöåäåíòà äàííîãî ïðàâèëà. Åñëè ëèòåðà-êîíñåêâåíò Ln ê ýêñïëèöèðóåò íå÷åòêîå âûñêàçûâàíèå, òî âûïîë- íÿåòñÿ êîððåêöèÿ ÔÏ ñîîòâåòñòâóþùåé íå÷åòêîé ïåðåìåííîé ïóòåì åå ðåäóêöèè (îòñå÷åíèÿ). Äëÿ ýòîãî ìîæíî èñïîëüçîâàòü îäèí èç ìåòîäîâ àêòèâèçàöèè íå÷åò- êîãî âûâîäà, íàïðèìåð êëàññè÷åñêóþ min–àêòèâèçàöèþ: � �� �( ) min ( , ( ))x r x , ãäå �� ( )x , �( )x — ñîîòâåòñòâåííî óñå÷åííàÿ è èñõîäíàÿ ÔÏ íå÷åòêîé ïåðå- ìåííîé çàêëþ÷åíèÿ ïðàâèëà. Çàòåì ýòà ëèòåðà ïåðåâîäèòñÿ â ðàçðÿä ôàêòîâ Ln ô. Ïðè ýòîì åñëè óæå ñóùåñòâóåò ôàêò q nLô òàêîé, ÷òî q r� , òî ôàêò r nLô óäàëÿåòñÿ, èíà÷å óäàëÿåòñÿ ôàêò q nLô. 52 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 Ïóñòü D — ìíîæåñòâî äèçúþíêòîâ. Ïîä S-âûâîäîì áóäåì ïîíèìàòü âûâîä, â êîòîðîì êàæäûé äèçúþíêò ÿâëÿåòñÿ ëèáî ÷ëåíîì D, ëèáî S-ðåçîëüâåíòîé. Äà- ëåå, ïóñòü äàíà òåîðåìà T : (F1, F2 , …, F Gn )� . Ïóñòü òàêæå D — ìíîæåñòâî äèçúþíêòîâ, êîòîðûå ÿâëÿþòñÿ êîíúþíêòèâíîé íîðìàëüíîé ôîðìîé ôîðìóë F1, F2 , …, Fn , à G *— äèçúþíêò-çàêëþ÷åíèå òåîðåìû. Òîãäà åñëè ñïðàâåäëèâà òåî- ðåìà T , òî ñóùåñòâóåò S-âûâîä ïóñòîãî äèçúþíêòà èç ìíîæåñòâà ( )*D G � . Âûâîä çàêëþ÷åíèÿ G ýòîé òåîðåìû èìååò äåäóêòèâíûé õàðàêòåð è åãî ìîæ- íî ïðåäñòàâèòü ñëåäóþùåé ñèñòåìîé ïðàâèë ïðîäóêöèé: ( ( .. .F F1 2� � ... ( ( ))) )� � ��F F Gn n1 � . Òàê êàê ðåàëèçàöèÿ ïðàâèë ïðîäóêöèé îñóùåñòâëÿ- åòñÿ S-ðåçîëþöèåé, òî, ïðèìåíÿÿ åå, ïîëó÷èì äèçúþíêò G *â êà÷åñòâå S-ðåçîëü- âåíòû. Ñëåäîâàòåëüíî, ( ) |*D G � �� � , ò.å. ñóùåñòâóåò S-âûâîä ïóñòîãî äèçúþíêòà èç ìíîæåñòâà ( )*D G � . ÑÒÐÀÒÅÃÈß ÓÏÐÀÂËÅÍÈß ÂÛÂÎÄÎÌ Èñïîëüçîâàíèå ñåìàíòè÷åñêèõ èíäåêñîâ ëèòåð ïîçâîëÿåò â ïðîöåññå äîêàçà- òåëüñòâà ïðèìåíÿòü òàêèå ýâðèñòèêè, êàê ïðÿìîé èëè îáðàòíûé âûâîä. Ïðÿìîé ëîãè÷åñêèé âûâîä ïðåäñòàâëÿåò ñîáîé öåïî÷êó ðàññóæäåíèé, êîòî- ðàÿ âåäåò îò èñõîäíûõ àêñèîì ê öåëåâîìó âûðàæåíèþ. Îñíîâíîé íåäîñòàòîê ïðÿìîãî ìåòîäà ñîñòîèò â åãî íåíàïðàâëåííîñòè, ÷òî ïðèâîäèò ê ðîñòó ïðîìåæó- òî÷íûõ çàêëþ÷åíèé, íå ñâÿçàííûõ ñ öåëåâûì óòâåðæäåíèåì. Îäíàêî â ñëó÷àÿõ, êîãäà íåîáõîäèìî ïîëó÷àòü çàêëþ÷åíèÿ íà îñíîâå ïîñòóïàþùèõ ðåçóëüòàòîâ âîñïðèÿòèÿ áåç ó÷åòà êàêîãî-ëèáî êîíêðåòíîãî çàïðîñà, ïðÿìàÿ öåïî÷êà ðàññóæäåíèé ÿâëÿåòñÿ åäèíñòâåííî âîçìîæíûì ìåòîäîì ëîãè÷åñêîãî âûâîä. Ïðè îáðàòíîì âûâîäå ïîèñê äîêàçàòåëüñòâà íà÷èíàåòñÿ ñ öåëåâîãî óòâåðæ- äåíèÿ. Îáðàòíûé âûâîä ÿâëÿåòñÿ íàïðàâëåííûì. Êàæäûé øàã âûâîäà â ýòîì ñëó- ÷àå ñâÿçàí âñåãäà ñ èñõîäíîé öåëüþ. Äëÿ îáðàòíûõ âûâîäîâ õàðàêòåðíà òåíäåí- öèÿ èñêëþ÷åíèÿ èç ðàññìîòðåíèÿ ïðàâèë, íå èìåþùèõ ïðÿìîãî îòíîøåíèÿ ê çà- äàííîé öåëè. Ïîýòîìó èñïîëüçîâàíèå îáðàòíîé öåïî÷êè ðàññóæäåíèé ïðåäïî÷òèòåëüíåå.  êà÷åñòâå èëëþñòðàöèè ïðèâåäåì îäèí èç âîçìîæíûõ àëãîðèòìîâ äîêàçàòåëüñòâà òåîðåìû îáðàòíûì ìåòîäîì. Ïóñòü òåîðåìà T ïðåäñòàâëåíà ñëåäóþùèì ñòðóêòóðèðîâàííûì ìíîæåñòâîì äèçúþíêòîâ: C1: M ô(a), C2 : rC bô ( ~ ) , C3 : Dô ( )�1 , C4 : � �� �M x D e L xa a( ) (~) ( )( )ê �1 , C5 : � �� �� �M x L x C g A xa a a( ) ( ) ( ~) ( )( )ê �2 , C6 : �A aç ( ) . Çäåñü äèçúþíêòû C C1 3! — ôàêòû; C C4 5, — ïðàâèëà; C6 — çàêëþ÷åíèå òåîðåìû. Ïóñòü òàêæå � ~ ( )g u , � ~ ( ) b u , � �~ ( )e — ôóíêöèè ïðèíàäëåæíîñòè íå- ÷åòêèõ ïåðåìåííûõ ~, ~ , ~g b e . Ïðè÷åì íå÷åòêèå ïåðåìåííûå ~g è ~ b çàäàíû íå÷åò- êèìè ìíîæåñòâàìè è îïðåäåëåíû íà îäíîì è òîì æå óíèâåðñàëüíîì ìíîæåñò- âå U u um� ( , , )1 � , à ïåðåìåííàÿ ~e çàäàíà íà óíèâåðñàëüíîì ìíîæåñòâå V n� ( , ..., )� �1 . Äàëåå, ïóñòü M — ìíîæåñòâî ôàêòîâ, F — ìíîæåñòâî ïðàâèë âûâîäà, G A0 �� ç — èñõîäíàÿ öåëåâàÿ ôîðìóëà (öåëü). Òîãäà òåîðåìó T ìîæíî ïðåäñòà- âèòü êîðòåæåì� �M F G, , 0 è åå äîêàçàòåëüñòâî îïèñàòü ñëåäóþùèì àëãîðèòìîì. Øàã 1. Ïðîâåðèòü íà ïðîòèâîðå÷èâîñòü ìíîæåñòâî {M G 0} . Åñëè { }|M G �� �0 , òî çàâåðøèòü ðàáîòó; òåîðåìà T äîêàçàíà.  ïðîòèâíîì ñëó÷àå ñëåäóþùèé øàã. ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 53 Øàã 2. Ïîìåñòèòü öåëü G0 â ñïèñîê LIST = (G0) è íàéòè ïðàâèëî, êîíñåê- âåíò êîòîðîãî ïîçâîëèë áû äîñòè÷ü öåëü G0 . Åñëè ïîäõîäÿùåãî ïðàâèëà íåò — çàâåðøèòü ïðîöåññ; òåîðåìà íå èìååò ðåøåíèÿ.  äàííîì ñëó÷àå òàêèì ïðàâèëîì ÿâëÿåòñÿ äèçúþíêò C5 . Åãî àíòåöåäåíò çàäàòü â êà÷åñòâå íîâîé öåëè G M a L a C ga a a 1 �� �� ��( ) ( ) (~ ) è ïîìåñòèòü åå â ñïèñîê LIST � ( ,G G1 0). Øàã 3. Ïðèìåíèòü S-ðåçîëþöèþ ê C1 è G1 : G L a C ga a 7 : ( ) (~ )� �� — S-ðåçîëüâåíòà. Øàã 4. Ïðèìåíèòü S-ðåçîëþöèþ ê C2 è C7 : C L aa 8 : ( )� — S-påçîëüâåíòà. Øàã 5. Òàê êàê íåò ôàêòà, êîòîðûé ìîã áû ðåçîëüâèðîâàòü ñ C8 , òî èñïîëü- çîâàòü àíòåöåäåíò ïðàâèëà C4 â êà÷åñòâå íîâîé öåëè G M a D ea a 2 �� ��( ) (~ ) è ïî- ìåñòèòü åå â ñïèñîê LIST = (G G G2 1 0, , ). Øàã 6. Ïðèìåíèòü S-ðåçîëþöèþ ê C1 è G2 : C D ea 9 : (~ )� — S-ðåçîëüâåíòà. Øàã 7. Ïðèìåíèòü S-ðåçîëþöèþ ê C3 è C9 : C10 : � — S-ðåçîëüâåíòà. Óäàëèòü G2 èç ñïèñêà LIST. Øàã 8. Âû÷èñëèòü ñîãëàñíî (5) çíà÷åíèå r èñòèííîñòè êîíñåêâåíòà L aê ( ) ïðàâèëà C4 è ïåðåâåñòè åãî â ðàçðÿä ôàêòîâ.  ðåçóëüòàòå ïîëó÷èì ëè- òåðó C L ar11: ( )ô . Øàã 9. Ïðèìåíèòü S-ðåçîëþöèþ ê C8 è C11: C12 : � — S-ðåçîëüâåíòà. Óäàëèòü G1 èç ñïèñêà LIST. Øàã 10. Âû÷èñëèòü àíàëîãè÷íî çíà÷åíèå r èñòèííîñòè êîíñåêâåíòà A aê ( ) ïðàâèëà C5 è ïåðåâåñòè åãî â ðàçðÿä ôàêòîâ.  ðåçóëüòàòå ïîëó÷èì ëèòåðó C A ar13 : ( )ô . Øàã 11. Ïðèìåíèòü S-ðåçîëþöèþ ê C13 è C6 : C14 : � — S-ðåçîëüâåíòà. Òåîðåìà äîêàçàíà ñ ðåçóëüòèðóþùèì ïðàâèëîì C5 , ïðè ýòîì èñòèííîñòü åå çàêëþ÷åíèÿ ðàâíà r . Àðãóìåíòàöèåé ýòîãî çàêëþ÷åíèÿ ÿâëÿåòñÿ ñëåäóþùàÿ öåïî÷êà ðàññóæäåíèé: èñõîäíûå ôàêòû � ïðàâèëî C4 � ïðàâèëî C5 � � çàêëþ÷åíèå òåîðåìû. Øàã 12. Åñëè íåò äðóãèõ ïîäõîäÿùèõ ïðàâèë, êîíñåêâåíòû êîòîðûõ ïîçâî- ëèëè áû äîñòè÷ü öåëü G0 , òî äîêàçàòåëüñòâî çàâåðøèòü.  ïðîòèâíîì ñëó÷àå âû- áðàòü ïðàâèëî, àíòåöåäåíò êîòîðîãî èìååò íàèìåíüøå ëèòåð, è ïðîöåññ ïîâòî- ðèòü. Åñëè ïðàâèëà èìåþò àíòåöåäåíòû îäèíàêîâîé äëèíû, òî äîêàçàòåëüñòâî ïðîâîäèòñÿ äëÿ êàæäîãî èç íèõ.  ýòîì ñëó÷àå èñòèííîñòü çàêëþ÷åíèÿ òåîðåìû áóäåò ìàêñèìàëüíîé ïðè âñåõ ðåçóëüòèðóþùèõ ïðàâèëàõ, à àðãóìåíòàöèÿ ýòîãî çàêëþ÷åíèÿ áóäåò àðãóìåíòàöèåé äîêàçàòåëüñòâà òåîðåìû. Ðàññìîòðåííûé àëãîðèòì âêëþ÷àåò äâà ýòàïà. Íà ïåðâîì ýòàïå (øàãè 1–8) îïðåäåëÿåòñÿ öåïî÷êà ðàññóæäåíèé, âåäóùàÿ ê öåëè, à íà âòîðîì ýòàïå (øàãè 9–11) âû÷èñëÿåòñÿ èñòèííîñòü çàêëþ÷åíèé ïðàâèë òåîðåìû. ÎÑÎÁÅÍÍÎÑÒÈ ÏÐÅÄËÀÃÀÅÌÎÃÎ ÏÎÄÕÎÄÀ 1.  êëàññè÷åñêîé ñõåìå äîêàçàòåëüñòâà ðåçîëüâåíòû ïðèñîåäèíÿþòñÿ ê èñõîä- íîìó ìíîæåñòâó äèçúþíêòîâ, ÷òî ïðèâîäèò ê åãî óâåëè÷åíèþ, à ñîîòâåòñòâåííî 54 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 è ê ïîòåðè ýôôåêòèâíîñòè. Ïðèìåíÿÿ S-ðåçîëþöèþ, ïîëó÷àåì â êà÷åñòâå ðå- çîëüâåíòû óêîðî÷åííóþ íååäèíè÷íóþ ïîñûëêó. Ïîñêîëüêó ñòàòóñ îòðåçàííîé ëèòåðû ôèêñèðóåòñÿ â åå ñåìàíòè÷åñêîì èíäåêñå, ôàêòè÷åñêè íåò íåîáõîäèìî- ñòè ýòó ëèòåðó îòðåçàòü, à ðåçîëüâåíòó ïðèñîåäèíÿòü ê òåêóùåìó ìíîæåñòâó. 2. Ïðèìåíåíèå S-ðåçîëþöèè ïîçâîëÿåò áëîêèðîâàòü áåñêîíå÷íûå âåòâè ïðî- öåññà äîêàçàòåëüñòâà. Íàïðèìåð, ïóñòü äàíî ìíîæåñòâî äèçúþíêòîâ: 1) �P a( ) , 2) � �P f f x P x( ( ( ))) ( ) . Ïðèìåíÿÿ ðåçîëþöèþ ê ýòèì äèçúþíêòàì, ìîæíî ïîëó÷èòü ñëåäóþùèé áåñ- êîíå÷íûé âûâîä: �P f f a( ( ( ))) , �P f f f f a( ( ( ( ( ))))) , … Òåïåðü ïðåäñòàâèì ýòî ìíîæåñòâî â ñòðóêòóðèðîâàííîì âèäå: 3) �P aô ( ) , 4) � �P f f x P xa ( ( ( ))) ( )ê .  ýòîì ñëó÷àå S-ðåçîëþöèÿ ê òàêèì äèçúþíêòàì íå ïðèìåíèìà ïî îïðåäåëåíèþ. 3. Ïðèìåíåíèå S-ðåçîëþöèè äàåò âîçìîæíîñòü îñóùåñòâëÿòü äîêàçàòåëüñòâî ïðè íàëè÷èè ïðîòèâîðå÷èâîé èíôîðìàöèè, êîòîðàÿ â êëàññè÷åñêîé ëîãèêå ïîçâî- ëÿåò èç óòâåðæäåíèÿ A è åãî îòðèöàíèÿ �A ïîëó÷èòü ëþáîå ñóæäåíèå. Íàïðèìåð, ïóñòü òåîðåìà ïðåäñòàâëåíà ìíîæåñòâîì äèçúþíêòîâ: 1) A, 2) �A, 3) � �B C, 4) �P. Çäåñü äèçúþíêòû 1) è 2) — ôàêòû, 3) — ïðàâèëî âûâîäà, 4) — îòðèöàíèå çà- êëþ÷åíèÿ òåîðåìû. Î÷åâèäíî, ÷òî â ýòîì ñëó÷àå óòâåðæäåíèå P âûâîäèìî. Ñ èñ- ïîëüçîâàíèåì S-ðåçîëþöèè ïîëó÷èòü òàêîé âûâîä íåâîçìîæíî, òàê êàê ê äèçú- þíêòàì-ôàêòàì S-ðåçîëþöèÿ òàêæå íå ïðèìåíèìà. 4. Ïðèìåíåíèå êîìïîçèöèîííîãî ïðàâèëà â êà÷åñòâå ïðàâèëà âûâîäà ïîçâî- ëÿåò ïåðåéòè îò «ìåëêèõ», íå åñòåñòâåííûõ äëÿ íàøåãî ïîíèìàíèÿ çàêëþ÷åíèé, êàêèìè ÿâëÿþòñÿ ðåçîëüâåíòû, ê ïðîäóêöèîííûì âûâîäàì, êîòîðûå áëèçêè ê ñî- äåðæàòåëüíîìó ðàññóæäåíèþ, ïðèâû÷íîìó äëÿ íàñ, è ïîçâîëÿþò èíòóèòèâíî ïðîñëåäèòü çà êàæäûì øàãîì ïðîöåññà äîêàçàòåëüñòâà. 5. Ââåäåíèå â àëôàâèò ÿçûêà ëîãèêè ïðåäèêàòîâ ñïåöèàëüíûõ êîíñòàíò, îáî- çíà÷àþùèõ òåðìû ëèíãâèñòè÷åñêèõ ïåðåìåííûõ, è ïðåäèêàòíûõ ñèìâîëîâ, êîòî- ðûå îòîáðàæàþò íå÷åòêèå îòíîøåíèÿ, ïîçâîëÿåò îñóùåñòâèòü äîêàçàòåëüñòâî êàê â íå÷åòêîé, òàê è â äâóçíà÷íîé ëîãèêå êàê åå ÷àñòíîì ñëó÷àå. Ïðè ýòîì äîïóñêà- åòñÿ èñïîëüçîâàíèå íå âïîëíå èñòèííîé àðãóìåíòàöèè. 6. Ïðåäëîæåííûå ìåõàíèçìû ïîçâîëÿþò ïîëó÷èòü áîëåå ïðîñòîé S-âûâîä. Àðãóìåíòàöèåé ýòîìó ìîãóò áûòü ñëåäóþùèå ðàññóæäåíèÿ. Èçâåñòíî, ÷òî ñëîæíîñòü âûâîäà îïðåäåëÿåòñÿ ÷èñëîì äèçúþíêòîâ â åãî ëè- íåéíîé çàïèñè. Ïóñòü D — ìíîæåñòâî äèçúþíêòîâ; �— ïóñòîé äèçúþíêò, ïðè- ÷åì D |�� � . Îáîçíà÷èì � âûâîä äèçúþíêòà � èç D, ãäå êàæäûé äèçúþíêò ÿâëÿ- åòñÿ ëèáî ÷ëåíîì D, ëèáî ðåçîëüâåíòîé. Ïîýòîìó ñëîæíîñòü âûâîäà � íåïîñðåä- ñòâåííî çàâèñèò îò êîëè÷åñòâà ðåçîëüâåíò. Ïðè ýòîì áóäåì ðàçëè÷àòü ðåçîëüâåíòû äâóõ âèäîâ: ïîëåçíûå ðåçîëüâåíòû, êîòîðûå ïîçâîëÿþò ïîëó÷èòü ïóñòîé äèçúþíêò, è áåñïîëåçíûå ðåçîëüâåíòû. Ïîëåçíûå ðåçîëüâåíòû ôîðìèðóþòñÿ, êîãäà îòðåçàåìûìè ÿâëÿþòñÿ ëèòåðà äèçúþíêòà-ôàêòà è ëèòåðà àíòåöåäåíòà äèçúþíêòà-ïðàâèëà. Ïðè ýòîì ÷åì ìåíüøå ëèòåð ñîäåðæàò ïîñûëêè, òåì ìåíüøå ïîëåçíûõ ðåçîëüâåíò.  ïðåäëàãàåìîì ïîä- õîäå ðåçîëüâåíòû âñåãäà ïîëåçíû, òàê êàê óêàçàííîå óñëîâèå ïîëó÷åíèÿ ðåçîëü- âåíò ÿâëÿåòñÿ óñëîâèåì ïðèìåíåíèÿ S-ðåçîëþöèè. Ñîêðàùåíèå òàêèõ ðåçîëüâåíò ìîæåò áûòü îáåñïå÷åíî çà ñ÷åò âûáîðà ïðàâèë ñ êîðîòêèìè àíòåöåäåíòàìè. Ãåíåðèðîâàíèå áåñïîëåçíûõ ðåçîëüâåíò âîçìîæíî â äâóõ ñëó÷àÿõ.  ïåðâîì ñëó÷àå îíè ìîãóò áûòü ïîëó÷åíû, êîãäà ðåçîëþöèÿ ïðèìåíÿåòñÿ ê ïîñûëêàì-ôàê- ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 55 òàì èëè ïîñûëêàì-ïðàâèëàì. Åñëè ìíîæåñòâî äèçúþíêòîâ íå ñòðóêòóðèðîâàíî, òî òàêîå ïðèìåíåíèå ðåçîëþöèè âîçìîæíî. Ïðèìåíåíèå S-ðåçîëþöèè ïîçâîëÿåò çà- áëîêèðîâàòü çàâåäîìî íåïåðñïåêòèâíûå ïîñûëêè è òàêèì îáðàçîì ñîêðàòèòü ïðî- ñòðàíñòâî ïîèñêà ðåøåíèÿ. Âî âòîðîì ñëó÷àå áåñïîëåçíûå ðåçîëüâåíòû ìîãóò áûòü ïîëó÷åíû, êîãäà âîçìîæíû ðàçëè÷íûå âàðèàíòû ïðèìåíåíèÿ ðåçîëþöèè, íà- ïðèìåð åñëè òåîðåìà ïðåäñòàâëåíà ñëåäóþùèì ìíîæåñòâîì äèçúþíêòîâ: 1) P i x x e( ( ), , ) , 2) P e x x( , , ) , 3) � �� �� �P x y u P y z P u z w P x w( , , ) ( , , ) ( , , ) ( , , )� � , 4) � �� �� �P x y u P y z P x w P u z w( , , ) ( , , ) ( , , ) ( , , )� � , 5) �P a e a( , , ) . Äàëåå áóäåì ñ÷èòàòü, ÷òî ýòî ìíîæåñòâî ñòðóêòóðèðîâàíî.  íåì äèçúþíê- òû 1) è 2) ÿâëÿþòñÿ ôàêòàìè, äèçúþíêòû 3) è 4) — ïðàâèëàìè âûâîäà, äèçú- þíêò 5) — çàêëþ÷åíèåì òåîðåìû.  ýòîì ñëó÷àå S-ðåçîëþöèÿ ê äèçúþíêòàì 3) è 4) íå ïðèìåíèìà ïî îïðåäåëåíèþ. À ïðè ïðèìåíåíèè S-ðåçîëþöèè, íàïðèìåð, ê äèçúþíêòàì 1) è 3) íåîïðåäåëåííîñòü âûáîðà ðåçîëüâèðóþùèõ ëèòåð ìîæåò áûòü óñòðàíåíà ñ ó÷åòîì ïîñëåäîâàòåëüíîñòè èõ îòðåçàíèÿ, êîòîðàÿ çàäàåòñÿ â ñåìàíòè÷åñêèõ èíäåêñàõ ýòèõ ëèòåð. Òàêæå íåîïðåäåëåííîñòü âûáîðà ðåçîëüâèðóþùèõ ëèòåð ìîæåò áûòü óìåíü- øåíà, èñïîëüçóÿ äåäóêòèâíóþ ñâÿçü ïðàâèë è îáðàòíóþ öåïî÷êó ðàññóæäåíèé, êîòîðàÿ ïîçâîëÿåò èñêëþ÷èòü èç ðàññìîòðåíèÿ ïðàâèëà, íå èìåþùèå ïðÿìîãî îò- íîøåíèÿ ê çàêëþ÷åíèþ òåîðåìû. Òàêèì îáðàçîì, íà îñíîâàíèè ñêàçàííîãî ìîæíî çàêëþ÷èòü, ÷òî ñîêðàùåíèå ðåçîëüâåíò â S-âûâîäå ïðîèñõîäèò ïðè ó÷åòå óïðàâëÿþùåé èíôîðìàöèè, êîòîðàÿ îòðàæàåò ñïåöèôèêó çàäà÷è è íàõîäèòñÿ â ñåìàíòè÷åñêèõ èíäåêñàõ ëèòåð òåîðåìû. À ïîñêîëüêó èçâåñòíûå îáîáùåíèÿ ïðèíöèïà ðåçîëþöèé íà íå÷åòêèå óòâåðæäåíèÿ òàêóþ èíôîðìàöèþ íå èñïîëüçóþò, òî ìîæíî ñ÷èòàòü, ÷òî ïðåäëîæåííûé ïîäõîä ê äîêàçàòåëüñòâó òåîðåì ÿâëÿåòñÿ áîëåå ïðîñòûì è áîëåå ãèáêèì. ÏÐÀÊÒÈ×ÅÑÊÎÅ ÏÐÈÌÅÍÅÍÈÅ Â íàñòîÿùåå âðåìÿ íå÷åòêîå óïðàâëåíèå ÿâëÿåòñÿ îäíîé èç íàèáîëåå àêòèâíûõ è ðåçóëüòàòèâíûõ îáëàñòåé ïðèìåíåíèÿ òåîðèè íå÷åòêèõ ìíîæåñòâ. Àëãî- ðèòìû íå÷åòêîãî óïðàâëåíèÿ îñíîâàíû íà íå÷åòêîì âûâîäå è ïðèìåíÿþòñÿ â ñëîæíûõ òåõíè÷åñêèõ ñèñòåìàõ â êà÷åñòâå èíòåëëåêòóàëüíûõ êîíòðîëëå- ðîâ [20]. Îñíîâíàÿ ôóíêöèÿ ñèñòåì íå÷åòêîãî óïðàâëåíèÿ çàêëþ÷àåòñÿ â âûðà- áîòêå â ñîîòâåòñòâèè ñ ïðàâèëàìè íå÷åòêèõ ïðîäóêöèé óïðàâëÿþùèõ âîçäåé- ñòâèé íà îñíîâå ïîñòóïàþùåé îò äàò÷èêîâ òåëåìåòðè÷åñêîé èíôîðìàöèè. Òà- êèå ñèñòåìû îòíîñÿòñÿ ê êëàññó ðåôëåêñíûõ ñèñòåì, ôóíêöèîíèðîâàíèå êîòîðûõ îñíîâàíî íà íåïîñðåäñòâåííîì îòîáðàæåíèè ñîñòîÿíèé â äåéñòâèÿ. Îäíàêî â îáùåì ñëó÷àå öåëü óïðàâëåíèÿ çàêëþ÷àåòñÿ â òîì, ÷òîáû íà îñíî- âàíèè àíàëèçà òåêóùåãî ñîñòîÿíèÿ îáúåêòà óïðàâëåíèÿ è âíåøíåé ñðåäû îïðåäå- ëèòü óïðàâëÿþùèå âîçäåéñòâèÿ, ðåàëèçàöèÿ êîòîðûõ ïîçâîëèò îáåñïå÷èòü æåëàå- ìîå ïîâåäåíèå èëè ñîñòîÿíèå îáúåêòà óïðàâëåíèÿ. Ïîýòîìó â áîëüøèíñòâå ïðî- áëåìíûõ ñèòóàöèé óïðàâëåíèå ïî ñâîåé ñóòè äîëæíî áûòü ñèòóàöèîííûì. Îñíîâíûìè çàäà÷àìè ñèòóàöèîííîãî óïðàâëåíèÿ ÿâëÿþòñÿ îöåíêà (ðàñïîçíà- âàíèå) ñèòóàöèé, îïðåäåëåíèå óïðàâëÿþùèõ ðåøåíèé è âûðàáîòêà ñîîòâåòñòâóþ- ùèõ âîçäåéñòâèé íà îáúåêò óïðàâëåíèÿ.  [21] ïîêàçàíî, ÷òî çàäà÷è îöåíêè ñèòóà- öèé è âûðàáîòêè óïðàâëÿþùèõ ðåøåíèé â ìîäåëÿõ ñèòóàöèîííîãî óïðàâëåíèÿ ìî- ãóò áûòü ñôîðìóëèðîâàíû êàê çàäà÷è äîêàçàòåëüñòâà òåîðåì, à ïðîöåäóðû èõ ðåøåíèÿ (â ñîâîêóïíîñòè) ìîæíî ðàññìàòðèâàòü êàê íå÷åòêèé íåäåòåðìèíèðîâàí- íûé ñåêâåíöèàëüíûé àâòîìàò âûðàáîòêè óïðàâëÿþùèõ ðåøåíèé. Èñïîëüçîâàíèå òàêîãî àâòîìàòà â òåõíè÷åñêèõ ñèñòåìàõ ïðåäñòàâëÿåòñÿ îñîáåííî ïåðñïåêòèâíûì ïðè óïðàâëåíèè àâòîíîìíûìè ðîáîòèçèðîâàííûìè ñèñòåìàìè [22], íàïðèìåð áåñ- ïèëîòíûìè ëåòàþùèìè àïïàðàòàìè, êîòîðûå â íàñòîÿùåå âðåìÿ øèðîêî èñïîëüçó- þòñÿ êàê â ìèðíûõ, òàê è â âîåííûõ öåëÿõ. Òàêèå ðîáîòû äîëæíû ñàìîñòîÿòåëüíî 56 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 äåéñòâîâàòü â çàðàíåå íåîïðåäåëåííûõ óñëîâèÿõ, îöåíèâàòü îêðóæàþùóþ ñðåäó, ïðèíèìàòü è ðåàëèçîâûâàòü ñîîòâåòñòâóþùèå óïðàâëÿþùèå ðåøåíèÿ. Ïîýòîìó ïðèìåíåíèå íå÷åòêîãî ñåêâåíöèàëüíîãî àâòîìàòà, îñîáåííî ñîâìåñòíî ñ ìåõàíèç- ìàìè íå÷åòêîãî óïðàâëåíèÿ, ïîçâîëèò îáåñïå÷èòü â íåêîòîðîé ìåðå àâòîíîìíîñòü è öåëåíàïðàâëåííîå ïîâåäåíèå ðîáîòèçèðîâàííûõ ñèñòåì. ÇÀÊËÞ×ÅÍÈÅ Ðàññìîòðåí ïîäõîä ê äîêàçàòåëüñòâó òåîðåì ñ íå÷åòêîé àðãóìåíòàöèåé.  êà÷å- ñòâå ïðàâèëà äîêàçàòåëüíîãî ðàññóæäåíèÿ èñïîëüçóåòñÿ êîìïîçèöèîííîå ïðàâè- ëî, à åãî ïðîöåäóðíàÿ ðåàëèçàöèÿ îñóùåñòâëÿåòñÿ S-ðåçîëþöèåé. Òàêîå êîì- ïëåêñèðîâàíèå ïîçâîëÿåò, ñ îäíîé ñòîðîíû, ñíÿòü ïðîáëåìó çíà÷èìîñòè ðåçîëü- âåíò â ñìûñëå (1), à ñ äðóãîé — îáåñïå÷èòü ðåãóëÿðíîñòü ïðîöåññà äîêàçàòåëüñòâà êàê â íå÷åòêîé ëîãèêå, òàê è â åå ÷àñòíîì ñëó÷àå — äâóçíà÷íîé ëîãèêå. Ïðè ýòîì äîïóñêàåòñÿ èñïîëüçîâàíèå íå âïîëíå èñòèííîé àðãóìåíòàöèè.  öåëîì äàííûé ïîäõîä ìîæåò áûòü ýôôåêòèâíûì ìåòîäîì ïðè ïîñòðîåíèè äî- êàçàòåëüñòâà òåîðåì â íå÷åòêîé ëîãèêå ñ èñïîëüçîâàíèåì ïðîöåäóðû îïðîâåðæåíèÿ. Îí íå ïðåòåíäóåò íà çàâåðøåííîñòü è ñëóæèò ëèøü èëëþñòðàöèåé èñïîëüçîâàíèÿ ìå- õàíèçìîâ ïðèáëèæåííûõ ðàññóæäåíèé äëÿ ïîëó÷åíèÿ íå÷åòêîãî âûâîäà ðåçîëþöèîí- íîãî òèïà è ìîæåò áûòü èñïîëüçîâàí â êà÷åñòâå ìåòîäîëîãè÷åñêîé îñíîâû äëÿ ðàçðà- áîòêè ðåãóëÿðíûõ àëãîðèòìîâ äîêàçàòåëüñòâà òåîðåì ñ íå÷åòêîé àðãóìåíòàöèåé. ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ 1. Ìóêàèäîíî Ì.À. Íå÷åòêèé âûâîä ðåçîëþöèîííîãî òèïà.  êí.: Íå÷åòêèå ìíîæåñòâà è òåî- ðèÿ âîçìîæíîñòåé (ïîä ðåä. ßãåðà Ð.). Ìîñêâà: Ðàäèî è ñâÿçü, 1986. Ñ. 153–161. 2. Dubois D., Prade H. Necessity and the resolution principle. IEEE Transactions on Systems, Man, and Cybernetics. 1987. Vol. 17, N 3. P. 474–478. 3. Kim C.S., Kim D.S., Park J. A new fuzzy resolution principle based on the antonym. Fuzzy Sets and Systems. 2000. Vol. 113, N 2. P. 299–307. 4. Fontana F.A., Formato F. A similarity-based resolution principle. International Journal of Intelligent Systems. 2002. Vol. 17, N 9. P. 853–872. 5. Raha S., Ray K.S. Approximate reasoning based on generalised disjunctive syllogism. Fuzzy Sets and Systems. 1994. Vol. 61, N 2. P. 143–151. 6. Habiballa H. Resolution principle in fuzzy predicate logic. Acta Fac. Paed. Univ. Tyrnaviensis. Ser. C. 2005. N 9. P. 3–12 7. Habiballa H. Resolution principle and fuzzy logic. Fuzzy Logic — Algorithms, Techni- ques and Implementations. Ch. 3. London: IntechOpen, 2012. P. 20. 8. Øòîâáà Ñ.Ä. Ïðîåêòèðîâàíèå íå÷åòêèõ ñèñòåì ñðåäñòâàìè MATLAB. Ìîñêâà: Ãîðÿ÷àÿ ëèíèÿ. Òåëåêîì, 2007. 288 ñ. 9. Raha S., Pal N.R., Ray K.S. Similarity based approximate reasoning: Methodology and application. IEEE Transactions on Systems, Man, and Cybernatics. Part A: Systems and humans. 2002. Vol. 32, N 4. P. 541–547. 10. Mondal B., Mazumdar D., Raha S. Similarity in approximate reasoning. International Journal of Computational Cognition. 2006. Vol. 4, N 3. P. 46–56. 11. Mondal B., Raha S. Similarity-based inverse approximate reasoning. IEEE Transaction on Fuzzy Systems. 2011. Vol. 19, N 6. P. 1058–1071. 12. Mondal B., Raha S. Approximate reasoning in fuzzy resolution. International Journal of Intelligence Science. 20113. Vol. 3, N 2. P. 86–98. 13. Ñàìîõâàëîâ Þ.ß. Ìåòîä ïðîáëåìíî-îðèåíòèðîâàííîãî äîêàçàòåëüñòâà â íå÷åòêîé ëîãèêå. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. 1995. ¹ 5. Ñ. 58–68. 14. Çàäå Ë.À. Ïîíÿòèå ëèíãâèñòè÷åñêîé ïåðåìåííîé è åãî ïðèìåíåíèå ê ïðèíÿòèþ ïðèáëèæåí- íûõ ðåøåíèé. Ìîñêâà: Ìèð, 1976. 165 ñ. 15. Bofill M., Moreno G., V�zquez C., Villaret M. Automatic proving of fuzzy formulae with fuzzy logic programming and SMT. Actas de las XIII Jornadas sobre Programacio' n y Lenguajes, PROLE’13, Jornadas SISTEDES, Madrid, 18–20 September 2013. P. 151–165. 16. Ñàìîõâàëîâ Þ.ß. Îöåíêà îáîñíîâàííîñòè óïðàâëåí÷åñêèõ ðåøåíèé íà îñíîâå íå÷åòêîé ëîãèêè. Óïðàâëÿþùèå ñèñòåìû è ìàøèíû. 2017. ¹ 3. C. 26–34. ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2 57 17. Ñàìîõâàëîâ Þ.ß. Ñîãëàñîâàíèå ýêñïåðòíûõ îöåíîê â ìàòðèöàõ îòíîøåíèé ïðåäïî÷òåíèÿ. Óïðàâëÿþùèå ñèñòåìû è ìàøèíû. 2002. ¹ 6. Ñ. 49–53. 18. Zwick R., Carlstein E., Budescu D.V. Measures of similarity among fuzzy concepts: A comparative analysis. International Journal of Approximat. 1987. Vol. 1, N 2. P. 221–242. 19. Mondal B., Mazumdar D., Raha S. Similarity in approximate reasoning. International Journal of Computational Cognition. 2006. Vol. 4, N 3. P. 46–56. 20. Wilamowski B.M., Irwin J.D. (Eds.) The industrial electronics handbook: Intelligent systems. Boca Raton: CRC Press, 2011. 610 p. 21. Ñàìîõâàëîâ Þ.ß. Àâòîìàòè÷åñêîå äîêàçàòåëüñòâî òåîðåì è íå÷åòêèé ñèòóàöèîííûé ïîèñê ðåøåíèé. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. 2001. ¹ 4. Ñ. 53–60. 22. Ford M. The rise of the robots: Technology and the threat of jobless future. New York: Basic Books, 2015. 334 p. Íàä³éøëî äî ðåäàêö³¿ 22.01.2018 Þ.ß. Ñàìîõâàëîâ ÄÎÂÅÄÅÍÍß ÒÅÎÐÅÌ Ó ÍÅײÒÊ²É ËÎòֲ ÍÀ ÎÑÍβ ÑÒÐÓÊÒÓÐÍί ÐÅÇÎËÞÖ²¯ Àíîòàö³ÿ. Ðîçãëÿíóòî ï³äõ³ä äî äîâåäåííÿ òåîðåì ó íå÷³òê³é ëîã³ö³ ³ íå ö³ëêîì ³ñòèííîþ àðãóìåíòàö³ºþ. ßê ïðàâèëî äîêàçîâîãî ì³ðêóâàííÿ âèêî- ðèñòîâóþòü êîìïîçèö³éíå ïðàâèëî âèâåäåííÿ Ë. Çàäå, à éîãî ïðîöåäóðíà ðåàë³çàö³ÿ çä³éñíþºòüñÿ ìåõàí³çìîì ñïðîñòóâàííÿ. Ñòðóêòóðíà ðåçîëþö³ÿ (S-ðåçîëþö³ÿ), ÿêà º óçàãàëüíåííÿì ïðèíöèïó ðåçîëþö³é íà íå÷³òê³ òâåð- äæåííÿ, çàïðîïîíîâàíà ÿê òàêèé ìåõàí³çì. S-ðåçîëþö³ÿ áàçóºòüñÿ íà ñåìàí- òè÷íèõ ³íäåêñàõ ë³òåð ³ ¿õí³é ñõîæîñò³. Ñåìàíòè÷í³ ³íäåêñè º ³ñòîòíèì ìî- ìåíòîì S-ðåçîëþö³¿. Âîíè ì³ñòÿòü ³íôîðìàö³þ, ÿêà âèêîðèñòîâóºòüñÿ ÿê êåð³âíà ó ïðîöåñ³ âèâîäó, à ñõîæ³ñòü ïîëÿãຠó ïîøóêó ë³òåð äëÿ îòðèìàííÿ S-ðåçîëüâåíòè. Êîìïëåêñóâàííÿ êîìïîçèö³éíîãî ïðàâèëà âèâîäó Ë. Çàäå ³ S-ðåçîëþö³¿ äîçâîëÿº, ç îäíîãî áîêó, çíÿòè ïðîáëåìó êîðåêòíîñò³ ðåçîëü- âåíò â íå÷³òê³é ëîã³ö³, à ç ³íøîãî — çàáåçïå÷èòè ðåãóëÿðí³ñòü ïðîöåñó äî- âåäåííÿ ÿê â äâîçíà÷í³é, òàê ³ â íå÷³òê³é ëîã³ö³. Êëþ÷îâ³ ñëîâà: àâòîìàòè÷íå äîâåäåííÿ òåîðåì, íå÷³òêà òåîðåìà, ïðèíöèï ðåçîëþö³é, íå÷³òêà ëîã³êà, íàáëèæåí³ ì³ðêóâàííÿ, óçàãàëüíåíå ïðàâèëî modus ponens, êîìïîçèö³éíå ïðàâèëî, íå÷³òê³ ïðåäèêàòè, íå÷³òê³ ³ ë³íãâ³ñòè÷í³ çì³íí³. Yu.Ya. Samokhvalov PROOF OF THEOREMS IN FUZZY LOGIC ON THE BASIS OF STRUCTURAL RESOLUTION Abstract. The author considers the approach to proof of theorems with fuzzy and not quite true argumentation. In this approach, the Zadeh composition rule of correctness is used as a rule of evidence, and its procedural implementation is carried out by refutation mechanism. As such a mechanism, a structural resolution (S-resolution) is proposed, which is a generalization of the principle of resolutions to fuzzy statements. S-resolution is based on semantic indices of letters and their similarity. Semantic indices are a key point of S-resolution. They contain information that is used as a control for the derivation process. And similarity implies finding letters to get S-resolvent. Combining the Zadeh compositional derivation rule and S-resolution allows, on the one hand, solving the problem of correctness of resolvents in fuzzy logic, and on the other hand, ensuring the regularity of the proof process in both two-valued and fuzzy logic. Keywords: automatic proof of theorems, fuzzy theorem, principle of resolutions, fuzzy logic, approximate reasoning, generalized rule of modus ponens, composition rule, fuzzy predicates, fuzzy and linguistic variables. Ñàìîõâàëîâ Þðèé ßêîâëåâè÷, äîêòîð òåõí. íàóê, ïðîôåññîð êàôåäðû Êèåâñêîãî íàöèîíàëüíîãî óíèâåðñèòåòà èìåíè Òàðàñà Øåâ÷åíêî, e-mail: yu1953@ukr.net. 58 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 2