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

• Петухова Нина Дмитриевна
• кандидат наук
• 2016

Оглавление диссертации кандидат наук Петухова Нина Дмитриевна

ВВЕДЕНИЕ

Степень достоверности и апробация результатов

Публикации результатов

Положения, выносимые на защиту

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

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

ГЛАВА 1. ОБЗОР СОВРЕМЕННОГО СОСТОЯНИЯ ПРЕДМЕТНОЙ ОБЛАСТИ

1.1. Постановка задач Искусственного Интеллекта при логико-предметном подходе

1.2. Обратный метод С.Ю. Маслова для решения задач логико-предметного распознавания образов

Общая схема обратного метода

1.3. Алгоритмы Муравья

1.4. Параллельные вычисления

1.5. Совместное применение идей муравьиных алгоритмов и параллельных вычислений

1.6. Понятие неполной выводимости предикатных формул

ГЛАВА 2. АДАПТАЦИЯ ОБРАТНОГО МЕТОДА МАСЛОВА РЕШЕНИЯ

ЗАДАЧ ЛОГИКО-ПРЕДМЕТНОГО РАСПОЗНАВАНИЯ ОБРАЗОВ

2.1. Формулировка обратного метода для решения задач логико-предметного распознавания образов

2.2. Алгоритм IMA (InverseMethodAlgorithm), использующий тактику обратного метода

Алгоритм IMA (Inverse Method Algorithm)

2.3. Оценка числа шагов работы алгоритма IMA

ГЛАВА 3. АЛГОРИТМ, ОСНОВАННЫЙ НА ПРИМЕНЕНИИ ОБРАТНОГО

МЕТОДА, МУРАВЬИНЫХ ТАКТИК И ПАРАЛЛЕЛЬНЫХ ВЫЧИСЛЕНИЙ

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

Алгоритм IAPTA

3.2. Оценка числа шагов работы алгоритма IAPTA

ГЛАВА 4. ВЫДЕЛЕНИЕ МАКСИМАЛЬНОЙ ОБЩЕЙ ПРЕДИКАТНОЙ

ПОДФОРМУЛЫ С ПОМОЩЬЮ ОБРАТНОГО МЕТОДА МАСЛОВА

4.1. Использование обратного метода для решения задачи выделения максимальной общей подформулы

4.2. Алгоритм PHIAPTA (PartialHatchabilityInverseAntParallelTacticAlgorithm) выделения максимальной общей подформулы

4.3. Оценка числа шагов работы алгоритма PHIAPTA

ЗАКЛЮЧЕНИЕ

ЛИТЕРАТУРА

ПРИЛОЖЕНИЕ А. Пример решения задачи с помощью алгоритма IMA

ПРИЛОЖЕНИЕ B. Пример решения задачи с помощью алгоритма IAPTA

ПРИЛОЖЕНИЕ C. Пример решения задачи выделения наибольшей общей

подформулы с помощью алгоритма PHIAPTA

Введение диссертации (часть автореферата) на тему «Разработка и оценка числа шагов работы алгоритмов решения задач логико-предметного распознавания образов с использованием тактик обратного метода Маслова»

ВВЕДЕНИЕ

Актуальность темы исследования.Во многих задачах искусственного интеллекта исследуемый объект характеризуется не только своими глобальными признаками, задающими его свойства как единого целого, но и свойствами его частей и отношений между ними. При распознавании контурного изображения объект может быть представлен как множество его вершин и вида соединений этих вершин[19], [72], [76], [78], [83], [93]. В задачах диагностики объект задаётся набором своих составляющих, а также зависимостями между этими элементами, позволяющими объекту функционировать [1],[10], [11], [12], [31], [32], [63].

Такой подход ещё в 70-ые годы XX века был сформулирован в литературе (см., например,[29], [60], [64], [70], [94]). Однако практического применения он почти не получил в силу высокой вычислительной сложности возникающих при этом задач, которые являются ^-трудными [2], [17], [90].

При изучении алгоритмов одно из ключевых мест занимает анализ времени их работы[36], [50], [71],[89],[92]. Первым шагом является нахождение асимптотических оценок: верхней и нижней границ работы алгоритмов [15], [23], [43], [44].

В настоящее время для множества задач найдены только такие алгоритмы, которые перебирают экспоненциально зависящее от длины записи исходных данных количество вариантов. Такие задачи, как правило, являются ИР--трудными [24]. Ясно, что при больших размерах решаемых задач применение алгоритмов с экспоненциальной оценкой иррационально, хотя для задач небольшого объема экспоненциальные решения могут оказаться лучше полиномиальных (например, при п>100 экспоненциальная оценка 1.1п лучше, чем 10п3)[73].

В данной работе построены и доказаны оценки числа шагов алгоритмов решения задач логико-предметного распознавания образов, использующих тактики обратного метода, который был предложен в середине 60ых годов советским логиком С.Ю. Масловым (1932 - 1983).

Обратный метод С.Ю. Маслова не является менее эффективным методом автоматического доказательства теорем, чем, например, метод резолюций [26], [33], [35],[52]. При практическом применении, как показано в диссертации, он является даже более эффективным, но не получил широкого распространения в программировании. Одной из причин этого является сложность реализации обратного метода в оригинальном изложении С.Ю. Маслова[34].

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

Степень разработанности темы исследования. Термин «обратный метод» впервые введен С.Ю. Масловым в 1964 году в работе [55]. В этой работе автором был разработан метод установления выводимости для формул классического исчисления предикатов без равенства и функциональных символов.

Интерес к обратному методу установления выводимости появился в связи с серией работ С.Ю. Маслова и группы математической логики ЛОМИ АН СССР: [25], [52], [53], [54], [56], [57] и [58].

В 1973 году Н. Нильсон написал книгу, посвященную методам поиска решений в пространстве состояний [60]. В 1976 году Р. Дуда и П. Харт изложили и систематизировали методы распознавания образов и дали анализ пространственных сцен по их плоскому изображению [28]. В 1981 году Г.Е. Минц, назвав обратный метод «резолютивными исчислениями», применил его к неклассическим пропозициональным логическим исчислениям. В 1982 году М. Гэри и Д. Джонсон написали книгу, посвященную вопросам сложности решения задач [24].В работе [59] обратный метод, хоть и названный «резолютивными исчислениями» впервые применяется к неклассическим пропозициональным логическим исчислениям.В [18] обратный метод рассматривается для

классической логики без равенства на основе обратного исчисления свободных переменных. В 1989 году выходит работа В. Лифшица в которой представлены основные идеи обратного метода в форме, подчеркивающей его связь с методом резолюций [99]. В 1992 году, в работе [105] приводится описание обратных исчислений свободных переменных для неклассических предикатных логик. Метод свободных переменных для классической логики с равенством, а также ряд критериев избыточности были введены в работе [85]. Реализация обратного метода для предикатной интуиционистской логики описана в работе [104].В 2001 году Дягтерев А.Н. и Воронков А.А. подвели некоторое обобщение в книге [86].

В период с 2000 по 2001 год В.В. Бурлуцким был написан ряд работ, посвященных логическому выводу в модальных системах и реализации обратного метода для модальных логик КТ и S5 [3], [4], [5], [6], [7], [8], [9]. В 2004 году В.П. Оревков применил обратный метод и доказал разрешимость нового хорновского фрагмента исчисления предикатов [62]. В ряде работ Д.С. Ларионова [45], [46], [47], [48], [49], [98] была разработана конкретизация обратного метода для автоэпистемической логики, которая применялась при построении экспертных систем.Г.Е. Минц в 2010 году доказал разрешимость класса Е, используя обратный метод [100]. Кроме того, в 2010 году была предложена реализация обратного метода с применением оператора получения благоприятного набора [79]. А в 2015 году В.А. Филипповским была предложена и реализована система автоматического поиска доказательств теорем, основанная на обратном методе, а также проведено сравнение обратного метода и метода резолюций [77].

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

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

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

3. На основе сформулированного метода разработать алгоритм решения задач логико-предметного распознавания образов.

4. Модифицировать этот алгоритм, используя тактики муравьиных алгоритмов и параллельных вычислений.

5. Использовать последний алгоритм для решения задачи нахождения наибольшей общей подформулы.

6. Получить асимптотические оценки всех построенных алгоритмов.

Цели и задачи диссертационной работы соответствуют области исследований паспорта специальности 05.13.17 - «Теоретические основы информатики»: пунктам 2 (Исследование информационных структур, разработка и анализ моделей информационных процессов и структур), 5 (Разработка и исследование моделей и алгоритмов анализа данных, обнаружения закономерностей в данных и их извлечениях разработка и исследование методов и алгоритмов анализа текста, устной речи и изображений) и 7(Разработка методов распознавания образов, фильтрации, распознавания и синтеза изображений, решающих правил. Моделирование формирования эмпирического знания).

Объектами исследования диссертационной работы являются формулы исчисления предикатов, к которым сводятся многие задачи искусственного интеллекта, и обратный метод Маслова. Предметом исследования являются разработка и реализация алгоритмов решения задач классификации Искусственного Интеллекта.

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

