12.2.2. Исключение тавтологий и уникальных литералов

Задача стратегий очищения состоит в том, чтобы удалить неподходящие предложения из до проведения резолюции. Пусть будет невыполнимым множеством предложений, таким, что любое его собственное подмножество выполнимо 1), т. е. для доказательства невыполнимости необходимо использовать каждое предложение из по крайней мере один раз. Вообще говоря, будет более эффективным работать с а не с . В самом деле, можно доказать, что существует по крайней мере один вывод пустого предложения который начинается с любого предложения (Андерсон и Бледсоу, 1970). Поэтому было бы желательно обнаружить и удалить предложения, принадлежащие если такие существуют, прежде чем проводить резолюцию. В тех случаях, когда это оказывается возможным, к удалению некоторых из таких предложений приводит исключение тавтологий и уникальных литералов. Обе стратегии легко применяются.

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

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

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

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