Стратегия опорного множества

Стратегия полного перебора.

В этой стратегии сначала вычисляются все резольвенты первого уровня, а затем все резольвенты второго уровня и т.д. Резольвенты первого уровня являются резольвентами для предложений из базового (исходного) множества.

Резольвентой i-ого уровня является такая резольвента, чей самый глубокий родитель является резольвентой i – 1 уровня.

Стратегия является полной, но весьма не эффективной.

Рис.13. Стратегия полного перебора

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

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

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

Рис.14. Стратегия опорного множества

Доказательство истинности нашего целевого высказывания не единственно (так как несколько NIL).

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