автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Построение импликативных зависимостей для аналитического описания предметных областей и обнаружения ошибок в данных

кандидата физико-математических наук
Ревенко, Артем Викторович
город
Москва
год
2013
специальность ВАК РФ
05.13.17
цена
450 рублей
Диссертация по информатике, вычислительной технике и управлению на тему «Построение импликативных зависимостей для аналитического описания предметных областей и обнаружения ошибок в данных»

Автореферат диссертации по теме "Построение импликативных зависимостей для аналитического описания предметных областей и обнаружения ошибок в данных"

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

Построение импликативных зависимостей для аналитического описания предметных областей и обнаружения ошибок в данных

Специальность 05.13.17 - "Теоретические основы информатики"

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

ИМЕНИ М.В.ЛОМОНОСОВА

На правах рукописи

РЕВЕНКО Артем Викторович

10 Т 2013

Москва 2013

005534817

Работа выполнена на кафедре анализа данных и искусственного интеллекта отделения прикладной математики и информатики ФГБОУ ВПО "Национальный исследовательский университет Высшая школа экономики".

Научный руководитель

доктор физико-математических наук Кузнецов Сергей Олегович.

Официальные оппоненты:

Чечкин Александр Витальевич, доктор физико-математических наук, профессор, Военная академия РВСН имени Петра Великого;

Аншаков Олег Михайлович,

доктор физико-математических наук, профессор, ФГБОУ ВПО Российский государственный гуманитарный университет.

Ведущая организация

ФГБОУ ВПО Воронежский государственный университет.

Защита состоится "30" октября 2013г. в 16ч. 45м. на заседании диссертационного совета Д 501.002.16 при ФГБОУ ВПО Московском государственном университете имени М.В.Ломоносова по адресу: Российская Федерация, 119991, Москва, ГСП-1, Ленинские горы, д.1, МГУ имени М.В.Ломоносова, Механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в Фундаментальной библиотеке ФГБОУ ВПО МГУ имени М.В.Ломоносова (Москва, Ломоносовский про-спект, д.27, сектор А).

Автореферат разослан "30" сентября 2013 г.

Ученый секретарь диссертационного совета Д 501.002.16 при ФГБОУ ВПО МГУ, доктор физико-математических наук,

профессор

Корнев Андрей Алексеевич

Общая характеристика работы

Актуальность

В последние десятилетия активно развиваются такие методы и средства автоматизации процессов работы с формальными теориями, как нахождение и проверка правильности доказательств. Однако до нахождения доказательств теорем и до проверки их справедливости необходимо породить гипотезы, которые составляют базу для последующей формулировки теорем. Методы и средства для порождения гипотез в импликативной форме хорошо известны и изучены в Анализе Формальных Понятий (АФП). Методология, используемая в АФП, может найти применения в самых разных областях науки и техники. Однако существующие методы не являются достаточно гибкими для применения и процесс автоматизации такого исследования недостаточно хорошо изучен и проиллюстрирован, что препятствует дальнейшему распространению АФП. Хорошо известно, что методы АФП являются очень чувствительными к ошибкам. Для расширения области применения таких методов необходимо предложить инструментарий для нахождения ошибок. Решение описанных выше задач позволит, таким образом, разработать инструментарий для автоматического порождения гипотез и подготовить АФП для применения в новых предметных областях.

Цели работы

Целью исследования, результаты которого представлены в диссертации, является разработка методов и средств автоматизации исследования импликативных зависимостей на основе методологии АФП.

Задачи, решению которых посвящены исследования:

1. разработать методы и средства автоматизации построения импликативных теорий на примерах:

• свойств функций на конечных множествах;

• алгебраических тождеств;

2. разработать методы и средства нахождения ошибок в бинарных данных с помощью импликативных зависимостей.

Объектом исследования являются импликативные зависимости.

Предметом исследования являются методы и программные средства автоматизации процессов порождения и анализа импликативных зависимостей.

В соответствии с паспортом специальности 05.13.17 "Теоретические основы информатики" работа включает в себя

• исследования процессов создания, накопления и обработки информации; методов преобразования информации в данные и знания;

• исследования методов преобразования информации в данные и знания;

• создание и исследование информационных моделей, моделей данных и знаний, методов работы со знаниями, методов машинного обучения и обнаружения новых знаний;

• исследования принципов создания и функционирования аппаратных и программных средств автоматизации указанных процессов.

В исследованиях затронуты следующие области из паспорта специальности 05.13.17 "Теоретические основы информатики".

4 Исследование и разработка средств представления знаний; принципы создания языков представления знаний, в том числе - для плохо структурированных предметных областей и слабоструктурированных задач; разработка интегрированных средств представления знаний; средств представления знаний, отражающих динамику процессов, концептуальных и семиотических моделей предметных областей.

5 Разработка и исследование моделей и алгоритмов анализа дан-

ных, обнаружения закономерностей в данных и их извлечения.

8 Исследование и когнитивное моделирование интеллекта, включая моделирование поведения, моделирование рассуждений различных типов, моделирование образного мышления;

12 Разработка математических, логических, семиотических и лингвистических моделей и методов взаимодействия информационных процессов, в том числе на базе специализированных вычислительных систем.

14 Разработка теоретических основ создания программных систем для новых информационных технологий.

Основные результаты

В рамках работы автором получены следующие основные результаты.

1. Разработаны и программно реализованы методы автоматизированного изучения импликативных взаимосвязей между свойствами функций на множествах. Испытания программных средств подтвердили их работоспособность.

2. Построено множество импликативных взаимосвязей между свойствами функций на двух-, трех- и четырехэлементных множествах. Получены доказательства части импликаций из базиса импликаций, составлен список недоказанных и не опровергнутых импликаций (открытых вопросов).

3. Разработаны и программно реализованы: методы автоматизированного построения импликативных взаимосвязей между алгебраическими тождествами, алгоритмы проверки выполнения алгебраических тождеств; нахождения алгебр на бесконечном носителе, удовлетворяющих некоторому множеству тождеств и не удовлетворяющих некоторому одному тождеству. Испытания программных средств подтвердили их работоспособность.

4. Построено множество всех истинных импликативных взаимосвязей между алгебраическими тождествами длины не более пяти. Получены доказательства всех импликаций из базиса импликаций.

5. Разработан метод нахождения ошибок в бинарных данных. Получено доказательство того, что разработанный метод удовлетворяет предъявляемым к нему требованиям. Программно реализован интерактивный полиномиальный алгоритм нахождения ошибок в бинарных данных. Проведенные тестовые испытания подтвердили его работоспособность.

Научная новизна

Разработанные автором диссертации методы автоматизации порождения импликативных теорий реализуют новые функциональные возможности. Решена задача нахождения алгебр на бесконечном носителе, заданных некоторым набором тождеств. Автором диссертации предложен новый метод нахождения ошибок в бинарных данных, основанный на АФП. Доказано, что этот метод обеспечивает решение задачи нахождения признаков (или классификации) за полиномиальное время.

Практическая ценность