Научная новизна данной работы заключается в следующем.

1. Сформулирована конкретизация обратного метода для решения задач логико-предметного распознавания образов, допускающих формулировку средствами языка исчисления предикатов.

2. Разработан алгоритм IMA решения задач логико-предметного распознавания образов, основанный на обратном методе. На основе этого алгоритма построен алгоритм IAPTA, использующий тактики муравьиных алгоритмов и параллельных вычислений. Сформулирован алгоритм PHIAPTA для решения задачи нахождения наибольшей общей подформулы. Получены асимптотические оценки всех построенных алгоритмов. Теоретическая и практическая значимость работы. Полученные

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

Степень достоверности и апробация результатов

Результаты диссертационной работы были представлены и обсуждались на научных конференциях: СПИСОК-2012, Санкт-Петербург, Россия, 25-27 апреля 2012; XV Международная научная конференция «Information theories and applications» (ITA 2012), Варна, Болгария, 18 июня-6 июля 2012; СПИС0К-2013, Санкт-Петербург, Россия, 23-26 апреля 2013; XVI Международная научная конференция «Information theories and applications» (ITA 2013), Варна, Болгария, 29 июня-11 июля 2012, СП0С0К-2016, Санкт-Петербург, Россия, 26-29 апреля 2016.

Основные результаты диссертации были получены в рамках выполнения исследований при финансовой поддержке РФФИ (проект 14-08-01276).

Публикации результатов

По теме диссертации опубликовано 7 работ, из них 3 статьи в рецензируемых научных журналах из перечня российских рецензируемых журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание учёных степеней доктора и кандидата наук[41], [68], [65], 2 статьи в зарубежных научных журналах на английском языке [96], [97] и тезисы 2 докладов [66],[67]. В статьях [41], [68] диссертанту принадлежит построение алгоритмов решения задач логико-предметного распознавания образов, основанных на обратном методе Маслова и нахождение асимптотических оценок этих алгоритмов. В статье [65] диссертантом предложено применение построенных ранее алгоритмов для решения задачи нахождения наибольшей общей с точностью до имён аргументов подформулы двух элементарных конъюнкций атомарных формул.

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

Положения, выносимые на защиту

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

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

3. Построен алгоритм PHIAPTA поиска наибольшей общей подформулы, основанный на алгоритме IAPTA. Получены асимптотические оценки числа шагов работы этого алгоритма.

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

Работа состоит из введения, четырех глав, разбитых на разделы подразделы, заключения, списка литературы и трех приложений. Общий объем рукописи составляет 157 страниц текста, включая88 страниц непосредственно текста диссертации и 69 страниц приложений. Текст содержит 21 рисунок. Библиографический список включает 105 наименований.

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

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

В первой главе приведен обзор современного состояния предметной области по рассматриваемой в диссертации теме. В разделе 1.1 рассматривается постановка задач Искусственного Интеллекта при логико-предметном подходе. В разделе 1.2 приведена формулировка обратного метода С.Ю. Маслова для решения задач логико-предметного распознавания образов. В разделах 1.3-1.6 даны обзоры тем алгоритмов муравья, параллельных вычислений и неполной выводимости предикатных формул соответственно.

Во второй главе обратный метод Маслова адаптирован для решения задач логико-предметного распознавания образов, построен алгоритм IMA решения таких задач на основе обратного метода, получены асимптотические оценки этого алгоритма.

В разделе 2.1 разработано применение обратного метода для доказательства выводимости формул вида

/

S

xnA Diak,xn)

i a1,...,ak,xi,...,xn.

Vi = 1

. (1)

Эта формула является частным случаем формул, для которых разработан обратный метод Маслова. В (1) дизъюнкты О-(а,х^хп) имеют вид

П ^^(аак Рк X*и )) , где ^^ Ц — ) - обозначение для

дизъюнкции отрицаний атомарных формул, входящих всписок постоянных атомарных формул£(а,...,^), а Р^ - предикатный символ.

Определение 1. Любой список Г формул вида О (&\г---, ^, С г---, сп)

являетсяГ-набором для формул вида (1), если формулы в этом списке не повторяются.

Определение 2. Пусть - список констант из списка а1 ?—?

|Зl,...,Pl - список переменных и констант из списка а1. Рассмотрим систему равенств:

Га1 = |

- (2)

а\ = !

Пусть и1,..,ир- список без повторений всех переменных, входящих в равенства системы (2). Систему (2) будем называть системой уравнений в переменныхи1,..,ир.Решением системы уравнений (2) будем называть всякий

набор значенийконстант у1?...)Ур из списка такой, что в результате

одновременной замены всех переменных и1,...,ир на константы Ур-.^Ур

соответственно левые и правые части каждого равенства системы совпадут.

Система уравнений (2) не имеет решений, если в списке у1,...,ур

естьповторения, или если в системе уравнений (2) приходится сравнивать разные константы.

Определение 3. F-набор называется пустым а, если все формулы, входящие в него, не имеют переменных и тавтологичны.

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

В разделе 2.2 сформулирован алгоритм IMA (InverseMethodAlgorithm), использующий тактику обратного метода.

Алгоритм IMA (inverse method algorithm)

1. Строим 5-членный F-набор, формулы в котором не повторяются. То есть в формуле (1) удаляем все знаки конъюнкций и составляем список элементарных

дизъюнкций вида v —S(а,..., а^ )v P^ ^,..., хп .

i V i J

2. Присваиваем значения переменным следующим образом:

2.1. Отменяем все пометки об удалениях предикатных формул из S (а) (если они были).

2.2. Берем формулу v-S(а^...,а^)vPk (¿1,...,tm) из рассматриваемого F-

набора, содержащую m-местный предикатный символ такой, что набор t1,...,tm содержит хотя бы одну переменную.

2.3. Ищем в S (а) формулуPfr (vj,...,vm) при наборе констант v1,...,vm с

отрицанием перед выбранным в п. 2.2 предикатным символом. Если нашли подходящую формулу - помечаем её как удаленную и переходим к пункту 2.4, если её не существует, то переходим к пункту 3.

2.4. Решаем систему уравнений, отождествляющую списки переменных

t1,...,tm и констант v1,...,vm . В случае, если эта система имеет решение, перейти к пункту 2.5, если система решений не имеет, то перейти к пункту 2.3.

2.5. Заменяем во всем F-наборе переменные из списка ti,...,tm на их значение, полученные в пункте 2.4.

2.6. В полученном F-наборе удаляем повторения формул.

2.7. Если получился пустой F-набор, то алгоритм заканчивает работу.

2.8. Если получился тупиковый F-набор - перейти к пункту 3.

2.9. Если в F-наборе все формулы, имеющие переменные помечены как удаленные - переходим к пункту 4.

2.10. Если в F-наборе существуют элементарные дизъюнкции, имеющие переменные, которым еще не присвоено значение, то перейти к пункту 2.2.

3. Возвратная часть алгоритма.

3.1. Отменяем последнее действие пункта 2.5, если это возможно, и переходим к пункту 2.3

3.2. Если отмена последнего действия пункта 2.5 невозможна, то помечаем атомарную формулу P^, tm) как удаленную и переходим к пункту 2.

4. Если все формулы помечены как удаленные значит, формула не выводима. Алгоритм заканчивает работу.

В разделе 2.3 получены асимптотические оценки числа шагов работы алгоритма IMA.

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

Пусть l - наибольшее количество аргументов в атомарной формуле; s+1 - количество атомарных формул в каждом из дизъюнктов;

sk - количество вхождений в исходную формулу атомарных формул с k-м

предикатным символом.

Теорема 1. (Нижняя оценка работы алгоритма IMA)Колuчесmво шагов решения задачи искусственного интеллекта, сведённой к доказательству

следствия вида S(а) ^ 3^A(x) при использовании алгоритма IMA, основанного

на тактиках Обратного метода не менее О^!)шагов.

Теорема 2. (Верхняя оценка числа шагов работы алгоритма IMA)Колuчесmво шагов затрачиваемых на решение задачи искусственного интеллекта, сведённой к доказательству следствия вида S(а) ^ 3x_iA(x)при

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

O

i \ 5 • max s-fc 5 • l

шагов.

v k J

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

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

1) присвоение значения переменным;

2) замена всех вхождений переменной на её значение;

3) проверка формул на графическое совпадение;

4) отмена присвоения значения переменным;

5) отмена замены всех вхождений переменной;

6) изменение приоритета данного действия на 0.

В разделе 3.1 сформулирован алгоритм IAPTA, основанный на применении обратного метода, муравьиных тактик и параллельных вычислений.

Алгоритм IAPTA (Inverse Ant Parallel Tactic Algorithm)

1. Строим 5-членный Б-набор, формулы в котором не повторяются. То есть

с \

при

переписываем без конъюнкций все дизъюнкты вида V —Б (ю) V Р^ г = 1,..,ё. Создаем популяцию из 5 процессоров.

Каждой паре потенциально контрарных формул Р^

х1,..., х

V г

с \

х1'...' хп

V г У

и

