Математическая логика и теория алгоритмов

Стратегия вычеркивания зависит от того, как вычеркиваются тавтологии и на.цдизъюнкты. Стратегия вычеркивания будет полной, если ее использовать вместе с методом насыщения уровней следую­ щим образом: сперва выписываются дизъюнкты ( «S'^ViS'v...v5"'') по порядку; затем вычисляются резольвенты сравнением каждого дизъюнкта Die{^vS^v...v^'^) с дизъюнктом стоящим после Di. Когда резольвента вычислена, она записывается в конце списка, как только поровдается, если она не тавтология и не поглоща­ ется каким-нибудь дизъюнктом ия списка. В противном случае она вычеркивается. Очевидно, что при этом не выписывается повторно один и тот же дизъюнкт. Применим эту стратегию вычеркивания к примеру из § 4 и получим следующий список; ( 1 )Pve , ( 2 ) 1P v f i (3)Pv1 f i ( 4 ) l P v 1 f i S'; ( 5 ; б из (1) и (2), (б)р из (1)и(3), (7)1Р из (2) и (4), (8) I s из (3) и (4), • из (5) и (8). Получили существенно более короткий список. Следовательно, стратегия вычеркивания может уменьшить потребную память для реализации метода резолюций. Ясно, что необходимые вычисления не уменьшаются, а увели­ чиваются. Чтобы использовать стратегию вычеркивания, нужно уметь решать, является ли полученный дизъюнкт тавтологией или является ли один из дизъюнктов поддизъюнктом другого. Метод резолюций, как уже указано, позволяет автоматизировать доказательство теорем. Видно, что неограниченное применение резо­ люции может порождать много лишних и ненужных дизъюнктов на­ ряду с полезными. Хотя можно использовать стратегию вычеркива­ 97