3.10.7. Преимущества и ограничения метода резолюции
Метод доказательства, основанный на принципе резолюции, представляет интерес, так как является систематическим. Большое число публикаций, трактующих вопросы “автоматического доказательства”, посвящено методу резолюции начиная со времени появления работ Эрбрана и реализации этой идеи Робинсоном в 1965 г. Невозможность определить эффективную стратегию решения для всех областей приложения приводит к следующему выводу: для заданного набора предложений либо доказательство получается очень быстро на ЭВМ, либо оно не получается вовсе. Однако эффективность программ резко падает с увеличением числа предложений. Проблема заключается в том, чтобы определить тот момент, когда надо остановить программу, поскольку при этом существуют две опасности: во-первых, взрывное увеличение числа предложений, а во-вторых, возможность преждевременного прекращения работы перед самым моментом получения решения.
Практическая значимость и оригинальность метода резолюции определяются его двумя свойствами, описанными ниже.
1. Управление движением по дереву И-ИЛИ, обычно необходимое при всяком доказательстве, в данном случае отсутствует. Эту функцию выполняет стандартизованный набор предложений, причем может быть определена очень простая процедура обработки "выбор + унификация”.
2. Гипотезы, предположение и промежуточные предложения играют здесь одну и ту же роль. Доказательства получаются при одновременном движении в двух направлениях: от гипотез к заключениям и от заключений к гипотезам, причем доказательство достигается, когда оба эти пути просмотра встречаются друг с другом (рис. 3.23).
Существенным недостатком метода является то, что уже по построению он предназначен только для доказательства теорем. Он не пригоден для того, чтобы изобретать или придумывать некоторые предложения, а затем уже доказывать их, как это обычно делает математик. К тому же, если предположение не является теоремой, резолюция может привести к построению бесконечного дерева решения. Таким образом, метод резолюции
интересен благодаря простоте и систематичности, но, к сожалению, применим только для ограниченного числа случаев (доказательство не должно иметь большую глубину, а число потенциальных резолюций не должно быть большим).
Рис. 3.23. Схема получения доказательства методом резолюции.