г \

V г У

входящих в один Б-набор, назначаем приоритет их

отождествления равным 1. Остальные приоритеты назначаем равными 0.

2. Копируем ¿-членный Б-набор 3 - 1 раз. Получаем ровно 5 одинаковых Б-наборов. Назначаем г-му процессору (г = 1,...,^) свою начальную формулу с \

- формулу, с которой данный процессор начинает свой

\

х1,..., хп

V г У

итерационный цикл, и потенциально контрарную ей формулу из Б (ю), имеющую приоритет, равный 1. Если каким-то двум процессорам назначены формулы, начинающиеся с одного и того же предикатного символа (таких формул не более 3), то назначаем для них разные формулы из Б(ю), потенциально контрарные данной.

Если для каких-то двух процессоров не существует разных потенциально контрарных формул, то формула не выводима. Алгоритм заканчивает работу. Иначе, переходим к п. 3.3.

3. Параллельно работают 5 процессоров; г-й процессор (г = 1,...,^) осуществляет присвоение значений переменным.

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

3.2. Ищем среди формул в £(®) формулу-Р

( \ а ] ,..., а.

I

, имеющую

Г \

с

приоритет, равный 1, и потенциально контрарную формуле Р^

IV 1 п У

которой работает этот процессор. Если нашли подходящую формулу, то переходим к п. 3.3. Если ее нет, то переходим к п. 4.

3.3. Решаем систему уравнений вида ц = а . ( = 1,...,п ), унифицирующую

^ I ^

список переменных и констант со списком констант. В случае, если эта система имеет решение, то переходим к п. 3.4. Если система решений не имеет, то понизить приоритет этого действия до 0 и переходим к п. 3.2.

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

3.5. Заменяем в F-наборе каждого процессора вхождения переменных из списка на их значения, полученные в п. 3.3 и 3.4, если успешно пройдена проверка на непротиворечивость.

3.6. Если для какого-либо процессора получился пустой F-набор, то алгоритм заканчивает работу. Формула выводима и найден набор значений переменных, существование которых утверждалось в формуле.

3.7. Если получился тупиковый F-набор, то переходим к п. 4.

3.8. Если для всех процессоров приоритеты всех действий равны 0, то формула не выводима. Алгоритм заканчивает работу.

3.9. Если в F-наборе какого-либо процессора существуют формулы, имеющие переменные, которым еще не присвоено значение, то переходим к п. 3.1.

4. Возвратная часть алгоритма.

4.1. Отменяем последнее действие п. 3.5, если это возможно, и переходим к

п. 3.2.

4.2. Если для какого-либо процессора отмена последнего действия п. 3.5 невозможна, то алгоритм заканчивает работу.

4.3. Если все процессоры закончили работу, но пустой F-набор не получен, то алгоритм заканчивает работу. Формула не выводима.

В разделе 3.2 получены асимптотические оценки числа шагов работы алгоритма 1АРТА

Теорема 3. (Нижняя оценка числа шагов работы алгоритма/ЛРТЛ) Количество шагов доказательства логического следования вида

Б (<х>)^Зхф Л^ (х) и нахождения значений переменных, для которых это

следование имеет место, при использовании алгоритма 1ЛРТЛ, не менее 28(8 + 2) + 2 шагов.

Теорема 4. (Верхняя оценка числа шагов работы алгоритма/ЛРТЛ)

Количество шагов доказательства логического следования вида

Б (<х>)^Зхф Л^ (х) и нахождения значений переменных, для которых это следование имеет место, при использовании алгоритма 1ЛРТЛ составляет

(

с

О

I ■

тах 8^

V к у

шагов.

V у

В четвертой главе рассматривается решение задачи выделения максимальной общей подформулы с использованием алгоритма 1АРТА.

В разделе 4.1 приведена постановка задачи выделения максимальной общей

подформулы двух заданных элементарных конъюнкций Л(х) и Л(у), с точностью до имён переменных, как доказательства логического следования [42]

Л(х)^ЗуЛ(у) с нахождением такой подформулы Л (у ) формулы Л(у), что имеет место следствие Л(хЗу Л(у ), а также общего унификатора А формул

Л(х) и Л (у ), то есть такой подстановки имён переменных у' вместо некоторых имён переменных из списка х, что Л (у ) является подформулой Л(х) после

применения унификатора X.

Если в алгоритме IAPTA заменить действие «присвоение значений переменным» на «отождествление переменных», этот алгоритм можно модифицировать до алгоритма PHIAPTA, и применить и для решения задачи выделения максимальной общей подформулы.

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

Алгоритм PHIAPTA (Partial Hatchability Inverse Ant Parallel Tactic

Algorithm)

1. Строим ¿-членный F-набор, формулы в котором не повторяются. То есть

переписываем без конъюнкций все дизъюнкты вида Л(х)VР^ у|,...,у'п

гV гУ

г = 1,...,8. Создаем популяцию из 8 процессоров.

/ \

Каждой паре потенциально контрарных формул р у|,...,у'п

г V г У

Х1,..., х.

, при

и

kJ

!'...' xn-V J У

, входящих в один F-набор, назначаем приоритет их

отождествления равным 1. Остальные приоритеты назначаем равными 0.

2. Копируем 8-членный F-набор 8-1 раз. Таким образом получаем ровно 8 одинаковых F-наборов. Назначаем г-му процессору (г = 1,...,3) свою начальную

С \

формулу р у|,...,у'п - формулу, с которой данный процессор начинает свой

г

V г У

итерационный цикл, и потенциально контрарную ей формулу вида

-Рк,

J У

из A(x), имеющую приоритет, равный 1. Для каждого

процессора назначаем переменную I/ = 0 (/ = 1,...,^), означающую длину

фрагмента формулы Л(х ) в формуле Л' (у').

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

из Л(х), потенциально контрарные данной. Если для каких-то двух процессоров не существует разных потенциально контрарных формул, берем для них одинаковые потенциально контрарные формулы и переходим к п. 3.3.

3. Параллельно работают 5 процессоров; /-ый процессор (/ = 1,...,^) осуществляет отождествление переменных следующим образом.

3.1. Если в рабочей формуле данного процессора нет переменных, которые еще не проходили процедуру отождествления, то в качестве рабочей для этого процессора выбираем формулу из следующей элементарной дизъюнкции, содержащую хоть одну «не отождествленную» переменную.

/ Л

3.2. Ищем среди формул в Л(х ) формулу ^Рк.

V ] у

имеющую

/ \

