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

"Мой компьютер ошибется".

Это утверждение логически следует из заданных аксиом в том смысле, что оно не может быть ложным, если истинны исходные утверждения (аксиомы). Корректности такого следствия легко доказываются компьютером — все, что от него требуется, так это обработать выражения в форме логической зависимости:

(любой Х)(F(X)) G(X))

F(a) / [G(a){X/a}]

которое читается следующим образом:

"Все элементы F являются элементами G, а входит в F, следовательно, F есть G".

Как и в случае с головоломками, некоторые концепции и методы, разработанные в области машинного доказательства теорем (иногда эту область исследований называют automated reasoning — машинным поиском логического вывода), весьма помогут студентам при решении практических проблем. Итак, знания, касающиеся решения некоторой проблемы, можно представить как набор аксиом, т.е. теорию, а процесс поиска решения проблемы можно рассматривать как попытку доказать теорему, каковой является искомое решение (подробнее об этом — в главе 8). Другими словами, поиск решения среди сформулированных теорем аналогичен поиску пути на графе в пространстве состояний и для его анализа можно использовать тот же аппарат.

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

Эвристический поиск

Поскольку слепой поиск возможен только в небольшом пространстве вариантов, напрашивается совершенно естественный вывод, что необходим некоторый способ направленного поиска. Если такой способ использует при поиске пути на графе в пространстве состояний некоторых знаний, специфических для конкретной предметной области, его принято называть эвристическим поиском. Лучше всего рассматривать эвристику в качестве некоторого правила влияния, которое, хотя и не гарантирует успеха (как детерминированный алгоритм или процедура принятия решения), в большинстве случаев оказывается весьма полезным.

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

Например, простая оценочная функция для программы игры в шахматы может включать очевидную оценку материала (количества и качества имеющихся на доске фигур) — своего и соперника. Затем программа перебирает возможные операторы перехода в новое состояние (возможные ходы фигур) и, сравнивая результаты вариантов, отыскивает такой, который характеризуется максимальным значением оценочной функции. Другими словами, ищется такой ход, который дает наибольший материальный выигрыш.