Глава 8. МЕТОДЫ ПОИСКА ДОКАЗАТЕЛЬСТВА В ИСЧИСЛЕНИИ ПРЕДИКАТОВ

81. СТРАТЕГИИ ПЕРЕБОРА

В гл. 6 мы отметили, что непосредственное применение принципа резольвенции соответствовало бы простой процедуре полного перебора при построении опровержения. Такой перебор мы начинали бы с множества предложений S, к которому добавляли бы все резольвенты всех пар предложений в S с тем, чтобы образовать множество . Затем добавляли бы все резольвенты всех пар предложений в с тем, чтобы образовать множества Этот тип перебора, как правило, непригоден для практики, ибо множества слишком быстро разрастаются. Практические процедуры доказательства определяются стратегиями перебора, применяемыми для его ускорения. Такие стратегии бывают трех типов: стратегии упрощения, стратегии очищения и стратегии упорядочения. Стратегии упорядочения точнее двух других стратегий соответствуют методам, применяемым при переборе на графах в пространстве состояний и «И/ИЛИ» графах. В настоящей главе мы кратко обсудим все три типа стратегий.

8.2. СТРАТЕГИИ УПРОЩЕНИЯ

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

Исключение тавтологий

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

можно отбросить.

Исключение путем означивания предикатов

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

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

Исключение подслучаев

Предложение называется подслучаем предложения если существует такая подстановка 0, что Например,

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

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