приоритет, равный 1, и потенциально контрарную формуле Р^ ,...,? (из

Список литературы диссертационного исследования кандидат наук Петухова Нина Дмитриевна, 2016 год

ЛИТЕРАТУРА

[1] Анисимов, Д.Н. Диагностика динамических объектов методами нечеткой логики с использованием параметров имитационных моделей / Д.Н. Анисимов, О.С. Колосов, Д.В. Вершинин, М.В. Зуева, И.В. Цапенко // Мехатроника, автоматизация, управление - 2010, №10, - С. 45-50, - ISSN 1684-6427

[2] Ахо, А. Структуры данных и алгоритмы / А. Ахо, Д. Хопкрофт, Д. Ульман // Москва: Вильямс, 2009, - 400 с. - ISBN: 978-5-8459-1610-5

[3] Бурлуцкий, В.В. Как сократить пространство поиска для разрешающей процедуры, основанной на обратном методе / В. В. Бурлуцкий // Национальный исследовательский Томский государственный университет, - Томск, 2001, - Деп. в ВИНИТИ РАН 21.09.2001 № 2017-В2001

[4] Бурлуцкий, В.В. Логический вывод в дедуктивных системах. / В.В. Бурлуцкий, В.Б. Новосельцев // Вторая сибирская школа молодого ученого: том 3, Томск: изд-во ТГУ, 2001, - с. 27-41

[5] Бурлуцкий, В.В. Логический вывод в модальных системах на основе обратного метода. / В.В. Бурлуцкий, В.Б. Новосельцев // Труды региональной научно-практическолй конференции студентов, аспирантом и молодых ученых "Вторая сибирская школа молодого ученого" Том 3, Физика, математика, информационные технологии, - Томск: изд-во ТГПУ, 2000, - с. 24

[6] Бурлуцкий, В.В. Применение обратного метода Маслова к системе модальной логики S5. / В.В. Бурлуцкий // Материалы XXXVII Международной научной студенческой конференции "Студент и научно-технический прогресс". Секция математики, - Новосибирск: изд-во НГУ, 1999, - с 18

[7] Бурлуцкий, В.В. Реализация обратного метода для модальной логики знания / В.В. Бурлуцкий // Труды XXIII Конференции молодых ученых механико-математического факультета МГУ, - Москва: изд-во Мех.-мат. Ф-та МГУ, - 2001, - с 66-70.

[8] Бурлуцкий, В.В. Реализация обратного метода для модальной логики КТ / В.В. Бурлуцкий // Исследования по математическому анализу и алгебре: Сборник статей, Томский университет [ТГУ] им. В.В. Куйбышева. -Томск: изд-во ТГУ, 2001, - том 3, - с. 26-32, ISBN 5-946210-10-6

[9] Бурлуцкий, В.В. Стратегия обратного метода вывода для модальной логики КТ, основанная на Ф-упорядочении / В. В. Бурлуцкий // Национальный исследовательский Томский государственный университет, - Томск, 2001, - Деп. в ВИНИТИ РАН 21.09.2001 № 2018-В2001

[10] Вагин, В.Н. Достоверный и правдоподобный вывод в интеллектуальных системах. Монография. / В.Н. Вагин, Е.Ю. Головина // Москва: Физматлит

12

13

14

15

16

17

18

19

20

21

22

- 2008, - 714 с. - ISBN 978-5-9221-0962-8

Вагин, В.Н. Решение задач диагностики с использованием систем поддержки истинности / В.Н. Вагин, Д.С. Зарецкий Известия южного федерального университета. Технические науки, - № 12, том 113, 2010, -с. 63-70, - ISSN 1999-9429

Вагин, В.Н. Эвристические и вероятностные методы снятия эффективных показаний в системах диагностики. / В.Н. Вагин, П.В. Оськин // Известия РАН. Теория и системы управления, - 2006, № 4, - с. 78-93, - ISSN 00023388

Ватутин, Э.И. Анализ результатов применения алгоритма муравьиной колонии в задаче поиска пути в графе при наличии ограничений / Э.И. Ватутин, В.С. Титов // Известия Южного федерального университета. Технические науки. 2014. № 12 (161). с. 111-120 - ISSN 1999-9429 Введение в контурный анализ. Приложения к обработке изображений и сигналов / под ред. Я. А. Фурман //, Москва: ФИЗМАТЛИТ, 2003. - 592 с.

- ISBN 978-5-9221-0374-9

Верещагин, Н. К. Колмогоровская сложность и алгоритмическая случайность / Н. К. Верещагин, В. А. Успенский, А. Шень, // Москва: МЦНМО 2013. - 576 с. - ISBN 978-5-4439-0212-8

Воеводин, В. В. Параллельные вычисления / Воеводин, В. В., Воеводин, Вл. В.//, Санкт-Петербург: БХВ, 2002. - 608 с. - ISBN 5-94157-160-7

Вопросы кибернетики. Вып.131 (проблемы сокращения перебора). Москва, 1987. - ISSN 0134-6388

Воронков, А.А. Метод поиска доказательства / А.А. Воронков // Вычислительные системы. Новосибирск. 1985. - том 107, - ISSN 0568-661X

Генкин, В.Л. Системы распознавания автоматизированных производств / В.Л. Генкин, И.Л. Ерош, Э.С. Москалев //. Москва: Машиностроение, -1988, - 242 с., - ISBN 5-217-00162-3

Гергель, В.П. Высокопроизводительные вычисления для многоядерных многопроцессорных систем / В.П. Гергель // Нижний Новгород: Изд-во ННГУ им. Н.И.Лобачевского, 2010. - 421 c. - ISBN 5-85746-602-4

Гонсалес, Р. Цифровая обработка изображений / Р. Гонсалес, Р. Вудс. // Москва: Техносфера, 2005. - 1072 c. - ISBN 5-94836-028-8 Гонсалес, Р. Цифровая обработка изображений в среде MATLAB: пер. с англ / Р. Гонсалес, Р. Вудс, С. Эддинс // Москва: Техносфера, - 2006, 616 с. - ISBN: 5-94836-092-Х.

Громкович, Ю. Теоретическая информатика. Введение в теорию автоматов, теорию вычислимости, теорию сложности, теорию алгоритмов, рандомизацию, теорию связи и криптографию: учебное пособие / Ю. Громкович, пер. с нем. под ред. Б. Ф. Мельникова. - 3-е изд. // СПб: БХВ-Петербург, 2010. - 336 с. - ISBN 978-5-9775-0406-5

[24] Гэри, М. Вычислительные машины и труднорешаемые задачи / М. Гэри, Д. Джонсон // Москва: Мир, 1982. - 416 с.

[25] Давыдов, Г.В. Машинный алгоритм установления выводимости на основе обратного метода / Г.В. Давыдов, С.Ю. Маслов и др.// Зап. научн. сем. ЛОМИ АН СССР. - 1969, том 16, - С. 8-20

[26] Давыдов, Г.В. Синтез метода резолюций с обратным методом / Г.В. Давыдов //Записки научных семинаров ЛОМИ АН СССР, Т.20, 1971. -ISSN 0373-2703

[27] Джонс, М. Т. Программирование искусственного интеллекта в приложениях / М. Т. Джонс, пер. с англ. Осипов А.И. // Москва: ДМК -Пресс, 2011. - 312 с. - ISBN 5-94074-275-0

[28] Дуда, Р. Распознавание образов и анализ сцен / Р. Дуда, П. Харт // Москва: «МИР», 1976. - 509 с.

[29] Жданов, А.А. Автономный искусственный интеллект / А.А. Жданов // Москва: БИНОМ. Лаборатория знаний, 2015. - 359 с. - ISBN 978-5-94774995-3

[30] Кажаров, А.А. Муравьиные алгоритмы для решения транспортных задач / А.А. Кажаров, В.М. Курейчик // Известия Российской академии наук, Теория и системы управления, 2010, № 1. с. 32-45. - ISSN 0002-3388

[31] Карабутов, H.H. Структурная идентификация статических объектов: анализ информационных структур / Н.Н. Карабутов // - Москва: Книжный дом «Либроком», 2009. - 176 с. - ISBN 978-5-397-00646-0

[32] Карабутов, H.H. Структурная идентификация статических объектов: Поля, структуры, методы / Н.Н. Карабутов // - Москва: Книжный дом «Либроком», 2011. - 152 с. - ISBN 978-5-397-01855-5

[33] Катречко, С.Л. Моделирование правила расщепления в обратном методе С.Ю.Маслова / С.Л. Катречко //Логические методы в компьютерных науках. - Москва: Институт философии РАН, 1992 с. 125-141

[34] Катречко, С.Л. Обратный метод С.Ю. Маслова [Электронный ресурс] / С.Л. Катречко // - Режим доступа: http://www.philosophy.ru/library/ksl/katr_107.doc, свободный, (05.03.2016)

[35] Катречко, С.Л. Обратный метод С.Ю. Маслова и его модификации. / С.Л. Катречко // Логика и компьютер (вып. 2): логические языки, содержащие рассуждения и методы поиска доказательства, - Москва: Наука, 1995, - с. 62-75.

[36] Кормен, Т. Алгоритмы: построение и анализ, 2-е издание/ Т.Кормен, Ч. Лейзерсон, Р. Ривест, К. Штайн // Москва: издательский дом «Вильямс», 2005. - 1296 с. - ISBN 5-8459-0857-4

[37] Косовская, Т. М. Доказательства оценок числа шагов решения некоторых задач распознавания образов, имеющих логические описания / Т.М. Косовская // Вестн. С.-Петербург.ун-та. Сер. 1. 2007. Вып. (4) с. 82 - 90. -ISSN 1025-3106

[38] Косовская, Т. М. Некоторые задачи Искусственного Интеллекта, допускающие формализацию на языке исчисления предикатов, и оценки числа шагов их решения / Т.М. Косовская //Труды СПИИРАН, 2010. Вып. 14. С. 58-75. - ISSN 2078-9181

[39] Косовская, Т. М. Об одном новом подходе к формированию логических решающих правил / Т.М. Косовская, А.В. Тимофеев // Вестник ЛГУ, 1985, №8. - с. 22-27

[40] Косовская, Т. М. Подход к решению задачи построения многоуровневого описания классов на языке исчисления предикатов / Т.М. Косовская // Труды СПИИРАН - 2014. - №3 (34). - С. 204-217. - ISSN 2078-9181

[41] Косовская, Т. М. Решение задач логико-предметного распознавания образов с использованием тактик обратного метода Маслова / Т.М. Косовская, Н.Д. Петухова // Компьютерные инструменты в образовании -2014. - Вып. 3. - с. 9-20. - ISSN: 20712340

[42] Косовская, Т. М. Частичная выводимость предикатных формул как средство распознавания объектов с неполной информацией / Т.М. Косовская // Вестник СПбГУ. Сер. 10. 2009. Вып. 1. С. 74-84. - ISSN 18119905

[43] Крупский, В. Н. Математическая логика и теория алгоритмов / В. Н. Крупский, В. Е. Плиско // Москва: изд. центр «Академия», 2013. - 416 с. -ISBN 978-5-7695-9559-2

[44] Кузюрин, Н. Н. Эффективные алгоритмы и сложность вычислений / Н.Н. Кузюрин, С.А. Фомин // Москва: МФТИ, 2007. - 369 с. - ISBN 5-74170198-1

[45] Ларионов, Д. С. Использование модальной логики для проектирования оболочек экспертных систем / Д.С. Ларионов// Известия Томского Политехнического Университета. - 2005. - Т. 308. - No 4. - С. 173-177, ISSN 2413-1830

[46] Ларионов, Д.С. Модальная логика для механизма вывода экспертной системы / Д.С. Ларионов // Труды XXIV Конференции молодых ученых механико-математического факультета МГУ, - Москва: изд-во Мех.-мат. Ф-та МГУ, - 2002, том I - С. 108-110

[47] Ларионов, Д.С. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом / Д.С. Ларионов // Материалы XXXIX Международной научной студенческой конференции. - 2001. - Новосибирск, НГУ. - С. 194-195

[48] Ларионов, Д.С. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом / Д.С. Ларионов, В.Б. Новосельцев // Математическое моделирование, ИММ РАН, 2002, - том 14, No 9. - С. 48-52 - ISSN 0234-0879

[49] Ларионов, Д.С. Оболочка экспертной системы с прямым и обратным выводом на основе нечетких рассуждений / Д.С. Ларионов // Труды XXIII Конференции молодых ученых механико-математического факультета МГУ, - Москва: изд-во Мех.-мат. Ф-та МГУ, - 2001, том II. - С. 223-229

Левитин, А.В. Алгоритмы: введение в разработку и анализ/ А.В. Левитин // Москва: Издательский дом «Вильямс», 2006. - 576 с. - ISBN: 5-84590987-2

Маслов, С. Ю. Обратный метод и тактики установления выводимости для исчисления с функциональными знаками / С. Ю. Маслов // Труды Математического института АН СССР, 1972, том 121, 14-56 Маслов, С.Ю. Связь между тактиками обратного метода и метода резолюций / С. Ю. Маслов // Зап. научн. сем. ЛОМИ, 1969, том 16, 137146

Маслов, С.Ю. О поиске вывода в исчисленьях общего типа / С.Ю. Маслов // Зап. научн. сем. ЛОМИ АН СССР. - 1972, том 32, - С. 59-65 Маслов, С.Ю. Обобщение обратного метода на исчисление предикатов с равенством / С.Ю. Маслов // Зап. научн. сем. ЛОМИ АН СССР. - 1971, том 20, - С. 80-96

Маслов, С.Ю. Обратный метод установления выводимости в классическом исчислении предикатов / С.Ю. Маслов // Москва, ДАН СССР, 1964, том 159, №1. - С. 17-20 - ISSN 0869-5652 Маслов, С.Ю. Обратный метод установления выводимости для логических исчислений / С. Ю. Маслов // Труды Математического института АН СССР, 1968, ХСУШ, 26-87.

Маслов, С.Ю. Обратный метод установления выводимости для непредваренных формул исчисления предикатов / С.Ю. Маслов // Москва ДАН СССР, 1967, №1, - С. 22-25 - ISSN 0869-5652

Маслов, С.Ю. Применение обратного метода к теории разрешимых фрагментов классических исчислений / С.Ю. Маслов // Москва, ДАН СССР, 1966, №1, - С. 1720 - ISSN 0869-5652

Минц, Г.Е. Резолютивные исчисления для неклассических логик / Г.Е. Минц // 9-ый Советский Кибернетический симпозиум, Москва: ВИНИТИ, 1981, - том 2, - С. 34-36

Нильсон, Н. Искусственный интеллект. Методы поиска решений / Нильсон Н. // Москва: Мир, 1973. - 273 с.

Оревков, В. П. Обратный метод поиска вывода / В.П. Оревков // - В кн.: Адаменко, А.Н. Логическое программирование и Visual Prolog / А.Н. Адаменко, А.М. Кучуков // - Санкт-Петербург: БХВ, 2003. - с. 952-965. -ISBN 5-94157-156-9

Оревков, В.П. Новый разрешимый хорновский фрагмент исчисления предикатов. / В.П. Оревков // Теория сложности вычислений IX, Зап. научн сем. ПОМИ, том 316, - Санкт-Петербург, ПОМИ, 2004, - с. 147-162, - ISSN 0373-2703

Пегат, А. Нечеткое моделирование и управление; пер. с англ / А. Пегат // Москва: БИНОМ. Лаборатория знаний, 2013- 798 с. - ISBN 978-5-99631319-8

[64] Петрунин, Ю.Ю. Философия искусственного интеллекта в концепциях нейронаук. (Научная монография) / Ю.Ю. Петрунин, М.А. Рязанов, А.В. Савельев // - Москва: МАКС Пресс, 2010, - 78 с., - ISBN 978-5-317-032517.

[65] Петухова, Н. Д. Выделение максимальной общей предикатной подформулы с помощью обратного метода Маслова / Н.Д. Петухова // Компьютерные инструменты в образовании - 2015. - Вып. 4. - С. 17-25. -ISSN: 20712340

[66] Петухова, Н. Д. Обратный метод для решения задач логико-предметного распознавания образов и оценки числа шагов его работы / Н.Д. Петухова // Материалы научной конференции по проблемам информатики СПИСОК-2012 - C. 90-94. - ISBN 978-5-9651-0686-8

[67] Петухова, Н. Д. Обратный метод Маслова и муравьиная тактика решения задач Искусственного Интеллекта / Н.Д. Петухова // Материалы научной конференции по проблемам информатики СПИСОК-2013 - C. 64-69. -ISBN 978-5-9651-0779-7

[68] Петухова, Н. Д. Применение тактик муравьиных алгоритмов для решения некоторых задач Искусственного Интеллекта / Н.Д. Петухова, Т.М. Косовская // Вестн. С.-Петерб. ун-та. Сер 10. - 2015. - Вып. 3. - С. 67-82. -ISSN 1811-9905

[69] Пытьев, Ю. П. Методы морфологического анализа изображений / Ю.П. Пытьев, А.И. Чуличков // Москва: ФИЗМАТЛИТ, 2010. - 336 с. - ISBN 978-5-9221-1225-3

[70] Рассел, С. Искусственный интеллект: современный подход, 2-е изд. / С. Рассел, П. Норвиг пер. с англ.// Москва: Издательский дом «Вильямс», 2006. - 1408 с. - ISBN 5-8459-0887-6

[71] Седжвик, Р. Алгоритмы на С++: анализ, структуры данных, сортировка, поиск, алгоритмы на графах / Р. Седжвик пер. с англ.// Москва: ООО «Вильямс», 2014. - 1056 с. - ISBN 978-5-8459-1650-1

[72] Сирота, А.А. Статистические алгоритмы обнаружения границ объектов на изображениях / А.А. Сирота, А.И. Соломатин // Вестник ВГУ. Сер. Системный анализ и информационные технологии, - 2008, № 1, - с. 58-64, - ISSN 1995-5499.

[73] Скиена, С. Алгоритмы. Руководство по разработке, 2-е изд. / С. Скиена пер. с англ.// Санкт-Петербург: БХВ, 2011. - 720 с. - ISBN 978-5-97750560-4

[74] Скобцов, Ю.А. Метаэвристики. Монография. / Ю.А. Скобцов, Е.Е. Федоров // Донецк: Ноулидж, 2013. - 426 с. - ISBN 978-617-579-800-3

[75] Стронгин, Р. Г. Параллельные вычисления в задачах глобальной оптимизации. Монография / Р. Г. Стронгин, В. П. Гергель, В. А. Гришагин, К. А. Баркалов // Москва: Издательство Московского университета, 2013. - 280 с. - ISBN 978-5-211-06479-9

[76] Стругайло, В.В. Обзор методов фильтрации и сегментации цифровых изображений / В.В. Стругайло // Наука и образование. МГТУ им. Н.Э. Баумана. Электроный журнал, - Режим доступа: http://technomag.bmstu.ru/doc/411847.html, - 2012 № 5 - ISSN 2307-0609 (05.03.2016)

[77] Филипповский В.А. Система автоматического поиска доказательств теорем, основанная на специальном варианте обратного метода С.Ю. Маслова: магистерская диссертация, Санкт-Петербургский государственный университет, Санкт-Петербург, 2015

[78] Шапиро, Л. Компьютерное зрение / Л. Шапиро, Дж. Стокман // - Москва: БИНОМ. Лаборатория знаний, 2006. - 752 с. - ISBN 978-5-9963-1312-9

[79] Шишмарев, М.С. Реализация метода Маслова /М.С. Шишмарев, А.Н. Диев, Л.О. Хорошавин, А.Н. Шайкин // Успехи в химии и химической технологии, том XXIV 2010, № 1 (106) - с. 15-18 ISSN 1506-2017

[80] Яне, Б. Цифровая обработка изображений / Б. Яне // Москва: Техносфера, 2007. - 584 с. - ISBN 978-5-94836-122-2

[81] Akl, S.G. Parallel Sorting Algorithms / S.G. Akl // USA, Orlando Fl: Academic Press, 1990. - 234 p. - ISBN 0120476800

[82] Ant colony optimization - methods and applications /edited by A. Ostfeld // Croatia, Rijeka: InTech, 2011. - 342 p. - ISBN 978-953-307-157-2

[83] Canny, J.F. Finding edges and lines in images. / J.F. Canny // Master's thesis. MIT, Cambridge, USA, 1983.

[84] Colorni, A. Distributed Optimization by Ant Colonies, actes de la première conférence européenne sur la vie artificielle / A. Colorni, M. Dorigo, V. Maniezzo// Paris, France, Elsevier Publishing, 1991, 134 - 142.

[85] Degtyarev, A. Equality elimination for the inverse method and extension procedures / A. Degtyarev, A. Voronkov, C. Mellish ed. // Proc. International Joint Conference on Artificial Intelligence (IJCAI) Montreal, 1995. - vol. 1, -pp. 342-347 - режимдоступа: http://www.ijcai.org/Proceedings/95-1/Papers/045.pdf, свободный (05.03.2016)

[86] Degtyarev, A. The inverse Method / A. Degtyarev, A. Voronkov // Handbook of automated reasoning, Elsevier science publishers B.V., - USA, Cambridge, Mass: The MIT Press, 2001, - pp 180-272, - ISBN 0-444-82949-0

[87] Dorigo, M. Artificial Ants as a Computational intelligence technique / M. Dorigo, M. Biratti, T. Stutzle// IEEE computational intelligence magazine, November 2006, pp 28-39

[88] Dorigo, M. Optimization, Learning and Natural Algorithms, PhD thesis, Politecnico di Milano, Italie, 1992.

[89] Downey, A.B. Think Complexity: Complexity Science and Computational Modeling / A.B. Downey // USA, Sebastopol, CA: O'Reilly Media, 2012, - 154 p., - ISBN 978-1-449-31463-7

[90] Du, D.Z. Theory of Computational Complexity / D.Z. Du, Ko K.I // Canada, Toronto: Wiley-Interscience Publication (John Wiley & sons inc.), 2014, - 512 p., - ISBN 978-1-118-30608-6

[91] Fokkink, W. Distributed Algorithms: An Intuitive Approach / W. Fokkink // USA, Cambridge, Mass: The MIT Press, 2013. - 248 p. - ISBN-10 0262026775, ISBN-13 978-0262026772

[92] Goldreich, O. Computational Complexity: A Conceptual Perspective / O. Goldreich // USA, Cambridge, Mass: Cambridge University Press, 2010, - 606 p. - ISBN 978-0-521-88473-0.

[93] Heikkila, M. A texture-based method for modeling the background and detecting moving objects / M. Heikkila, M. Pietikainen // IEEE Transactions on Pattern Analysis and Machine Intelligence, - 2006, vol. 28, no. 4, - pp. 657662, - ISSN 0162-8828

[94] Johnston, J. The Allure of Machinic Life: Cybernetics, Artificial Life, and the New AI / J. Johnston //, USA, Cambridge, Mass: The MIT Press, 2008, - 480 p. - ISBN 978-0-262-10126-4.

[95] Kosovskaya, T. Distance between objects described by predicate formulas / T. Kosovskaya // International Book Series. Information Science and Computing. Book 25. Mathematics of Distances and Applications (Michel Deza, Michel Petitjean, Krasimir Markov (eds)), ITHEA - Publisher, Sofia, Bulgaria, 2012. P. 153 - 159.

[96] Kosovskaya, T. The Inverse Method for Solving Artificial Intelligence Problems in the Frameworks of Logic-Objective Approach and Bounds of its Number of Steps / T. Kosovskaya, N. Petuchova // International Journal «Information Models and Analyses» - 2012. - Vol. 1. - P. 84-93. - ISSN 13146416

[97] Kosovskaya, T. The Maslov's Inverse Method and Ant Tactics for Exhaustive Search Decreasing / T. Kosovskaya, N. Petuchova // International Journal «Information Models and Analyses» - 2013. - Vol. 2. Num. 1. - P. 81-89. -ISSN 1314-6416

[98] Larionov, D.S. Auto-epistemic Logic for Expert System's Inference Engine /D.S. Larionov // Materials of the 9th Russian-Korean International Symposium on Science and Technology "KORUS-2005", Vol. 1, - P. 649-652 ISBN 07803-8943-3

[99] Lifshitz, V. What is the inverse method? / V. Lifshitz // Journal of Automated Reasoning, Netherlands, Dordrecht: Kluwer Academic Publishers, - vol. 5(1), 1989 №1, - pp 1-23 - ISSN 0168-7433

[100] Mints, G. Decidability of the Class E by Maslov's Inverse Method. /G. Mints // Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birrthday, 2010, - pp 529-537 ISBN 978-3-319-23534-9

[101] Moyson, F. The collective behaviour of Ants: an Example of Self-Organization in Massive Parallelism / F. Moyson, B. Manderick // Actes, AAAI Spring Symposium on Parallel Models of Intelligence, Stanford, Californie, 1988.

[102] Process Algebra for Parallel and Distributed Processing / edited by M. Alexander, W.Gardner// USA, Cleveland, Oh: Chapman & Hall/CRC, 2008. -440 p. - ISBN 9781420064865

[103] Robinson, J.A. A machine-oriented logic based on the resolution principle / J.A. Robinson // Journal of the ACM (JACM) - New York, NY, USA 1965. -Volume 12 Issue 1. pp 23-41. - ISSN 0004-5411

[104] Tammet, T. A resolution theorem prover for intuitionistic logic / T. Tammet, M. McRobbie and J. Slaney, Eds. // CADE-13, Lecture Notes in Artificial Intelligence. - 1996, vol. 1104, Springer Verlag. - pp. 2-16 - ISSN 0302-9743

[105] Voronkov, A. Theorem-proving in non-standard logic based on the inverse method / A. Voronkov // 11 th International Conference on Automated Deduction, D. Kapur ed. 1021.cture Notes in Artificial Intelligence, 1992, - vol. 607, Germany, Berlin: Springer Verlag. - pp. 648-662. - ISSN 0302-9743

ПРИЛОЖЕНИЕ А. Пример решения задачи с помощью алгоритма IMA

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

Рис. 1. Предикаты V и Ь.

Задан класс объектов ^ - класс контурных изображений «троек». Схематическое изображение эталонного объекта имеет вид (см. рис. 2):

Рис. 2. Контурное изображение «тройка».

Описание класса задается следующей формулой:

A(xi,..., x6 ) = V (x2, Xi, x4) & V (x4, x2, x3) & V (x4, X3, x6) & V (x6, x4, x5) & l(x4, x2, x6)

Пусть задано контурное изображение, представленное на рис. 3, в котором требуется найти хотя бы один объект, принадлежащий классу «троек».

Это изображение имеет описание:

5 (а-,..., а6 ) = {V (а-, аз ) & V {а2, а-, а4 ) & V (а3, а-, а4 ) & V (аз, а4, а5 ) & £(аз, а-, а5 )

& V(a4, а2, аз ) & V(a4, аз, а6 ) & £(а4, а2, а6 ) & V(a5, аз, а6 ) & V(a6, а4, а5 )}

Оценка числа шагов решения этого примера (так как 8=10, 5=5) имеет порядок 105 .

Для того, чтобы выделить объект, принадлежащий классу «троек», необходимо доказать выводимость следующего логического следования:

Общезначимость этой формулы равносильна общезначимости формулы

,..., О^ЭХ!,..., Хб

V{х2,Х1,Х4—1У(О1,О2,О3) V —1V(о2,О!,О4) V —1V(03,О!,О4) V ^ Ту(о3, О4, О 5) V —V (о4, О2, О3) V—V(o4, 03, о6) V—V(o5, 03, О6) V & у —V(o6,О4,О5) V—ь(о3,О1,О5) V—Ь(О4,О2,О6) у

^ V(x4, Х2, Х3 )v—V(o^, О2, О3) V — V (О2, О\, О 4) V—V(o3, О\, О 4) V л

у(о3,О4,О5) V —V(О4,О2,О3) V —1V(о4,О3,О6) V —V(О5,О3,О6) V & у —V(o6, О4, О5) V—Ь(О3, О1, О5) V—Ь(О4, О2, Об) у

А V(x4 3,Х6)v — V(ol,о2,о3) V 1V(о2,оъо4) V 1V(о3,ОъО4) V Л У(О3, О4, О5) V —V (04, О2, О3) V —1 V (о 4, О3, Об) V —1 V (О5, О3, Об) V &

у —V(06, О4,05) V—Ь(03, О1,05) V—Ь(04, О2, Об) у

^ V(x6, Х4, Х5 )v—V (о\, 02,03) V—V (02,0\, о 4) V—V (03,0\, о 4) V л V(03,04,05) V —1V(о4,02,03) V —V(04,03,Об) V —1V(05,03,Об) V &

у —V (Об, О4,05) V—Ь(03, О1,05) V—Ь(04, О2, Об) у

^ ь(х4, Х2, Хб )v—V(0l, 02,03) V — V (02,0\, О 4) V — V (03, 0\, О 4) V л 1V(03,04,05) V —1V(о4,02,03) V —V(04,03,Об) V —1V(05,03,Об) V

уу —V (Об, О4,05) V—Ь(03, О1,05) V—Ь(04, О2, Об) у у

Результатом выполнения п. 1 будет следующий Б-набор:

^ V (хъ Х\„ Х4 )v—V (о!, 02,03) V— V (02, О1, О 4) v—V (03,01, О 4) V

-1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V

у —V (Об, О4, О5) V —Ь(03, О1, О5) V—Ь(О4, 02, Об) у

Г V(x4, Х2, Х3 )v—V(o^, О2,03) V—V (02, О1, О 4) V—V (03, О1, О 4) V Л -1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V

у —V (Об, О4,05) V—Ь(03, О1,05) V—Ь(04, О2, Об) у

Г V(x4, Х3, Хб )v—V (01, О2,03) V —1 V (02, О1, О 4) V—V (03, О1, О 4) V Л

В:

-1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V

у —V (Об, О4,05) V—Ь(03, О1,05) V—Ь(04, О2, Об) у

г V(x6, Х4, Х5 ')v—V(0l, 02,03) V—V (02,01, О 4) V—V (03,01, О 4) V Л -1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V

у —V (Об, О4,05) V—Ь(03, О1,05) V—Ь(04, О2, Об) у

Г Ь( Х4, Х2, Хб )v—V (01,02,03) V—V (02, О!, О 4) V —1 V (03, О!, О 4) V Л -1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V

уу —V(Об,О4,05) V—Ь(03,О!,05) V—Ь(04,О2,Об) уу

На выполнение п. 1 алгоритма IMA потребовалось 5 шагов. П. 2.1 на этом этапе не применяется. Согласно п. 2.2, берем формулу V(x2,Xi,Х4), согласно п. 2.3 берем отрицание атомарной формулы с тем же предикатным символом —¡V (а^, ^, а^) (2 шага), и помечаем его как уделенное (5

шагов). Согласно п. 2.4 решаем систему уравнений, отождествляющую эти две формулы:

Х2 — ai Xi — а2

Х4 — аз

(3 шага)

Согласно п. 2.5 рассматриваемый F-набор D приобрел вид

D:

V(ai,а2,аз)v — V(ai,а2,аз) v —V(a2,а^,а4) v—V(аз,а^,а4) v

\Л

и V(аз,а4„а5) v — V(а 4,а^,аз) v — V(а 4,аз,а^) v — V(а$,аз,а^) v — V(а6,а4„а5) v —Ь(аз,а^„а5) v —Ь(а4,а2,а^)

V(аз,а1,Хз)v — V(а1,а2,аз) v—V(а2,а1,а4) v— V(аз,а1,а4) v

-1V(аз,а4,а5) v — V(а 4,а2,аз) v — V(а 4,аз,аб) v — V(а5,аз,аб) v — V(а^„а4,а5) v —Ь(аз,а^„а5) v —Ь(а4,а2,а^)

V(аз,Хз,Хб)v —1V(а1,а2,аз) v— V(а2,а1,а4) v— V(аз,а1,а4) v

-1V(аз,а4,а5) v — V(а4,а^,аз) v — V(а4,аз,а^) v — V(а5,аз,а^) v — V(а6,а4,а5) v —Ь(аз,а^„а5) v —Ь(а4,а2,а^)

аз,Х5)v — V(а1,а2,аз) v —V^2,а1,а4) v—V(аз,а1,а4) v

V(аз,а4,а5) v — V(а4,а2,аз) v — V(а4,аз,а^) v — V(а5,аз,а^) v — V(а^,а4,а5) v —Ь(аз,а^„а5) v —Ь(а4,а2,а^)

Ь(аз,а1,Хб)v — V^i,а2,аз) v—V(а2,а1,а4) v— V(аз,а1,а4) v

