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

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

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

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

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

– Опять дерево?
– удивляется силлогизм, а вместе с ним, быть может, и внимательный читатель.

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

– Вы называете свои теоретические построения деревьями для простоты? Небось в^науке они иначе именуется?

– Ничего подобного. Их так и называют - деревья. Бывают конечные деревья и бесконечные деревья, развивается математика деревьев. Но прежде чем говорить о деревьях вообще, давайте познакомимся с деревом опровержений.

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

Дерево опровержений - это наоборотное дерево, чьи ветви всегда собираются парами. Так велит метод резолюции.

Этот метод относится к самым крупным достижениям за все время работы в области Искинта. Найден алгоритм, свободный от человеческих слабостей, исчерпывающий все "за" и "против" и обязательно приводящий к результату. К реальному результату в реальной вычислительной машине!

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

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

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

Героиня задачи "Обезьяна и бананы" может отказаться от ненадежных услуг ЛЮБОЗАРа и предпочесть ему обязательную резолюцию. Впрочем, обезьяны давно пользовались методом резолюции, не ручаюсь за всех обезьян, но мартышки точно пользовались.

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

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

Резолюция вызывает энтузиазм специалистов, проявления которого очевидны, например, в отрывке из совсем свежей научной статьи: "Система доказательства теорем чарует и влечет. В самом деле, она универсальна, упорядочена и ее достоинства имеют подтверждение; опираясь на правильные входные данные, она весело и непринужденно приведет вас к искомому результату".

Итак, "мартышкин труд" предпочтительней эвристик. ЛЮБОЗАР с его колебаниями и отсутствием гарантий успешного решения должен уступить дорогу властной резолюции. Машинная логика сама, без человека одолеет любые препятствия.