Доказательство теорем

Еще одной областью, связанной с вычислительными задачами, является доказательство теорем. Эта область творческой деятельности человека наиболее просто поддается автоматизации, т.к. математическое доказа­тельство в достаточной степени формализовано, особенно в тех разделах математи­ки, которые тесно связаны с формальными системами. Поэтому первыми теорема­ми, доказанными с помощью ЭВМ с США в середине 50-х годов, были теоремы исчисления высказываний, а затем и исчисления предикатов. Несколько позже ЭВМ использовались для доказательства теорем абстрактной алгебры и некоторых несложных геометрических теорем. На первом этапе ЭВМ оказались способными искать лишь простые доказательства путем применения правил вывода к исходным аксио­мам. Одной из первых систем такого типа была разработанная в СССР программа АЛПЕВ, созданная под руководством Н.А.Шанина. Однако довольно скоро внима­ние логиков привлекла сама проблема вывода и поиска эффективных процедур такого вывода. Во второй половине 60-х годов были найдены две такие процедуры, которые прочно вошли в состав средств, используемых в исследованиях по искусст­венному интеллекту. Это метод резолюций, предложенный в 1965 году Дж.Робинсономи обратный метод С.Ю.Маслова, предложенный двумя годами позже. Оба метода дают возможность осуществлять поиск доказательств в исчислении предикатов и являются достаточно мощными. На их основе построено множество модификаций, обладающих теми или иными достоинствами. Поиск таких процедур продолжается. Он стимулируется еще и тем, что, как было показано независимо друг от друга в 1936 г. А.Черчем и А.Тьюрингом, не существует универсальной процедуры доказательства тождественной истинности произвольной формулы в исчислении предикатов первого порядка, если заранее не известно, является ли она таковой. Поэтому представляет большой интерес поиск процедур вывода, ориентированных на те или иные проблемные области, в которых за счет их специфических особенностей можно строить эффективные процедуры доказа­тельств.Это соображение лежит в основе второй особенности машинных систем доказа­тельства теорем, важной для искусственного интеллекта. С учетом семантики решаемой задачи на дереве поиска вывода возможно указать некоторые эвристиче­ские правила, сокращающие перебор путей, ведущих от исходных формул к доказываемой или от доказываемой к исход­ным. Именно при доказательстве теорем, по-видимому, впервые возникла идея эвристических правил, как путей сокращения большого перебора. Эта идея в дальнейшем развилась в целую ветвь – эвристиче­ское программирование, сыгравшую большую роль на начальном этапе работ по интеллектуальным системам. Особенно интересными были эвристические правила, отражавшие особенности доказательства теорем человека в геометрии. Начальный этап исследований в области машинного доказательства теорем отражен в сборнике, вышедшем в США в 1963 г.

Распознавание образов

Это еще одно направление, родившееся в 50-е годы, как следствие начала использования ЭВМ для решения не вычислительных задач. Традиционная постановка задач в этой области близка к задаче класси­фикации: необходимо найти совокупность классифицирующих признаков, с по­мощью которых было бы возможным построить решающие правила, относящие те или иные единичные объекты к заранее выделенным или формируемым по отноше­нию близости по признакам классам. Распознавание образов – активно и бурно развивающаяся наука, имеющая ярко выраженное прикладное значение, вырабо­тавшая свои приемы и методы решения задач. Часть из них (например, статистические методы распознавания или распознавание с помощью метода потенциальных функций) по своим идеям весьма далеки от идей и методов искусственного интеллекта. Поэтому они не оказали заметного влияния на его развитие. Другая же часть методов теории распознавания (особенно та, методы которой опираются на идею построения классифицирующей системы признаков в процессе обучения), наоборот, весьма близка к искусственному интеллекту, связана с ним и продолжает оказывать значительное влияние на работы в области интеллектуальных систем.

Игровые программы

Использование ЭВМ для моделирования на них процес­са игры также имеет давнюю историю. Программы для простых игр типа "крести­ки-нолики" или "ханойская башня" появились в самом конце 40-х годов. Потом число таких программ стало быстро увеличиваться. На ЭВМ стали воспроизводить процесс игры в различные карточные игры, домино, шашки, шахматы, и многие другие. Практически, сейчас нет ни одной игры, которая была бы достаточно популярна и не использовалась бы для воспроизведения на вычислительной маши­не. При создании таких программ исследователи столкнулись с проблемой поиска и перебора. И эти процедуры надолго привлекли внимание специалистов. Нахож­дение эффективных стратегий поиска по дереву игры было задачей, во многом похожей на задачу поиска эффективных путей доказательства теорем. Классифи­кация ситуаций, складывающихся на игровом поле, во многом сближала возника­ющие здесь задачи с традиционными задачами распознавания образов. Это делало игровые программы хорошим полигоном для отработки различных приемов и методов поиска решений в условиях богатого множества альтернатив.Впервые проблема алгоритмизации шахматной игры была рассмотрена в 1949 г. К.Шенноном, который предложил использовать при организации шахмат­ных программ следующие три принципа, остающиеся до настоящего времени основными для большинства программ такого рода:

1. перебор возможных продолже­ний шахматной партии на определенное число ходов вперед;

2.  оценка возникаю­щих позиций с помощью некоторой оценочной функции, учитывающей материал и позицию;

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

Последний принцип особенно важен, т.к. рост перебора вариантов при увеличе­нии глубины просмотра продолжения шахматной партии происходит весьма быстро, имея экспоненциальный характер, что предъявляет повышенные требования к быстродействию ЭВМ. Поэтому именно в шахматных программах зародились идеи методов сокращения перебора на древовидных структурах. В СССР первый такой метод (метод граней и оценок) был предложен А.С.Брудно. В США методами подобного типа много занимался Н.Нильсон. Примером удачного применения эвристических приемов к шахматным программам может служить программа "Каисса", созданная в СССР В.Л.Арлазаровым, Г.М.Адельсоном-Вельским и М.Б.Дон­ским. В последнее время в связи с развитием методов искусственного интеллекта стали появляться новые идеи и в шахматных программах. Их функционирование стало опираться не на простой перебор вариантов, а на попытку смоделировать на ЭВМ особенности мышления человека-шахматиста. В СССР эти новые идеи нашли свое отражение в проекте программы "Пионер", разработанной под руководством М.М.Ботвинника. За рубежом принципы построения программ такого типа обоснованы Д.Мичи. Эвристики и приемы сокращения перебора при большом количестве вариантов, разработанные в области создания игровых про­грамм, находят сейчас широкое применение в различных интеллектуальных системах.