W

1V(аз,а4,а5) v — V(а4,а^,аз) v — V(а4,аз,а^) v — V(а5,аз,а^) v — V(а6,а4,а5) v —Ь(аз,а^„а5) v —Ь(а4,а2,а^)

JJ

на замену всех вхождений переменных на их значения уходит 13 шагов.

На выполнение пп. 2.6 и 2.7 (проверку не получился ли пустой или тупиковый Б-набор) затрачено 10 шагов. На выполнение п. 2.8 ушло 5 шагов.

Согласно п. 2.9 (4 шага) возвращаемся к п. 2.2 и 2.3. Берем формулу V {аз, аъ х3 ) и

отрицание атомарной формулы с тем же предикатным символом — V(аз,аа4) (7 шагов). Согласно п. 2.4 решаем систему уравнений, отождествляющую эти две формулы

Х3 — а4

Согласно п. 2.5 рассматриваемый Б-набор Э приобрел вид

(1 шаг)

/V

В:

V{a1,а2,аз^ — V(a1,а2,аз) V — V(а2,а±,а4) V — V(аз,а±,а4)

V

\Л

-1 V(аз,а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а^) V —V(а$,аз,а6) V — V(а6,а4,а5) V —Ь(аз,а^„а5) V —Ь(а4,а2,а6)

V {аз, ау„ а 4 )

IV

V(а\,а2,аз) V—V(а2,а1,а4) V — V(аз,а1,а4)

V

-лУ(аз„а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а6) V —V(а5,аз,а6) V — V(а§,а4,а5) V —Ь(аз,а\,а5) V —Ь(а4,а2,а6)

V ^ а4^ Х6 )

