1.5. ИСПОЛЬЗОВАНИЕ ФОРМАЛЬНОЙ ЛОГИКИ ПРИ РЕШЕНИИ ЗАДАЧ
Часто для решения задачи либо требуется проведение логического анализа в определенном объеме, либо поиск решения существенно облегчается после такого анализа. Иногда такой анализ показывает, что определенные проблемы неразрешимы. В игре в пятнадцать, например, можно доказать, что целевая конфигурация
не может быть получена из начальной конфигурации
Необходимость делать логические заключения возникает как в подходах, основанных на использовании пространства состояний, так и в подходах, связанных с редукцией задач. В подходах первого типа логических выводов может потребовать тот тест, с помощью которого определяется, будет ли некоторое состояние состоянием, отвечающим поставленной цели. Кроме того, логические умозаключения могут понадобиться при определении, какой из операторов применим к данному состоянию.
Как мы уже видели, иногда можно доказать, что некоторая задача неразрешима. В подходах, основанных на редукции задачи, доказательство такого рода позволило бы избежать тщетных попыток разрешить неразрешимые подзадачи. В дополнение к таким приложениям мы хотим также иметь возможность решать задачи, которые представляют собой задачи на доказательство. Например, возможно, мы захотим найти доказательство некоторой мдтематической теоремы, записанной в определенной формальной системе, такой, как исчисление предикатов первого порядка.
Таким образом, полное исследование приемоврешения задач должно включать рассмотрение машинных методов поиска доказательства. Некоторые из этих методов опираются на стратегии поиска, подобные тем, которые мы будем обсуждать в связи с подходами, основанными на пространстве состояний и редукции задач. Хотя известно много способов выбора конкретного логического формализма, мы будем рассматривать разработанную в последнее время методику доказательства теорем в исчислении предикатов первого порядка, основанную на принципе резольвенций, и применения такой методики к решению задач. Этому будут посвящены гл. 6—8.
При обсуждении автоматического доказательства теорем мы покажем, что даже нематематические задачи могут быть сформулированы как теоремы, подлежащие доказательству. Многие из головоломок, которые мы рассмотрим, так же как и многие возникающие в реальной действительности задачи, требующие для их анализа здравого смысла, могут быть в принципе сформулированы в рамках определенного логического формализма и после этого решены методом доказательства теорем. Использование формальной логики и методов доказательства теорем позволяют нам думать о действительно «универсальном» решателе задач. Новая информация в такой решатель задач могла бы вводиться просто в форме внесения в его память новых дополнительных аксиом, а не посредством переделывания его программы. Он мог бы решать задачи из достаточно широких областей, поскольку существуют логические формализмы, достаточно универсальные для того, чтобы выразить любую информацию и записать любую задачу.
