"Математическая логика долгое время была одной из самых абстрактных ветвей математики. Задачи, которые она ставила перед собой и решала, носили чисто внутренний математический характер, важный лишь для этой науки. Основной целью математической логики было подвести прочный и непротиворечивый фундамент под здание математики... Давно стало трюизмом утверждение о том, что любая сколь угодно абстрактная ветвь математики со временем становится практически важной и необходимой. Так было с топологией, так было с теорией групп, так случилось и с математической логикой".
Моделирование рассуждений человека, осуществление логического вывода (поиск вывода) с помощью вычислительной машины — одно из важнейших направлений работ по ИИ. И здесь результаты, полученные в математической логике, оказались исключительно важными для решения задач ИИ.
В 1961 году из участников семинара по математической логике и конструктивной математике, проводимого Н. А. Шаниным на математико-механическом факультете Ленинградского университета, образовалась группа математической логики Ленинградского отделения Математического института им. В. А. Стеклова АН СССР (ЛОМИ). Эта группа занялась поиском естественного логического вывода, максимально близкого по форме к "человеческому".
Работа группы началась с построения алгорифма, который выдавал бы достаточно "хороший" и естественный вывод данного утверждения из данных аксиом. Такая постановка задачи была связана с тем, что известные алгоритмы, дающие для каждой выводимой формулы какой-то ее вывод, могли выдавать излишне длинный и трудно воспринимаемый вывод. Первоначально рассматривался вывод в классическом исчислении предикатов. Исследования завершились разработкой Алгорифма Поиска Естественного Вывода (АЛПЕВ), который был запрограммирован и обладал по тем временам выдающейся производительностью [82]. В этой программе впервые в мире был смоделирован "человеческий" логический вывод при поиске доказательства утверждений.
АЛПЕВ применим для логики высказываний, для исчисления предикатов требовались новые идеи. Идея "метапеременных", предложенная Н. А. Шаниным, дала импульс для создания в 1964 году "обратного метода", разработанного С. Ю. Масловым.
В отличие от созданного в 1965 году метода резолюций Дж. Робинсона, обратный метод С. Ю. Маслова нацелен как на машинную реализацию, так и на получение результатов в самой математической логике. Он позволил не только создать программу поиска вывода в исчислении предикатов, но и решить задачу систематической трактовки разрешимых классов формул исчисления предикатов, поставленную Гильбертом.
Опыт, накопленный при создании метода поиска вывода в исчислении предикатов, послужил отправной точкой для работ в области общей теории дедуктивных систем. Здесь речь идет о том, что процесс решения человеком творческих задач может моделироваться на основе теории машинного вывода в исчислениях общего типа (исчисления Э. Л. Поста).
Этимология слова intellego (inter и lego) — "выбираю среди". Большинство задач, обычно относящихся к творческим, от решения кроссвордов и головоломок до написания стихов и доказательства теорем, связаны с перебором вариантов. Тем не менее особенностью человека является способность рационально уменьшить этот перебор. До тех пор, пока машина не обладала достаточным быстродействием, она часто проигрывала в шахматы даже мастеру спорта. Как только быстродействие достигло определенного уровня, она смогла обыграть даже чемпиона мира: в 1994 году ПК на базе процессора Intel Pentium со смехотворной, по нынешним временам, частотой 90 МГц обыграл в серии турниров по шахматам нескольких сильнейших гроссмейстеров мира, включая действующего чемпиона мира — Гарри Каспарова.
Под термином "творческая задача" можно понимать выполнение некоторой последовательности элементарных действий (или ходов), ведущих к решению основной задачи. Примерами таких задач являются и игра в шахматы, и нахождение интеграла, и решение задачи на построение циркулем и линейкой. Наилучшей модельной задачей такого творчества, которое может быть сведено к интеллектуальному перебору в конечном и четко очерченном множестве (решение кроссвордов, игра в шахматы), а не к выбору и уточнению объекта из неопределенно-неограниченного поля объектов (отгадывание загадок, сочинение стихов), является доказательство теорем в фиксированной и полностью формализованной формальной теории. А такая задача относится к области теории поиска вывода, определяемой как область математической логики, занимающаяся выявлением по гипотезе структуры ее возможных доказательств, по исчислению и объекту, представленному на языке исчисления, структуры возможных выводов этого объекта. В отличие от классической логики, для которой главное — "что считать истиной", центральным вопросом теории поиска вывода является — "как найти истину".
Если говорить о математике в целом, то лишь в редких работах рассказывается о том, как был получен тот или иной результат. Важно только, чтобы он был правильным. Этап же проб и ошибок, который предшествовал нахождению истины, остается за скобками рассмотрения.
Теорию поиска вывода, являющуюся ветвью математической логики, интересует именно процесс нахождения решения: формальный вывод в теории поиска вывода. Правило вывода называется допустимым, если его добавление не расширяет множество выводимых элементов.
Для понимания творческого процесса и разработки систем ИИ важными являются взаимосвязанные задачи:
- выработка критериев отбора допустимых правил;
- выявление механизмов их формирования.
Первая из этих задач решается путем накопления опыта, выявления и формализации знаний экспертов. Вторая, более сложная, в общем виде не решалась.
Поиск решений в ИИ заключается в нахождении эвристик, используемых человеком в процессе решения задач, т. е. механизмов, позволяющих избежать полного перебора вариантов. Таким образом, задача теории поиска вывода в математической логике и эвристического программирования в ИИ общая, с той лишь разницей, что отправной точкой математического рассмотрения является формальная или дедуктивная система (теория, исчисление), а исходная точка ИИ — сам процесс решения задачи человеком.
Пусть имеется некоторый класс Р творческих, в выше описанном смысле, задач (см. примеры разд. "Аксиоматический метод и формальные теории" гл. 1).
В качестве аксиом исчисления Тр возьмем задачи, решение которых известно. В качестве правил вывода возьмем правила вида:
^ь •••> $п \~ $0
означающие, что задача ^0 будет решена в случае, если решены задачи 5\, ..., 5п. Таким образом, некоторая задача из Р имеет решение в случае, если она выводима в построенном исчислении. Найти решение задачи — то же самое, что найти один из ее выводов в построенном исчислении, причем лучшим будет решение, соответствующее более короткому выводу. Исчисление при "удачном" построении может быть полным, т. е. задача из Р будет иметь решение только в том случае, когда она выводима в Тр.
Таким образом, решение творческой задачи сводится к поиску вывода в формальной системе. Так как обратный метод С. Ю. Маслова пригоден не только для логических исчислений, но и для произвольных исчислений со свойствами подформульности, автоматизация вывода в этом исчислении приведет и к автоматизации решения исходной задачи.
Но задача может решаться по-разному: опыт и мастерство перворазрядника не идут ни в какое сравнение с опытом мастера. Именно переход от одного уровня знания к другому, более высокому, ассоциируется у нас с творчеством в полном смысле этого слова. С точки зрения аппарата исчислений можно говорить о переходе от одного исчисления к другому, более совершенному, в котором количество решаемых (выводимых) задач больше, а время, требуемое на их решение, меньше. Приобретение опыта, таким образом, можно ассоциировать с совершенствованием дедуктивной системы, с помощью которой мы решаем задачи данного класса, а переход с одного уровня знания на другой — с "башней исчислений" [51].
По этому поводу Маслов пишет: "...машинный поиск найдет решение лишь простейших задач. Как же поступит специалист по искусственному интеллекту? Путем теоретических рассмотрении и изучения опыта мастеров он найдет вариант исчисления существенно лучше приспособленный к организации поиска вывода. Другими словами, он поднимется на следующий этаж башни исчислений и втащит с собой свою машину. Вот теперь-то ЭВМ начнет обыгрывать людей с ограниченным опытом. И будет обыгрывать до тех пор, пока человек, сам умеющий модифицировать свои исчисления, не влезет на следующий этаж... Современные машины тысячекратно превышают человеческие возможности к механическому поиску на своем этаже, но лишь способность к усовершенствованию исчислений человек склонен считать творческой. По крайней мере, пока. Пока машинное моделирование этой способности находится в зачаточном состоянии. Надеюсь, когда-нибудь человек научит машину моделировать эту способность. Надеюсь, у него и тогда останется много оснований для высокой самооценки".