V

V(а^„а2,аз) V—V(а2,а1,а4) V — V(аз,ау„а4)

V

-1 V(аз,а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а6) V —V(а5,аз,а^) V — V(а6,а4,а5) V —Ь(аз,а^„а5) V —Ь(а4,а2,а6)

V ^ аз^ Х5 )

IV

V(a1,а2,аз) V—V(а2,а\,а4) V —V(аз,а\,а4)

V

У(аз„а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а6) V —V(а5,аз,а6) V — V(а§,а4,а5) V —Ь(аз,а\,а5) V —Ь(а4,а2,а6)

Ь{аз,а1,Х6^ — V(а1,а2,аз) V—V(а2,а1,а4) V — V(aз,а1,а4)

V

\\

У(аз„а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а6) V —V(а5,аз,а^) V — V(а6,а4,а5) V —Ь(аз,а^„а5) V —Ь(а4,а2,а6)

на замену всех вхождений переменных на их значения уходит 6 шагов.

8 9 шагов на подстановку полученных в результате решения системы уравнений значений переменных в Б-

наборе и 4 шага на п. 2.6, то есть на проверку наличия повторений формул в Б-наборе и их удаление.

На п. 2.6 уходит 5 шагов. Согласно п. 2.7 получился тупиковый Б-набор (10 шагов), переходим к п. 3 и отменяем последнее действие п. 2.5. Рассматриваемый Б-набор Э принимает вид

/V

В:

V (оу, 02, О3 ^ — V (Оу, О2,03) V—V (02, О!, 04) V —V (03, О!, О4)

V

\Л

-1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V — V (Об, О4,05) V —¿(03, Оу, 05) V —Ь(04, О2, Об)

V ^ оЪ Х3 )

IV

V (Оу, 02,03) V—V (02, Оу, 04) V — V (03, Оу, 04)

V

—IV(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V — V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04,02, Об)

V ^ ^ Хб)

