Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

(39) ^ из (5) и (12). Было порождено много не относящихся к делу и лишних дизъюнктов. Например, (7), (8), (9) и (10) - тавтологии. Так как тавтология всегда истинна, то если вычеркиваем тавтологию из невыполнимого множества дизъюнктов, оставшееся множество должно быть невыполнимо. Следовательно, тавтология является не относяш,имся к делу дизъюнктом. Если она появляется, то (за исключением очень немногих случаев) ее следует вычеркнуть. Далее дизъюнкты Р, Q, —iP, —iQ порождаются неоднократно. Также имеются другие повторяющиеся дизъюнкты, см. (13) - (16), (20) - (23), (26) - (29) и (33) - (36). На самом деле, чтобы получить доказательство для S, нужно получить дизъюнкты (5), (12) и (39). Для сокращения избыточности рассмотрим стратегию вычеркивания. § 4. Стратегия вычеркивания Дизъюнкт Di называется поддизъюнктом D2, если Di является некоторой частью дизъюнкта D2. Нри этом D2 называется наддизъюнктом для Di. Пример. Пусть Di=P, Di=Pv Q. Известно, что P&(Pv Q)~ Р, следовательно, поддизъюнкт поглощает наддизъюнкт: Di& D2 ~ Di. Стратегия вычеркивания зависит от того, как вычеркиваются тавтологии и наддизъюнкты. Стратегия вычеркивания будет полной, если ее использовать вместе с методом насыщения уровней следующим образом: сначала выписываются дизъюнкты vSW... по порядку; затем вычисляются резольвенты путем сравнения каждого дизъюнкта DiE(S^ дизъюнктом СТОЯЩИМ после Д . Когда резольвента вычислена, она будет записана в конце списка, если она не тавтология и не поглощается каким- нибудь дизъюнктом из списка. Очевидно, что при этом не выписывается повторно один и тот же дизъюнкт. Применим эту стратегию вычеркивания к примеру из § 4 и получим следующий список: (l)PvQ, {2)^VQ, Ci)Pv^Q, S': {5)Q из(1)и(2), (6)i^ из (1)и(3), (7) из (2) и (4), (8) -.6 из (3) и (4), S^: из (5) и (8). 65