12.3.4. Совместное применение стратегий использования подслучаев и слияния

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

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

Рис. 12.8. Структура доказательства с леммами для примера (63).

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

образом, для заданного предложения можно ограничиться соответствующим подмножеством в

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

Здесь — литерал слияния. Хотя обозначения в этом примере относятся к линейному выводу, идея слияния столь же успешно может применяться и в доказательствах с леммами.

Андерсон и Бледсоу (1970), доказав следующую теорему, показали, что слияние, использование подслучаев и линейный вывод можно объединить.

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

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

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