Исследованием вычислительной обозримости (или необозримости) проблем занимается теория сложности. Для начала нам потребуется только знать, что существуют классы проблем, решение которых требует ресурсов, экспоненциально возрастающих при линейном увеличении размерности задачи. Например, время, необходимое для отыскания пути в лабиринте, экспоненциально увеличивается при увеличении количества разветвлений в лабиринте. Аналогично, время, необходимое для поиска доказательства теоремы исчислением утверждений, растет экспоненциально по отношению к количеству переменных. Такие проблемы являются в общем случае необозримыми и называются NP-hard. Читателей, которые ими заинтересуются, мы отсылаем к специальной литературе, в частности книге Хопкрофта и Ульмана [Hopcroft and Ullman, 1979].
Проблемы, время решения которых связано с размерностью задачи полиномиальной функции, считаются обозримыми. Например, проверка заданного маршрута в лабиринте или проверка правильности доказательства некоторой теоремы — обозримые проблемы. Но можно показать, что, к сожалению, большинство проблем, которые интересуют нас в области искусственного интеллекта, относятся к классу NP-hard. Поэтому такое важное значение придается использованию эвристических методов при их решении.
Прекрасное изложение теории вычислительной сложности, рассчитанное на читателя, несклонного к излишнему теоретизированию, можно найти в работе Паунд-стоуна [Poundstone, 1988, Chapter 9].
Рассмотрим такой пример. Пусть имеются две аксиомы, представленные на некотором формальном языке:
"Если компьютер может ошибаться, он ошибется" и
"Мой компьютер может ошибаться".
Тогда, используя механизм исчислений только правил влияния, мы можем показать, что справедлива теорема.
"Мой компьютер ошибется".
Это утверждение логически следует из заданных аксиом в том смысле, что оно не может быть ложным, если истинны исходные утверждения (аксиомы). Корректности такого следствия легко доказываются компьютером — все, что от него требуется, так это обработать выражения в форме логической зависимости:
(любой Х)(F(X))
F(a) / [G(a){X/a}]
которое читается следующим образом:
"Все элементы F являются элементами G, а входит в F, следовательно, F есть G".
Как и в случае с головоломками, некоторые концепции и методы, разработанные в области машинного доказательства теорем (иногда эту область исследований называют automated reasoning — машинным поиском логического вывода), весьма помогут студентам при решении практических проблем. Итак, знания, касающиеся решения некоторой проблемы, можно представить как набор аксиом, т.е. теорию, а процесс поиска решения проблемы можно рассматривать как попытку доказать теорему, каковой является искомое решение (подробнее об этом — в главе 8). Другими словами, поиск решения среди сформулированных теорем аналогичен поиску пути на графе в пространстве состояний и для его анализа можно использовать тот же аппарат.