IV

V (Оу, О2,03) V—V (02, Оу, 04) V — V (03, Оу, 04)

V

-1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V — V (Об, О4,05) V —¿(03, Оу, 05) V —¿(04, О2, Об)

V ^ Х5 )

IV

V(0!, 02,03) V—V (02, Оу, 04) V —V (03, Оу, 04)

V

1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V — V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04,02, Об)

ь(О3, Оу, Хб ^ — V (Оу, О2,03) V—V (02, Оу, 04) V — V (03, Оу, 04)

V

уу

1 V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V —V(05,03,Об) V — V (Об, О4,05) V —¿(03, Оу, 05) V —¿(04, О2, Об)

уу

на обратную замену всех вхождений значений переменных на их имена уходит 2 шага.

Возвращаемся к 2.3. У формулы V(03,Оу,Х3) нет подходящей для унификации (8 шагов). Согласно п. 3 рассматриваемы Б-набор принимает исходный вид, но формулы —V(Оу,О2,О3) и — V(03,Оу,О4) помечены как удаленные и не принимают участия в переборе (9 шагов).

В

Г Г

V(x2, Ху, Х4 ^ — V (Оу, 02, 03) V — V (02, Оу, 04) V — V (03, Оу, 04)

\л

V

-IV(03,04,05) V — V(04,02,03) V — V(04,03,Об) V — V(05,03,Об) V — V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04, 02, Об)

V (Х4, Х2, Х3 ^

V(0!, 02,03) V — V (02, Оу, 04) V — V (03, Оу, 04)

V

-IV (03,04,05) V — V (04,02,03) V — V (04,03, Об) V — V (05,03, Об) V

— V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04, 02, Об) V (Х4, Х3, Хб ^ — V (Оу, 02,03) V— V (02, Оу, 04) V — V (03, Оу, 04)

V

-IV (03,04,05) V — V (04,02,03) V — V (04,03, Об) V — V (05,03, Об) V — V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04, 02, Об)

V (x6, x4, Х5 )

V

V(0!, 02,03) V — V (02, Оу, 04) V —I V (03, Оу, 04)

V

V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V — V(05,03,Об) V — V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04, 02, Об)

