Алексей Чачко - Искусственный разум

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

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

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

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

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

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

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

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

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

Аристотелевские умозаключения (силлогизмы)

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

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

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

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

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

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

Что речь идет "без смысла", строго формально, так это в определенном смысле даже лучше: только строго формальная диета прописана вычислительной машине; понимать "по смыслу" она не умеет.