12.3. Стратегии, учитывающие ход вывода

12.3.0. Введение

Обсудим теперь более сложные стратегии, в которых допустимые резолюции определяются требованиями, налагаемыми на допустимые операции вывода для разрешаемых предложений. Стратегии, учитывающие ход вывода, довольно эффективны, так как позволяют выигрывать как в числе рассматриваемых резолюций, так и в объеме машинной памяти, необходимой для записи выведенных предложений. Если известно, что для некоторого предложения есть вывод, не удовлетворяющий требованиям, налагаемым на резолюции, допускаемые выбранной стратегией, то незачем хранить это предложение, поскольку оно никогда не понадобится в последующих резолюциях. На самом деле такая ситуация встречается часто. При использовании стратегий, учитывающих ход вывода, возникают трудности, связанные с эффективностью. Для того чтобы установить, пригодится ли конкретное предложение в резолюции, надо хранить в памяти информацию о том, как оно было получено. Это, безусловно, приводит к дополнительным затратам машинной памяти и машинного времени. При некоторых стратегиях предложение, годное для резолюции на этапе процесса вывода, может не годиться для резолюции на этапе (Обратное неверно.) Это означает, что должна быть предусмотрена процедура „сборки мусора” для удаления из памяти предложений, которые стали не нужны. Даст ли это выигрыш, зависит от величины сэкономленной памяти и сложности вычислений, связанных со сборкой мусора.

12.3.1. Несущее множество

В большинстве задач доказательства теорем множество можно разбить на два подмножества, одно из которых состоит из аксиом рассматриваемой системы, а другое — из отрицаний

тех предложений, которые надо доказать. Обычно бывает разумно предположить, что аксиомы внутренне непротиворечивы, т. е. что множество выполнимо. Вос, Карсон и Робинсон (1965) доказали, что в этом случае при невыполнимости можно вывести последовательностью резолюций, в каждой из которых участвует по крайней мере одно предложение из несущего множества, т. е. такого множества, которому принадлежат

(i) все предложения из

и

(ii) резольвента, если хотя бы одно из ее родительских предложений принадлежит несущему множеству.

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

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

Возможны следующие наименьшие невыполнимые множества:

Заметим, что пустое предложение легко вывести из любого множества . К тому же, если задано то любое предложение можно определить как несущее множество, поскольку все собственные подмножества наименьшего невыполнимого множества выполнимы.

12.3.2. Линейный вывод

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

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

Вот один из линейных выводов пустого предложения из

Вывод (62) изображен в виде графа на рис. 12.6. Каждое предложение имеет в качестве левого родительского предложения и в качестве правого родительского предложения. Каждое предложение либо задано, либо для некоторого

Стратегия линейного вывода, относящаяся к стратегии очищения, полна (Андерсон и Бледсоу, 1970) и потому может быть полезна при написании программ доказательства теорем. Интересно проследить, как программа, использующая такую стратегию очищения, приходит к выводу пустого предложения Предположим, что — наименьшее невыполнимое множество. Тогда найдется по крайней мере один линейный вывод пустого предложения в котором участвуют все предложения из но нельзя узнать заранее, какой из них (если их несколько) приводит к быстрее. К тому же не все линейные выводы, начинающиеся с заданного предложения, окончатся и заранее нельзя указать те, которые не приводят к . В результате программе доказательства теорем приходится решать задачу поиска на дереве, аналогичную обсуждавшимся в гл. 10. Это отражено на рис. 12.7, где показаны связи между различными предложениями, выведенными такой программой. Корень дерева соответствует началу программы. Узлы, расположенные непосредственно под корнем, представляют

(кликните для просмотра скана)

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

12.3.3. Доказательство с леммами

Метод, который мы изложим здесь, не удовлетворяет условиям линейного вывода. В нескольких словах, в методе доказательства с леммами объединяются две или несколько самостоятельных линий доказательства. Примером такого доказательства может служить вывод из (61) пустого предложения

Соответствующий граф изображен на рис. 12.8. Заметим, что частные выводы независимо начинаются от нескольких исходных предложений, относящихся к а затем сливаются. Это напоминает абстрактное изображение работы резолюции на рис. 12.5. Обычно правила доказательства с леммами не столь ясны, как правила линейного вывода. Понятие об этом методе доказательства мы ввели в основном как альтернативу линейному выводу. С другой стороны, вывод (63) короче линейного вывода (62) и, значит, его можно считать „более изящным. Но хотя часто линейный вывод оказывается более длинным, его легче реализовать на вычислительной машине. Например, для вывода (63) все же надо было прежде догадаться о том, с каких предложений начать, а это, как известно, плохо формализуется. Что же касается вывода (62), его легко осуществить весьма понятной машинной процедурой.