Ь(Х4, Х2, Хб ^ —У(0\, 02,03) V — V (02, Оу, 04) V — V (03, Оу, 04)

V

уу

V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V — V(05,03,Об) V — V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04, 02, Об)

уу

Согласно пп. 2.2 и 2.3 берем формулу V(Х2,Ху,Х4) и отрицание — V (02, Оу, О 4) (7 шагов). Согласно п. 2.4 решаем систему уравнений, отождествляющую эти две формулы

Х2 ~ о2 Ху = Оу

Х4 = О 4

(3 шага)

Согласно п. 2.5 рассматриваемый Б-набор Э приобрел вид

В:

V

— V (а1, а2, аз) V — V (а2, а\, а 4) V — V (аз, а\, а 4)

V

V {а2, а1, а 4 )

— V(аз,а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а^) V — V(а5,аз,а^) V — V(а6,а4,а5) V —Ь(аз,а\,а5) V —Ь(а4,а2,а^)

V {а4, а2, Хз )

\л

V

— V (а1, а2, аз) V — V (а2, а\, а 4) V — V (аз, а\, а 4)

V

-IV(аз,а4,а5) V — V(а4,а^,аз) V — V(а4,аз,а^) V — V(а5,аз,а^) V — V(а6,а4,а5) V —Ь(аз,а^„а5) V —Ь(а4,а2,а^

V ^ ^ Х6 )

IV

— V (а1, а2, аз) V — V (а2, а\, а 4) V — V (аз, а\, а 4)

V

— V(аз,а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а^) V — V(а5,аз,а^) V

— V(а6,а4,а5) V —Ь(аз,а\,а5) V —Ь(а4,а2,а^) V {х6, а4, Х5 ) V

— V (а1, а2, аз) V — V (а2, а\, а 4) V — V (аз, а\, а 4)

V

— V(аз,а4,а5) V — V(а4,а^,аз) V — V(а4,аз,а^) V — V(а5,аз,а^) V — V(а6,а4,а5) V —Ь(аз,а^„а5) V —Ь(а4,а2,а^

^,{^4, а2, Х6 )

IV

— V (а1, а2, аз) V — V (а2, а\, а 4) V — V (аз, а\, а 4)

V

1V(аз,а4,а5) V — V(а4,а2,аз) V — V(а4,аз,а^) V — V(а5,аз,а^) V — V(а6,а4,а5) V —Ь(аз,а\,а5) V —Ь(а4,а2,а^)

на замену всех вхождений переменных на их значения уходит 13 шагов.

Согласно п. 2.9 (5 шагов) возвращаемся к п. 2.2 и 2.3. Берем формулу

V{а4,а2,Хз) и отрицание —V(а4,а2,аз) (7 шагов). Согласно п. 2.4 решаем

систему уравнений, отождествляющую эти две формулы

Хз — аз

(1 шаг)

Согласно п. 2.5 рассматриваемый Б-набор Э приобрел вид

(г

В:

V(o2,Оу,04^ —V(0!,02,03) V — V(02,Оу,04) V —V(0з,Оу,04)

\\

V

V(oз,04,05) V —V(04,02,03) V—V(04,03,Об) V—V(05,03,Об) V

1 V (Об, 04,05) V —¿(03, Оу, 05) V —¿(04,02, Об)

V (04,02, 03 ^ —V(0!, 02, 03) V — V (02, Оу, 04) V —V(0з, Оу, 04)

V

V(oз,04,05) V —V(04,02,03) V—V(04,03,Об) V—V(05,03,Об) V

1 V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

V (о4 , 03, Хб ^ —V (Оу, 02,03) V — V(02, Оу, 04) V \^(0з, Оу, 04)

V

V(oз,04,05) V —V(04,02,03) V—V(04,03,Об) V—V(05,03,Об) V

1 V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

V(x6,04,Х5)v — V(оу,02,03) V — V(02,Оу,04) V —V(oз,Оу,04)

V

V(oз,04,05) V —V(04,02,03) V—V(04,03,Об) V—V(05,03,Об) V

1 V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

¿(04,О2,Хб^ —V(0!,О2,03) V — V(02,Оу,04) V —V(0з,Оу,04)

V

V(oз,04,05) V —V(04,02,03) V—V(04,03,Об) V—V(05,03,Об) V

уу

1 V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

уу

на замену всех вхождений переменных на их значения уходит 5 шагов.

На выполнение пп. 2.6 и 2.7 затрачено 10 шагов. На выполнение п. 2.8 ушло 5 шагов. Согласно п. 2.9 (5 шагов) возвращаемся к п. 2.2 и 2.3. Берем формулу V(04,03,Хб) и отрицание —V(04,03,Об) (7 шагов). Согласно п. 2.4 решаем систему уравнений, отождествляющую эти две формулы

Х6 - 06

I

I

—

I

(1 шаг)

Согласно п. 2.5 рассматриваемый Б-набор Э приобрел вид

(г

В:

V (02, Оу, 04 ^ — V (Оу, 02,03) V — V (02, Оу, О 4) V — V (03, Оу, О 4)

\\

V

V(03,04,05) V — V(04,02,03) V — V(о4,03,Об) V — V(05,03,Об) V

V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

V (04,02, 03 ^ —V(0!, 02,03) V — V (02, Оу, 04) V —V(0з, Оу, 04)

V

V(03,04,05) V — V(04,02,03) V — V(04,03,Об) V — V(05,03,Об) V

V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

V (04,03, Об ^ —V(0!, 02,03) V — V (02, Оу, 04) V —V(0з, Оу, 04)

V

V(03,04,05) V — V(04,02,03) V — V(о4,03,Об) V — V(05,03,Об) V

V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

V(o6, О4, Х5 ^ —V(0!, О2,03) V — V (02, Оу, 04) V —V(0з, Оу, 04)

V

V (03,04,05) V — V (О4, О2,03) V ^(04,03, Об) V — V (05, 03, Об) V

V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

¿(04,О2,Об^ —V(0!,О2,03) V — V(02,Оу,04) V —V(0з,Оу,04)

V

V(03,04,05) V — V(04,02,03) V — V(о4,03,Об) V — V(05,03,Об) V

уу

V (Об, 04,05) V —Ь(0з, Оу, 05) V —¿(04,02, Об)

уу

на замену всех вхождений переменных на их значения уходит 6 шагов.

На выполнение пп. 2.6 и 2.7 затрачено 10 шагов. На выполнение п. 2.8 ушло 5 шагов. Согласно п. 2.9 (5 шагов) возвращаемся к пп. 2.2 и 2.3. Берем формулу

V (06 ,04,Х5) и отрицание —у(о6,о4,о5) (8 шагов). Согласно п. 2.4 решаем

систему уравнений, отождествляющую эти две формулы

Х5 - 05

I

I

—

I

(1 шаг)

Согласно п. 2.5 рассматриваемый Б-набор Э приобрел вид

/V

В:

V{a2,а1,а4^ —V(a1,а2,аз) V —V(a2,а1,а4) V —V(aз,а1,а4)

\\

V

V(aз,а4,а5) V —V(a4,а2,аз) V — V(a4,аз,а6) V—V(а5,аз,а6) V

1V(а6,а4,а5) V —Ь(аз,а1,а5) V —Ь(а4,а2,а6)

V{a4,а2,аз^ —V(a1,а2,аз) V —V(a2,а1,а4) V —V(aз,а1,а4)

V

V(aз,а4,а5) V —V(a4,а2,аз) V — V(a4,аз,а6) V—V(а5,аз,а6) V

1V(а6,а4,а5) V —Ь(аз,а1,а5) V —Ь(а4,а2,а6)

V{а4,аз,а6^ — V(а1,а2,аз) V — V(а2,а1,а4) V — V(аз,а1,а4)

V

V(aз,а4,а5) V —V(a4,а2,аз) V — V(a4,аз,а6) V—V(а5,аз,а6) V

1V(а6,а4,а5) V —Ь(аз,а1,а5) V —Ь(а4,а2,а6)

V{a6,а4,а5^ —V(a1,а2,аз) V ^(а2,а-,а4) V —V(aз,а1,а4)

V

V(aз,а4,а5) V ^(а4,а2,аз) V — V(a4,аз,а6) V—V(а5,аз,а6) V

1V(а6,а4,а5) V —Ь(аз,а1,а5) V —Ь(а4,а2,а6)

Ь{а4,а2,а6^ —V(a1,а2,аз) V —V(a2,а-,а4) V —V(aз,а-,а4)

V

V(aз,а4,а5) V —V(a4,а2,аз) V — V(a4,аз,а6) V—V(а5,аз,а6) V

\\

1V(а6,а4,а5) V —Ь(аз,а-,а5) V —Ь(а4,а2,а^

на замену всех вхождений переменных на их значения уходит 5 шагов.

Согласно п. 2.6 получился пустой Б-набор (5 шагов), объект «тройка» выделен.

Рис. 2.2.5. Выделенный на заданном контурном изображении объект «тройка».