Стратегия вычеркивания

Дизъюнкт называется поддизъюнктом (или поглощает ), если является некоторой частью дизъюнкта . При этом называется наддизъюнктом для . Например, если , , то - поддизъюнкт, а наддизъюнкт для .

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

1.

2.

3.

4.

____________________________

: 5. (1,2)

6. (1,3)

7. (2,4)

8. (3,4)

____________________________

ð (5,8)

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

Дата добавления: 2015-06-27