Методы и средства автоматизации построения импликативных теорий и разработанный метод нахождения ошибок в бинарных данных имеют решающее значение для разработки системы анализа и обработки данных на основе АФП. Разработанные в диссертации методы могут быть использованы для автоматизации построения импликативных теорий в некоторых формализуемых областях наук, таких как, например, алгебраические тождества. Полученные в рамках проведения диссертационного исследования импликативные теории могут быть использованы в соответствующих предметных областях.

Разработанный метод нахождения ошибок в бинарных данных допускает его использование на больших наборах данных.

Апробация

Результаты проведенных исследований докладывались на семинаре кафедры анализа данных и искусственного интеллекта НИУ-ВШЭ (с 2010г. по 2013г., неоднократно), на семинаре института алгебры Политехнического Университета Дрездена (с 2011г. по 2013г., неоднократно) и на семинаре "Проблемы современных информационно-вычислительных систем" на механико-математическом факультете МГУ имени М.В.Ломоносова (2013г.). Результаты докладывались на следующих международных семинарах и конференциях:

1. 19-21.10.2010 Concept Lattices and Their Applications 2010, Sevilla, Spain

http://www.glc.us.es/cla2010/;

2. 23-25.02.2011 inFormal Concept Analysis Workshop, Dresden, Germany

http://tu-dresden.de/die_tu_dresden/fakultaeten/ fakultaet_mathematik_und_naturwissenschaften/ f achri chtung_mathemat ik/institute/algebra/ conferences/201lifca;

3. 11-13.07.2012 European PhD Program in Computional Logic Workshop 2012, Dresden, Germany

http://www.epcl-study.eu/content/phdwsl2/;

4. 1-3.07.2013 European PhD Program in Computional Logic Workshop 2013, Dresden, Germany

http://www.epcl-study.eu/content/phdwsl3/

5. 2.05.2013 IPID Doktorandtentreffen, Cologne, Germany https://www.daad.de/hochschulen/ internationalisierung/ipid/13303.de.html

6. 28.06.2013 International Seminar, Dresden Germany

http://tu-dresden.de/die_tu_dresden/fakultaeten/ fakultaet_mathematik_und_naturwissenschaften/ fachrichtung_mathematik/institute/algebra/ veranstaltungen;

7. 28.08.2012 What can FCA do for Artificial Intelligence? 2012, Montpellier, France

http://fca4ai.hse.ru/2012/;

8. 11-14.10.2012 Concept Lattices and Their Applications 2012, Malaga, Spain

http://www.matap.uma.es/cla2012/CLA2012/Welcome.html;

9. 24.03.2013 Formai Concept Analysis meets Information Retrieval 2013, Moscow, Russia

http://fcair.hse.ru/;

10. 03.08.2013 What can FCA do for Artificial Intelligence? 2013, Beijing, China

http://fca4ai.hse.ru/2013.

По теме диссертации опубликовано 7 печатных работах, в том числе две из них [5, 7] в журналах, включенных в список ВАК.

Структура и объем диссертации

Работа состоит из пяти глав, включая введение, заключение, список литературы. Объем диссертации - 153 страницы, включая оглавление. Список литературы включает 86 наименования. В текст диссертации входят 16 иллюстраций, 2 таблицы, 1 листинг и 3 алгоритма.

Содержание работы

Во введении описываются цели работы, обосновывается ее актуальность и практическая значимость. Перечисляются основные результаты, представляются конспективные сведения по истории во-

проса, которые затрагивают положения диссертационного исследования. Дается краткий обзор основных смежных научных направлений. Проводится сравнения с другими методами анализа данных, использующими алгебраические решетки, а также приводятся примеры применения методов и средств анализа формальных понятий (АФП) для решения задач анализа данных в различных областях наук.

Методология анализа формальных понятий используется в данной работе как основной инструментарий для порождения, анализа и представления импликативных теорий. Кроме того, разработанные в рамках данной работы методы дополняют методы АФП, особенно в части, которая касается нахождения ошибок в данных.

Во второй главе дается введение в АФП, содержание которого предназначено для облегчения понимания положений диссертации. Оно начинается с изложения элементов теории решеток, так как исторически АФП возник при попытке придать прикладную направленность этой теории. В следующем разделе представлено введение в АФП. В двух заключительных подразделах второй главы рассматриваются частные вопросы АФП, имеющие прямое отношение к данной работе, такие как метод активного обучения "Исследование признаков" и вопросы представления знаний в виде диаграммы решетки.

В том числе даются следующие основные определения.

Пусть даны множества С, М. Пусть / С Д х М - бинарное отношение между множествами би¥. Тройка К := (£7, М, I) называется (формальным) контекстом. Множество С называют множеством объектов, множество М - множеством признаков. Пусть А С М, X С й. Рассмотрим отображения <р: 2е —> 2м и ф: 2м —> 2е:

<р(Х) := {т £ М | д1т для всех д £ X}; ф{А) := {д б С | д1т для всех т € А}.

Обычно вместо ¡риф используют единое обозначение (•)'. Пусть ^ С М или 2 С й, (£)" называется замыканием 2 в К, Пусть

1С G, ACM. (Формальное) понятие есть пара (X, Л):

Х' = А и А' = Х.

Пусть у = (X, А). X называется объемом понятия у, А называется содержанием понятия у. Формальные понятия частично-упорядочены отношением

pCi, Ai) > (Х2,Л2) XiDX2 (Аз 2 Ах).

Пусть то G М,Х С G, тогда то называется отрицательным признаком. то € X' в том и только в том случае, если ни один х G X' не удовлетворяет xlrn. Пусть А С М; А С X' в том и только в том случае, если все то G А удовлетворяют то € X'. Импликацией в контексте К = (G, М, I) называется пара (А, В), пишут А —»• В, где А. В С. М. А называется посылкой, В называется следствием импликации А В. Импликация А В удовлетворяется множеством признаков N, если А N или В С JV. В противном случае считают, что множество признаков противоречит импликации. Импликация А —» В верна в К, если она удовлетворяется всеми g', д G G, то есть каждый объект, обладающий всеми признаками из А также обладает всеми признаками из В. Поддержкой импликации в контексте К называют множество всех объектов контекста К, чьи содержания содержат как посылку, так и следствие импликации. Атомарной импликацией называют такую импликацию, в следствии которой содержится только один признак, то есть А -> Ь, где А С М, Ъ G М. Новые верные импликации из уже имеющихся можно получить с помощью правил Армстронга-.

_ А -> В А-> B,BUC ^ D

А->А' AUC^B' AUC^D

Базисом импликаций контекста К называют множество £ импликаций, из которого любая верная в контексте К импликация может быть выведена (с помощью правил Армстронга) и никакое собственное подмножество множества £ не обладает таким свойством. Подмножество признаков Р С М называется псевдосодержанием,

