8.11. БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕЧАНИЯ

Обсуждения стратегий перебора

Проблема построения эвристически эффективных стратегий перебора (поиска) при условии сохранения логической полноты прекрасно изложена в статье Дж. Робинсона (1967). Г. Робинсон и др. (1964) дали ясное описание нескольких стратегий и привели много примеров.

Стратегии упрощения

Проблема исключения подслучаев в процессе поиска доказательства оказывается тоньше, чем это может показаться. В статье Ковальского (1970а) указаны некоторые несоответствия в исследовании данной проблемы Ковальским и Хэйесом (1969); полностью этот вопрос рассмотрен в диссертации Ковальского (1970б),

Стратегии очищения

Стратегия формы с отфильтрованными предшествующими вершинами (-формы) является простейшей из семейства связанных между собой стратегий. В теореме 8.1 утверждается, что -стратегия логически полна; доказательство этой теоремы приведено в работе Лакхэма (1969). Хотя мы здесь показали, что полнота стратегии поддерживающего множества следует из теоремы 8.1, на самом деле она была разработана раньше (Вое и др., 1965).

Существуют разные пути дальнейшего усовершенствования -стратегии. В некоторых случаях их объединяют со стратегией, предложенной Эндрюсом (1968), использующей слияния. Среди работ, в которых доказывается полнота -формы со слиянием, укажем работы Киберца и Лакхэма (1971), Йейтса, Рафаэля и Харта (1970), Андерсона и Бледсоу (1970). В первой содержатся другие результаты, касающиеся свойств доказательств в -форме, а в двух последних применяются сравнительно новые методы доказательства полноты, представляющие самостоятельный интерес. Андерсон и Бледсоу доказали своим методом полноту и других стратегий. В статье Лавленда (1968) устанавливается полнота еще одного ограничения на -стратегию.

Модельные стратегии представляют собой развитие -дедукций, предложенных впервые Дж. Робинсоном (19656). Слейджл (1967) доказал полноту некоторых очень общих модельных стратегий. Теорема 8.2 взята у Лакхэма (1969); она является простым частным случаем одной из теорем Слейджла. Мельцер (1966, 1968) предлагает дополнительные результаты, касающиеся дедукций -типа.

Стратегии упорядочения

Стратегия предпочтения одночленам была предложена и оправдана Восом и др. (1964). Она и стратегия поддерживающего множества включены как основные элементы в ряд автоматических доказателей теорем.

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

имеющуюся семантическую информацию, и форму предложений-кандидатов. Некоторые теоретические результаты о свойствах стратегий с оценочными функциями содержатся в статье Ковальского (1970а). Его результаты о поиске на структурах «графов вывода» аналогичны результатам Харта и др. (1968) для структур графов в пространстве состояний.

Примеры реализации

Уже написано несколько программ для автоматического доказательства теорем. Например, программы Робинсона и Воса (1969), Аллена и Лакхэма (1970), Гарда и др. (1969), а также система Грина — Рафаэля — Йейтса, модифицированная Гарвеем и Клингом (1969).

Задачи

(см. скан)

(см. скан)