если Р фР" и для любого псевдосодержания ф, такого что <3 С Р, имеет место ф" с Р. Минимальный по числу импликаций базис известен как канонический базис импликаций Посылки этого базиса можно описать в терминах псевдо-содержаний. Канонический базис импликаций тогда можно предстваить в виде: {Р -4 (Р" \Р) \ Р -псевдо-содержание}.

Зависимостями предметной области называются такие импликации, которые являются истинными как аксиомы или теоремы в предметной области.

В третьей и четвертой главах на примерах двух предметных областей представлены разработанные автором методы и средства автоматизации, которые необходимы при использовании методологии АФП и в процессе построения импликативных теорий.

Третья глава посвящена решению задачи, направленной на создание методов и средств автоматизации построения взаимосвязей между свойствами функций на конечных множествах. Вопросы о взаимосвязях свойств функций на конечных множествах возникают в разных областях математики. К их числу относятся: теория выбора; теория решеток; теория множеств; примеры исследований взаимосвязей между свойствами функций, которые представлены далее, в разделе 3.1. Однако кроме актуальности для других научных дисциплин, рассмотренная в третьей главе задача обладает еще одним важным преимуществом. В связи с тем, что свойства функций определены математически, представляется целесообразным автоматизировать проверку наличия тех или иных свойств у конкретных функций. Если, кроме того, автоматизировать генерацию функций на конечных множествах, то, тем самым, будет автоматизирован процесс построения начального контекста для исследования признаков.

Как отмечается во второй главе, для применения метода "исследование признаков" необходимо иметь возможность находить контрпримеры к исследуемым импликациям. В данном исследовании контрпримеры были найдены следующим образом. Сначала ге-

нерировался исходный контекст, и строился его канонический базис импликаций. После этого генерировались функции на множестве заданного размера. Эти функции проверялись относительно ранее выбранных свойств, далее производилась проверка полученных комбинаций свойств на удовлетворение каждой импликации. В соответствии с описанием метода в разделе 2.2.1 если хотя бы один контрпример был найден, то этот контрпример добавлялся к контексту, и базис вычислялся заново.

В процессе исследования признаков на свойствах функций не было необходимости проверять все импликации. Благодаря тому, что вопросы взаимосвязей свойств функций имеют длительную историю изучения, некоторые импликации между свойствами функций, получение которых являются целью данной главы, были уже исследованы другими авторами и доказаны как теоремы. Эти знания использовались в ходе проведения данного исследования. Большая часть базисов импликаций на свойствах функций, однако, не была ранее освещена в литературе. Они впервые рассмотрены и частично доказаны в рамках работы в разделе 3.3. Доказательства импликаций, выполненные автором в работе (утверждения 3.3.7-9), а также рядом других авторов (для более полного представления), изложены в разделе 3.3.2. В разделе 3.3.3 приведен подготовленный автором список импликаций, доказать которые не удалось. Отмечено, что в случае доказательства всего представленного списка импликаций, построение импликативной теории будет завершено.

При доказательстве импликаций большую трудность представляли собой импликации, имеющие большую посылку. Практически импликации, имеющие более четырех свойств в посылке, крайне трудны для рассмотрения потому, что многие из этих свойств являются зависимыми. Для упрощения работы с такими импликациями в разделе 3.2 было сформулировано, доказано и в последующем применено утверждение о возможности изменения вида базиса импликаций.

Утверждение 3.2.1 Пусть <3 - канонический базис импликаций контекста К. содержащий импликацию Н —» Н" \ Н. Тогда, если

ХС Ни X" = Н", то множество импликаций ©о, построенное из в заменой импликации Я —» Н"\Н на импликацию X Н"\Н, остаётся минимальным по размеру базисом импликаций контекста К.

В рамках исследования автором доказательно установлена истинность следующих импликаций (утверждения 3.3.3-9):

• ЭКС О, Н, О АО Б;

• ИНТ АОБ, ОБ;

• М В, С;

• Б -»■ ИНТ, К, ИД, НП, О, С, Н, М;

• НП ИД, КГ;

• Н ОАОБ;

• ИД, В -> О;

. ИД, М -> О;

• ИД, КГ НП;

• К О, Н, С;

• ИНТ, НП +-> ИНТ, КГ;

• ИНТ, ИД, В о ИНТ, О;

• ИНТ, НП «-»■ ИНТ, Н, О;

. ЭКС, НП <-► ЭКС, ИД, М;

• ИНТ, Н, М о ИНТ, Б.

Составлен список импликаций, истинность которых предстоит проверить для завершения исследования (открытые вопросы):

1. КГ В;

2. ИД, ОБ, АОБ -»■ ОАОБ;

3. АТ Н, ОБ, ОАОБ, АОБ, В;

4. ИНТ, ОБ -> Н, ИД, ОАОБ;

5. Н, ИНТ ->■ ИД;

6. АТ, С КГ;

7. О, ОБ, АОБ С;

8. Н, ИД, О, АОБ С;

9. О, В, ОБ С;

10. О, АОБ, КГ О АОБ, С; И. К О АОБ, АОБ;

12. НП ->• ОАОБ, С, В, О;

13. Б ОБ;

14. М, ОБ О;

15. ИНТ, КГ -» Н, К, ОАОБ, С, О;

16. Н, М О;

17. Н, ИД, В -> С;

18. ИНТ, В, ОБ ->• К, НП, КГ;

19. ИД, КГ ОАОБ, С;

20. М, АОБ, ОБ ОАОБ;

21. ИД, М, ОБ ОАОБ;

22. М, АТ -> ИД, НП;

23. АТ, ЭКС ИД, НП, М;

24. М, ЭКС КГ;

25. НП, АТ -> М;

26. НП, ОБ Н;

27. М, К -> ИД;

28. Н, М, ОБ КГ;

29. М, ЭКС, К Б, ИНТ.

Получена следующая диаграмма решетки рассмотренных

Рис. 1: Диаграмма решетки контекста функций на множествах М2, М3 и М4

свойств функций на множествах, рис. 1.

В процессе исследования основное внимание было уделено функциям на множествах размера 2 и 3. В разделе 3.3.1 представлены результаты проведенного автором исследования различий в им-пликативных теориях взаимосвязей свойств функций на множества размера 2 и 3. Сформулированы и доказаны утверждения, объясняющее все различия в импликативных теориях этих типов функций.

Утверждение 3.3.1 Для любой функции /, определённой на множестве Мг, из наличия свойства О следует наличие свойства С.

Утверждение 3.3.2 Для любой функции /, определённой на множестве Мг, из наличия свойства ИНТ следует наличие свойства С.

В разделе 3.4 показано, каким образом можно обобщить определение свойств функций, а вместе с тем - и полученные результаты, на случай функций, заданных не на произвольных множествах, а на решетках.

В результате исследований, представленных в третьей главе, получены следующие результаты.

1. Разработаны методы автоматизации и структуризации процедуры исследования импликативных взаимосвязей свойств функций на множествах. Исследуемые взаимосвязи структурированы в виде решетки понятий, а также в виде базиса импликаций. Представлены доказательства импликаций, подготовлен список открытых импликаций.

2. Разработан и программно реализован метод, позволяющий изменять вид базиса импликаций и отобразить импликации в более удобной для практических приложений форме.

3. Сформулированы и доказаны различия между импликативны-ми теориями для функций на двух- и трехэлементных множествах.

4. Дано обобщение результатов исследования свойств функций на случай функций, заданных на решетках.

5. Разработаны и программно реализованы методы, позволяющие автоматизировать процесс получения импликативных взаимосвязей между свойствами функций. Написанное программное обеспечение удовлетворяет сформулированным требованиям.

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

добиться еще большей степени автоматизации, чем при изучении свойств функции, так как количество представляющих интерес для приложений тождеств в этом случае значительно больше. Для рассмотрения были выбраны тождества, длина которых не превышает 5 (длиной тождества называется сумма числа вхождений переменных и операций). Таких тождеств насчитывается 70.

Область науки, изучающая общие закономерности алгебраических систем, называется универсальной алгеброй. Эквациональ-ными классами в универсальной алгебре называют классы алгебр, удовлетворяющих заданным алгебраическим тождествам. Эквацио-нальные классы играют в этой области центральную роль. В разделе 4.1 приведена ключевая теорема универсальной алгебры, показывающая эквивалентность многообразий алгебр и эквационалъных классов.

В разделе 4.2 описаны рассматриваемые в четвертой главе тождества. Алгебраические тождества, как и свойства функций на множествах, заданы строго математически. Более того, проверку удовлетворения конкретной алгеброй конкретного тождества можно автоматизировать. Порождение всех алгебр на носителе ограниченного размера также можно автоматизировать. Эти задачи были решены автором и представлены в разделе 4.3.1. Изоморфизм алгебр позволяет избежать порождения тех алгебр, которые заведомо не могут привнести новой информации.

Изучение алгебраических тождеств является подходящей задачей, решение которой целесообразно с применением метода "исследование признаков", в том числе потому, что на настоящее время относительно высокого уровня развития достигли инструментальные средства автоматического доказательства теорем и нахождения конечных моделей. Для этих целей в процессе диссертационного исследования использовались программы Масе4 и РгоуегЭ, решающие поставленные задачи быстрее других средств, которые могут быть использованы для тех же целей, и имеют удобный интерфейс для доступа к ним из внешних программ.

Доказанные в разделе 4.3.2 утверждения показывают, однако, что порождения лишь алгебр на конечном носителе недостаточно для построения импликативной теории выбранных алгебраических тождеств. Задача нахождения бесконечных алгебр, удовлетворяющих заданным тождествам, крайне трудоемка и в общем случае не имеет решения. Автору удалось найти методы порождения алгебр на бесконечном носителе, необходимые для завершения исследования, а также - программно реализовать эти методы (раздел 4.3.3).

Задача порождения алгебр на бесконечном носителе ставится следующим образом. Пусть дана импликация А —> 6, А С Мц, Ь 6 Mid- Тогда необходимо найти такую алгебру А = (N, *, —, а), которая удовлетворяет всем тождествам из А и не удовлетворяет тождеству Ь.

Для нахождения таких алгебр была зафиксирована форма бинарной, унарной и нулярной операций. Нулярная операция всегда фиксировалась равной нулю а = 0. Унарная операция — искалась в следующем виде:

-п =

и о, ии и2,

если п — 0 если п = 1 если п = 2

р х п + д, если п> 3,

где tio,in,U2 е N<5, p<eN<3, g е {0,1,-1,2,-2,3,-3}.

Бинарная операция * искалась в следующем виде:

771*71 =

£>оо, £>оъ Ью. Ьц, Ьо2, £>оз,

Ь\2,

£>13,

Ью, £>зо, £>21, ¿>31, £>22,

Со X 771 + С?о С1 X Ш + С2 X Ш + (¿2

с3 х т + «¿3 С4 х т + ¿1

С5 X 7П + С?5

Сб х т + ¿6

С7 X ТО + (¿7

с8 х то + с?8

кСд X 771 + ¿9

X п + во, хп + е 1, х п + е2, х п + е3, х п + е4, X п + е5) х п + е6, хп + е 7, х п + е8, х п + ед,

если т = 0 и п = 0;

если то = 0 и п = 1;

если то = 1 и п = 0;

если т = 1 и п = 1;

если то = 0 и п — 2;

если то = 0 и п = 3;

если то = 1 и п = 2;

если то = 1 и п = 3;

если то = 2 и п = 0;

если то = 3 и п = 0;

если то = 2 и п = 1;

если то = 3 и п = 1;

если то = 2 и п = 2;

если то = 0 и 71 > 3;

если то = 1 и п > 3;

если то > 3 и п = 0;

если то > 3 и п — 0;

если то > 2 и то = п;

если т>1ип — т+1;

если то>2ип = то — 1;

если то>1ип = 77г + 2;

если то>3ип=то— 2;

если т>4ип^т,т±1,т±2,

где 600А1А0А1 е N<4,

Ьо2- £>оз, Ьи, £>1з, 612, £>13,62о, £>зо, £>22 £

со-э, ¿0-9 е {0,1}, е0-э 6 {0,1, -1,2, -2,3, -3}.

Все импликации, к которым не были найдены контрпримеры в заданном виде, были доказаны. Таким образом, такой выбор структуры алгебр позволил найти все необходимые контрпримеры.

Для нахождения алгебр в заданном виде автором диссертации предложен алгоритм поиска с возвратом.

Input: idls_prem С Мц, id_conc € М;

Output: Алгебра А сигнатуры (*, —, 0), удовлетворяющая тождествам idls_prem и не удовлетворяющая тождеству id_conc.

1 while True do

2

3

4

5

6

7

8 9

10 11 12

13

14

15

16

17

18 19

for id in idls_prem do

sat, field = check_identity_partial(.4, id) if sat = False then backtrack (,4) break

if sat = None then update(«4, field) break

else

sat, field = check_identity_partial(.A, id_conc) if sat = True then backtrack(.4.) continue

if sat = None then update(»4, field) continue

if sat = False then [_ return .4

Алгоритм 1:1^_а^еЬга

Построение импликативной теории алгебраических тождеств удалось полностью завершить, доказав все импликации, находящи-

еся в каноническом базисе импликаций построенного контекста. Результаты исследования представлены в разделе 4.4. Программный код, тесты к программному коду, получившийся контекст, базис импликаций, а также доказательства импликаций из базиса импликаций вынесены в приложение к диссертационной работе. Требования, предъявляемые к разработанным и реализованным автором методам, заключались в следующем: построить импликативную теорию 70 выбранных тождеств и получить доказательства всех импликаций из базиса импликаций. Требования были выполнены.

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

1. Получено развитие подходов, ранее используемых для автоматизации процессов построения импликативной теории свойств функций на множествах. Разработаны методы автоматизации построения импликативной теории алгебраических тождеств,

2. Разработаны и программно реализованы алгоритмы, которые позволяют проверить, удовлетворяются ли тождества, а также - порождать неизоморфные алгебры на конечных носителях.

3. Разработан метод и реализован алгоритм нахождения алгебры на бесконечном носителе, удовлетворяющей некоторому множеству тождеств и не удовлетворяющей одному выбранному тождеству.

4. С использованием только программных средств построена им-пликативная теория для всех 70 алгебраических тождеств длины не более 5. Созданное программное обеспечение удовлетворяет предъявляемым к нему требованиям.

В главах 3 и 4 появление ошибок в содержаниях объектов удалось исключить вследствие того, что математически определены признаки контекстов и алгоритмизирована их проверка. Однако показано, что не во всех случаях такое возможно. Например, информация о связях объектов и признаков, найденная в глобальной сети Интернет, не может считаться надежной и отсутствие ошибок га-

рантировать нельзя. В случае проведения исследований методами АФП в политологии, эксперты не всегда могли сойтись во мнении относительно того или иного объекта и признака.

Еще более остро необходимость решения задачи нахождения ошибок в новых объектах контекста встает тогда, когда предполагается одновременный доступ к контексту несколькими пользователями. В таком случае некоторые пользователи могут попытаться намеренно испортить исследование путем добавления новых объектов, содержащих ошибки. На настоящее время в рамках АФП не предложено ни одного подхода к решению этой задачи. Метод нахождения ошибок в новых объектах контекста мог бы расширить область применения АФП на более широкий круг задач, в том числе - на описанные выше, и, тем самым, способствовать появлению новых возможностей для их решения.

В рамках АФП нет никаких внутренних ограничений на содержания объектов, поэтому любой объект может иметь любое содержание, начиная от пустого множества и заканчивая всем множеством признаков. Такие ограничения могут, однако, быть присущи предметной области, а, следовательно, являются внешними по отношению к АФП. Конечно, ничто не мешает использовать внешние ограничения при добавлении новых объектов к контексту. При этом можно проверять содержание всех новых объектов на предмет удовлетворения внешним ограничениям. Однако в таком случае эксперт должен заранее сформулировать весь набор ограничений, чтобы гарантировать отсутствие ошибок. Таким образом, эксперту необходимо задать логические правила, которые описывают все невозможные комбинации признаков в предметной области. Такая задача крайне сложна для решения и, в общем случае, она сравнима с построением всей импликативной теории вручную. Кроме того, при подобном подходе не учитывается специфика описания предметной области, принятая в АФП, а также уже накопленные знания (объекты, которые уже введены в контекст). По этой причине в рамках данной работы упомянутый подход не рассматривается.

Сущности в АФП задаются прагматическим образом, а именно

- через взаимодействие с другими сущностями. По этой причине любая информация, полученная из названия объекта, будет внешней по отношению к АФП. Любой подход, основанный на использовании названия объекта, не может быть общеприменимым для всех формальных контекстов. Таким образом, не может ставиться задача нахождения верного описания, исходя из названия объекта. Все, что при таком подходе можно гарантировать, это отсутствие такой комбинации формальных признаков в содержании формального объекта, которая не встречается ни в одном реальном объекте из предметной области. Такого условия, однако, достаточно для построения импликативной теории предметной области, так как сами названия объектов не играют для нее никакой роли.

С другой стороны, как отмечалось в разделе 2.2, множество всех верных импликаций эквивалентным образом представляет формальный контекст. Как следствие, для учета уже накопленных знаний при нахождении ошибок можно использовать множество всех верных импликаций контекста. Кроме того, работа с импликациями для пользователя в общем проще и интуитивно понятнее, так как изначально импликации призваны строго математически формализовать условное высказывание, привычное в обычной жизни. Для пользователя легче ответить на вопрос, выполняется ли импликация в предметной области, чем искать неверные значения в таблице или записывать все возможные правила о том, чего не может быть.

В других областях наук, отличных от АФП, задача нахождения ошибок имеет длинную историю изучения. К сожалению, разработанные методы неприменимы в АФП из-за специфики работы с бинарными таблицами. Краткое описание существующих подходов, а также обоснование необходимости разработки нового метода в рамках АФП, приведено в разделе 5.1.

В пятой главе впервые приводится классификация возможных ошибок в содержаниях формальных объектов через зависимости предметной области (раздел 5.2.1). Выделено четыре возможных типа ошибок, являющиеся следствием нарушения зависимостей предметной области.

1. А ->■ 6;

2. А Ь;

3. А-^ЬУ с,

4. А —Ф, где Ф - любая логические формула кроме представленных выше, например, Ф = а V (Ь Л с).

Далее рассматриваются только типы 1 и 2, так как они являются наиболее простыми и часто встречающимися.

В разделе 5.2.2 автором на основе проведенной классификации возможных ошибок предложены два разных подхода к нахождению ошибок в содержаниях формальных объектов. Один из них основан на использовании базиса импликаций формального контекста, другой - на вычислении замыканий подмножеств содержания объекта. Так как замыкание может быть вычислено быстро, большее внимание уделено второму подходу. Изначально оба подхода позволяют находить только один тип ошибок. Для подхода, использующего замыкания для выявления ошибок, автору удалось предложить модификацию, позволяющую использовать подход для нахождения еще одного типа ошибок. Модификация, доказательство корректности получаемых результатов, а также алгоритм работы представлены в разделе 5.2.4.

Утверждение 5.2.1 Преть К = (в, М, I), А С М. Множество 1А = {В I Ве МСА,в,ев"\Аи А\В},

где МСА = {В е СА\$С 6 СА : В С С} и СА = {А Г) д' | д е С}, является таким множеством всех атомарных импликаций (или их следствий с некоторыми признаками, добавленными в посылку), имеющих вид зависимостей Типов 1 и 2, что они верны в контексте К, не удовлетворяются А и имеют ненулевую поддержку.

Алгоритм выглядит следующим образом.

Input: К = (G, M, I), А С M.

Output: Импликации, которые противоречат А.

1 if А" = A then

2 return 0

3 Candidates = {object' П А | object € G}

4 Candidates = {С 6 Candidates | $В е Candidates: С С В}

5 Result 0

в for Candidate in Candidates do

7 Result.add({Candidate d \

_ d e (Candidate" \ A U A \ Candidate)})

8 return Result

Алгоритм 2: inspect_direct

Утверждение 5.2.2 Временная сложность алгоритма 2 составляет 0(|G|2 х |М|2).

В разделе 5.2.5 сравниваются результаты работы обоих предложенных выше подходов на примере из раздела 5.2.3, на случайных контекстах и на реальных данных. Метод нахождения ошибок, предложенный в настоящей главе, допускает другое более наглядное представление через диаграмму решетки (раздел 5.3). Завершает изложение методов нахождения ошибок в содержаниях формальных объектов раздел 5.4, в котором приведен исходный код с комментариями о его структуре, а также тесты, использованные для проверки работы исходного кода.

В пятой главе автором также предложено одно из возможных нетривиальных применений разработанных методов для отладки исходного программного кода. Подход излагается в разделе 5.5, приводится пример применения метода. В разделе 5.6 представлен исходный код, который использовался для реализации предложенного способа отладки исходного программного кода, а также тесты к нему.

Основными результатами, представленными в пятой главы, являются решения следующих задач.

1. Приведена классификация возможных ошибок в бинарных

данных с помощью представления этих ошибок через зависимости в предметной области.

2. На основе проведенной классификации ошибок предложены два метода нахождения ошибок. Отмечено, что один из них находит результаты за меньшее время. Доказано, что этот метод приводит к нахождению нарушенных взаимосвязей, которые до этого выполнялись хотя бы для одного объекта из контекста.

3. Разработаны модификации более быстрого метода, позволяющие находить ошибки двух классов. Доказана корректность результатов.

4. Разработан и программно реализован интерактивный полиномиальный алгоритм нахождения ошибок в бинарных данных. Получена характеризация в виде модифицированного метода ближайших соседей.

5. Проведены эксперименты по оценке качества нахождения ошибок, а также - по скорости работы на случайных данных и на реальных данных.

6. Основываясь на методе нахождения ошибок предложен способ нахождения ошибок в исходном программном коде.

В рамках исследования импликативной теории свойств функций на множествах разработаны общие подходы к автоматизации процесса такого исследования. В результате дальнейшего развития и улучшения ранее разработанных подходов в рамках исследования алгебраических тождеств автору удалось в автоматическом режиме построить импликативную теорию всех 70 алгебраических тождеств длины не более 5. Необходимо отметить, что результат получен за счет комбинирования прагматического подхода, характерного для АФП, и учета структуры предметной области, позволяющей находить контрпримеры к получаемым импликациям. Разработанные методы нахождения ошибок в бинарных данных позволяют расширить область применения разработанных методов автоматического построения импликативных теорий на тот случай, когда достовер-

ность данных нельзя гарантировать, однако с данными работает эксперт в предметной области.

В заключении представлены основные результаты работы.

1. Разработаны и программно реализованы методы автоматизированного изучения импликативных взаимосвязей между свойствами функций на множествах. Испытания программных средств подтвердили их работоспособность.

2. Построено множество импликативных взаимосвязей между свойствами функций на двух-, трех- и четырехэлементных множествах. Получены доказательства части импликаций из базиса импликаций, составлен список недоказанных и не опровергнутых импликаций (открытых вопросов).

3. Разработаны и программно реализованы: методы автоматизированного построения импликативных взаимосвязей между алгебраическими тождествами, алгоритмы проверки выполнения алгебраических тождеств; нахождения алгебр на бесконечном носителе, удовлетворяющих некоторому множеству тождеств и не удовлетворяющих некоторому одному тождеству. Испытания программных средств подтвердили их работоспособность.

4. Построено множество всех истинных импликативных взаимосвязей между алгебраическими тождествами длины не более пяти. Получены доказательства всех импликаций из базиса импликаций.

5. Разработан метод нахождения ошибок в бинарных данных. Получено доказательство того, что разработанный метод удовлетворяет предъявляемым к нему требованиям. Программно реализован интерактивный полиномиальный алгоритм нахождения ошибок в бинарных данных. Проведенные тестовые испытания подтвердили его работоспособность.

Благодарности

Автор выражает глубокую благодарность научному руководителю, доктору физико-математических наук Сергею Олеговичу Кузнецову за постановку задач, постоянное внимание и помощь в работе. Автор выражает глубокую благодарность профессору Васенину Валерию Александровичу за плодотворные обсуждения, критические замечания и помощь в работе. Автор выражает глубокую благодарность профессору Бернарду Гантеру за плодотворное обсуждение и внимание к работе.

Список публикаций автора

[1] A. Revenko. Debugging programs using formal concept analysis. In FCAIR 2013, pages 105-112. CEUR, 2013, 0.8 п. л. (личный вклад 0.8 п. л.).

[2] A. Revenko. Debugging program code using implicative. In FCA4AI 2013, pages 27-39. CEUR, 2013, 1 п.л. (личный вклад 1 п. л.).

[3] A. Revenko and S.O. Kuznetsov. Attribute exploration of properties of functions on ordered sets. In Proc. 7th International Conference on Concept Lattices and Their Applications, University of Sevilla, pages 311-324, 2010, 0.9 п. л. (личный вклад 0.6 п. л.).

[4] A. Revenko and S.O. Kuznetsov. Finding errors in new object intents. In CLA 2012, pages 151-162. CEUR, 2012, 1 п.л. (личный вклад 0.8 п. л.).

[5] A. Revenko and S.O. Kuznetsov. Attribute exploration of properties of functions on sets. Fundamenta Informaticae, 115(4):377—394, 2012, 1.2 п. л. (личный вклад 0.7 п. л.).

[6] A. Revenko, S.O. Kuznetsov, and В. Ganter. Finding errors in new object in formal contexts. In FCA4AI 2012, pages 65-72. CEUR, 2012, 0.7 п. л. (личный вклад 0.3 п. л.).

[7] А. Ревенко. Нахождение ошибок в бинарных таблицах данных.

Научно-техническая информация. Серия 2. € Информационные процессы и системы6:10-18, 2013, 1 п.л. (личный вклад 1 н.л.).

Отпечатано в отделе оперативной печати Геологического ф-та МГУ : Тираж 100 экз. Заказ №

Текст работы Ревенко, Артем Викторович, диссертация по теме Теоретические основы информатики

ФГБОУ ВПО Национальный исследовательский университет "Высшая школа экономики"

04201451679 На правах рукописи

РЕВЕНКО Артем Викторович

Построение импликативных зависимостей для аналитического описания

предметных областей и обнаружения

(

ошибок в данных

Специальность 05.13.17 - "Теоретические основы информатики"

ДИССЕРТАЦИЯ

на соискание ученой степени кандидата физико-математических наук

Научный руководитель доктор физико-математических наук

Кузнецов Сергей Олегович

Москва 2013

Оглавление

1 Введение 10

1.1 Анализ формальных понятий............................16

1.2 Обнаружение зависимостей в данных..................20

1.2.1 Предметные области..............................25

1.3 Общее описание работы..................................26

1.3.1 Актуальность......................................26

1.3.2 Цели работы ......................................27

1.3.3 Основные результаты ............................28

1.3.4 Научная новизна..................................29

1.3.5 Практическая ценность..........................30

1.3.6 Апробация..........................................30

1.4 Содержание................................................32

2 Теоретические положения 36

2.1 Основы теории решёток..................................36

2.2 Анализ формальных понятий............................39

2.2.1 Исследование признаков..........................44

2.2.2 Диаграммы решеток..............................50

3 Исследование импликативной теории свойств функций на конечных множествах 53

3.1 Функции и свойства функций............................55

3.1.1 Интерес к изучению свойств функций на конечных множествах ..................................58

3.2 Изменение вида базисов..................................60

3.3 Базисы импликаций......................................63

3.3.1 Различия в базисах импликаций для функций

на множествах размера 2 и размера 3..........75

3.3.2 Доказательства импликаций ....................79

3.3.3 Недоказанные импликации......................83

3.4 Обобщение свойств функций............................84

3.5 Выводы....................................................86

4 Исследование импликативной теории алгебраических тождеств 87

4.1 Многообразия алгебр......................................89

4.2 Алгебраические тождества..............................91

4.3 Алгебры....................................................95

4.3.1 Порождение алгебр на конечном носителе ... 96

4.3.2 Необходимость порождения алгебр на бесконечном носителе..................................98

4.3.3 Порождение алгебр на бесконечном носителе . 100

4.4 Выводы....................................................104

5 Нахождение ошибок в содержаниях формальных объектов 106

5.1 Методы нахождение ошибок в различных областях знаний......................................................109

5.2 Нахождение ошибок в содержаниях формальных объектов ........................................................111

5.2.1 Классификация ошибок..........................112

5.2.2 Нахождение ошибок..............................114

5.2.3 Пример ............................................115

5.2.4 Доказательство корректности и улучшения . . 119

5.2.5 Результаты поиска ошибок ......................125

5.3 Другое представление метода нахождения ошибок . . 130

5.4 Нахождение ошибок в исходном коде программы . . . 132

5.4.1 Ошибки в исходном программном коде .... 132

5.4.2 Отладка с помощью методов АФП..............134

5.4.3 Выводы............................................139

Заключение 141

Литература 143

Приложение 152

Список иллюстраций

1.1 Дерево принятия решения играть ли на улице в теннис 23

2.1 Контекст выпуклых четырехугольников Kq...... 47

2.2 Контекст выпуклых четырехугольников Кц, дополненный прямоугольным четырехугольником...... 48

2.3 Контекст выпуклых четырехугольников Кц, дополненный прямоугольным четырехугольником и прямоугольной равнобедренной трапецией.......... 49

2.4 Диаграмма решетки контекста функций на множестве

М2............................. 52

3.1 Исходный контекст из примера 3.2.2.......... 63

3.2 Контекст с добавлением контрпримера из примера 3.2.2 63

3.3 Редуцированный контекст функций на множестве 67

3.4 Редуцированный контекст функций на множествах

М2, М3 и М4....................... 68

3.5 Диаграмма решетки контекста функций на множествах М2, М3 и М4.................... 69

5.1 Расширенный контекст выпуклых четырехугольников

Ко............................. 117

5.2 Контекст ошибок Ке................... 118

5.3 Сравнение времен работы реализаций методов inspect_direct и inspect_dg на случайных контекстах........................... 129

5.4 Поиск ближайших соседей в решетке понятий .... 131

5.5 Контекст с успешными запусками функции remove_html_markup ................... 137

Контекст с неуспешными запусками функции гетоуе_11"Ьт1_тагкир...................

Список таблиц

1.1 Таблица истинности материальной импликации в

классической двузначной логике............. 13

5.1 Сравнение времен работы реализаций методов з.11зрес1;_с1:1ге^ и 1пзрес1:_с^ на реальных данных из хранилища 11С1..................... 130

Список листингов

5.1 Функция remove_html_markup............. 135

Список алгоритмов

4.1 check_ identity..............................................92

4.2 find_algebra ................................................102

5.1 inspect_direct ..............................................123

1 Введение

Историческую основу современной логики образуют две теории дедукции, созданные в 4 в. до н. э. древнегреческими мыслителями: одна — Аристотелем, другая — его современниками и философскими противниками, диалектиками мегарской школы. Преследуя одну цель — найти "общезначимые" законы логоса, о которых говорил Платон, они двигались разными путями к этой цели. Аристотель [67] на своем пути создал весьма ограниченную по своим возможностям, но зато законченную теорию - силлогистику. Силлогистика (от греч. "выводящий умозаключение") - теория логического вывода, исследующая умозаключения, состоящие из так называемых категорических высказываний (суждений). Высказывание, в котором утверждается, что все предметы класса обладают или не обладают определенным свойством, называется общим (соответственно, общеутвердительным или общеотрицательным). Высказывание, в котором утверждается, что некоторые предметы класса обладают или не обладают определенным свойством, называется частным (соответственно частноутвердительным или частноотрица-тельным). По Аристотелю, все простые высказывания делятся на следующие шесть типов: единичноутвердительные; единичноотри-цательные; общеутвердительные; общеотрицательные: частноутвер-дительные; частноотрицательные. Аристотелев силлогизм - это схема для логического вывода, состоящая из трех простых высказываний, каждое из которых принадлежит одному из определенных выше типов. Первые два высказывания называются основаниями, третье - выводом.

Задача аристотелевой силлогистики, блестяще решенная самим Аристотелем, состоит в том, чтобы обнаружить все те силлогизмы

(схемы умозаключений), которые справедливы, то есть представляют собой логические следования. Таких силлогизмов, как установил Аристотель, имеется ровно 19, остальные — неверны. При этом 4 из 19 правильных силлогизмов оказываются условно правильными. В рамках силлогистики впервые была реализована идея алгоритмизации вывода заключений. В качестве доказывающего правила в верных силлогизмах применяется введенное Аристотелем основное правило вывода в исчислении высказываний "отделение вывода" (разрешающее при истинности высказываний "А" и "если А, то В" "отделить" высказывание "В", modus ponens в современной нотации). Разберем пример.

Пример 1.0.1.

Каждый человек смертен.

Сократ человек.

Сократ смертен.

Первое основание силлогизма ("Каждый человек смертен.") представляет собой общеутвердительное высказывание. Чтобы непосредственно применить правило отделения вывода, первое высказывание можно переформулировать таким образом: "Если (кто-то) человек, то (он) смертен." Второе высказывание - единичноутверди-тельное, устанавливает факт того, что Сократ является человеком. Из этих двух оснований можно "отделить" единичноутвердительный вывод о том, что Сократ смертен.

Несмотря на значимость доказывающего правила, в настоящей работе ключевую роль играет понятие условного высказывания ("если А, то В"), или, в терминах Аристотеля, общеутвердительное высказывание. Условное высказывание тесно связано с законом отделения вывода, однако не следует их путать. Условное высказывание, как логическое выражение, может само принимать значения истины или лжи. Отделение вывода (правило вывода) утверждает, что во всех случаях, когда исходные основания верны ("А" и "если А. то В"), вывод также будет верным ("Б"). Вернемся к Примеру 1.0.1, выводящему смертность Сократа. Из двух оснований: смертности л ro-

дей и того, что Сократ является человеком, устанавливается факт, что Сократ смертен. Для установления этого факта было использовано правило отделения вывода. Истинность вывода зависит лишь от истинности условий, но не от самого правила. В этом примере, как упомянуто выше, присутствует и условное высказывание "Если человек, то смертен". В отличие от правила отделения вывода, можно говорить об истинности или ложности условного высказывания. В данном случае, исходя из всех имеющихся сведений, условное высказывание является истинным.

Разберем другой пример, где в качестве одного из оснований выступает неверное утверждение.

Пример 1.0.2.

Все лебеди белые.

Сигнус Атратус лебедь.

Сигнус Атратус белый.

В данном случае устанавливается факт того, что Сигнус Атратус имеет белый окрас. Однако, данный факт не является верным (Сигнус Атратус - вид лебедей, обладающих черным окрасом). Хотя правило отделения вывода и применено корректно, условное высказывание, лежащее в основе правила, является ложным (не все лебеди белые).

Обратимся теперь к философским оппонентам Аристотеля -философам из Мегары. Известно, что основатель мегарской философской школы Евклид из Мегары широко использовал доказательства от противного и аргументы, по форме близкие к силлогическим, и таковы многие дошедшие до нас софизмы мегариков, например, софизм Евбулида из Милета "Рогатый":

Что ты не потерял, ты имеешь. Рогов ты не терял. Стало быть, ты рогат.

Последователи Евклида Диодор Крон из Иаса и его ученик Филон из Мегары [75, 74], считая, что заключения "о присущем", выражаемые фигурами силлогизма, нуждаются в более общей осно-

ве, впервые в истории обратились к детальному анализу условных высказываний. Уже при первом рассмотрении были отмечены некоторые спорные аспекты этого понятия. В частности, соглашаясь в том, что условное высказывание истинно, когда заключение следует из посылки, Диодор Крон и Филон расходились, однако, в толковании понятия "следует". Филон полагал, что условное высказывание "если А, то В" полностью определяется сводом истинностных значений. Таблица истинности материальной импликации задается следующим образом ("И" - истинно, "Л" - ложно):

Ж # а - я мЛ -ИД !

и ч И

л

?и1 # * и

м * * и

Таблица 1.1: Таблица истинности материальной импликации в классической двузначной логике.

В современной науке редко используют термин "условное высказывание". Чаще используют более поздний термин "импликация", который берет начало в латинском языке от слова "¡трНса^о", означающего "связь"; импликация обозначает конкретный тип связи, по своему применению приближенного к условному высказыванию "если А, то В"; А называют посылкой импликации. В - заключением. Определенное Филоном условное высказывание носит название "материальной импликации". Как следует из Таблицы 1.1, материальная импликация является ложной только в том случае, если А истинно, а В ложно. Следует отметить, что таким образом определенная материальная импликация не лишена парадоксов. В частности, выделяют следующие парадоксы (в данной работе для обозначения

логического отрицания используется горизонтальная черта над символом, например, а):

1. а —У (а —Ь), из ложной посылки следует любое утверждение;

2. а —> (Ь —> а), верное заключение следует из любой посылки;

3. (а —6) V (6 —> с), в некотором смысле, этот пункт является комбинацией двух предыдущих, ведь если Ь истинно, то оно следует из любого а (по 2), а если Ь ложно, то из него следует любое с (по 1);

4. (а —)■ Ь) —>■ (аЛб), если одно утверждение не является следствием другого, то первое обязательно истинно, а второе ложно.

Данные парадоксы являются следствием строгого функционального определения импликации, не учитывающего содержания утверждений. Данный аспект был отмечен еще учителем Филона Диодором, который утверждал, что В следует из А, когда условное высказывание "если А, то В" необходимо, так что нельзя утверждать в зависимости от случая, что иной раз оно истинно, а иной раз нет, если А и В одни и те же высказывания. Хотя и другие авторы предлагали другие виды импликаций (например, "строгая импликация" [17] или "релевантная импликация" [6]), позволяющие избежать описанных выше парадоксов, материальная импликация остается наиболее популярной трактовкой импликации. Это связано прежде всего с простотой ее определения (таблица истинности) и интерпретации.

Рассматриваемые в рамках данной работы импликации имеют строго определенную структуру. В них не встречаются дизъюнкции импликаций (как в Парадоксе 3) или отрицание импликации в посылке (как в Парадоксе 4). Парадокс 2 не доставляет затруднений, ведь импликации с безусловно верными утверждениями редко представляют интерес. Затруднения возникают лишь с Парадоксом 1, учет которого требует в некоторых случаях дополнительного рассмотрения (см. раздел 5.2.4).

Для обозначения импликации используются разные символы,

например: Э,—(стрелки могут быть направлены и в другую сторону). Далее в данной работе, за исключением специально оговоренных случаев, используется термин "импликация" в значении именно материальной импликации, а для обозначения импликации используется символ "—>■".

Таким образом импликации являются удобной формой для описания логических взаимосвязей между исследуемыми сущностями. Интересно, что в рамках классической двузначной логики, используя только две логические связки: импликацию и отрицание - можно выразить любое логическое утверждение. Более привычным является, однако, описание объектов через присущие им черты, чем через перечисление тех черт, которыми они не обладают. Поэтому, хотя большинство методов, используемых в данной работе, могут быть тривиально адаптированы для работы и с отрицаниями, с целью сохранения простоты и интуитивности интерпретации преимущественно рассматриваются импликации без отрицания. Исключение составляет методы нахождения ошибок (глава 5), в которых для полноты нахождения ошибок рассматриваются импликации с отрицаниями в заключении.

Еще перед выбором сущностей для изучения выбирают некоторую предметную область - область знаний, в рамках которых предполагается описывать изучаемые сущности и их признаки. В данной работе изучаются методы построения взаимосвязей в предметной области для ее структуризации и нахождения внутренних закономерностей. С этой целью ищется множество всех верных им-пликативных зависимостей между изучаемыми признаками сущностей предметной области. Как уже отмечалось ранее, рассматриваются импликации без отрицания, хотя обобщение тривиально, но нецелесообразно. Описанное множество всех истинных в предметной области импликаций обозначается в настоящей работе термином "импликативная теория". В импликативной теории предметной области содержатся все истинные импликации и не содержится ни одной ложной импликации.

Важность и общность такого подхода видны на примере био-

логической систематики - научной дисциплины, в задачи которой входит разработка принципов классификации живых организмов и практическое приложение этих принципов к построению системы. Построение импликативной теории биологических видов - основная задача биологической систематики. Пример импликации, входящей в импликативную теорию биологических видов:

{жилкование сетчатое, две семядоли, количество частей

цветка кратно четырем, корневая система стержневая}

—У класс: двудольные.

1.1 Анализ формальных понятий

В последнее время широкое распространение получили различные инструменты для автоматического доказательства и проверки им-пликативных (и не только) связей в предметных областях [20, 47, 11]. Однако до начала нахождения доказательств теорем и до проверки их правильности необходимо породить гипотезы. Выдвижение гипотез является наиболее творческой частью построения теории и потому наиболее трудно алгоритмизируемой. От содержания этих гипотез зависит, насколько "интересной" будет разработанная теория, от "полноты" множества доказанных теорем зависит степень разработанности теории. Эту задачу позволяет решить Анализ Формальных Понятий (АФП) - область на стыке математики, информатики и философии [31]. Стандартным представлением данных в АФП является бинарная таблица (формальный контекст), содержащая отношения между множеством (формальных) объектов и (формальных) признаков. Отношение формализует наличие или отсутствие у объекта соответствующего признака. Далее по этому отношению строится алгебраическая решетка, называемая "решеткой понятий".

Интересно отметить общий философский подтекст, присущий как материальной импликации, так и АФП. В случае работы с материальной импликацией, нет необходимости учитывать внутреннюю природу или структуру исследуемой сущности, ведь матер