Дерево опровержения. 
Системы поддержки принятия решений часть 1

Выбранную стратегию опровержения удобно отображать в виде графа с корневой вершиной с пометкой Л. Такой граф не только придает процессу наглядность, но и предостерегает от ошибочных или просто повторных шагов. Выше мы рассматривали пример с математиками (см. пример 3.16). Построим соответствующее ему дерево опровержения. Для каждого базового предложения отведем свою вершину. Если две вершины образуют родительскую пару, то исходящие из них ребра будут сходиться к вершине, помеченной их резольвентой, — потомком.

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

Согласно стратегии опорного множества процесс опровержения строится так, что, по крайней мере, один из родителей в каждой резольвенте выбирается из предложений, полученных при отрицании заключения (целевая ППФ) или их потомков (опорное множество). Эта стратегия обладает полнотой, т. е. можно показать, что если опровержение существует, оно может быть найдено по алгоритму стратегии опорного множества. Его применение приводит к более медленному росту числа резольвент (особенно в ширину) при большей интенсивности проникновения в глубину (увеличивая количество уровней). Такое движение как раз способствует поиску пустого дизъюнкта. Дерево опровержения на рис. 3.1 могло бы быть порождено стратегией опорного множества.

Рис. 3.1. Дерево опровержения.

Можно утверждать, что стратегия предпочтения одночленам есть модификация предыдущей. Стратегия же здесь заключается в том, что на каждом шаге резолюции мы пытаемся в качестве одной из родительских вершин выбирать однолитерное предложение. В такой стратегии заключается определенный смысл: когда в резолюции используется одночлен, резольвента содержит меньшее по сравнению с другим родителем число литералов. Процесс целенаправленно движется в сторону увеличения однолитерных резольвент, что способствует получению пустого дизъюнкта. Рисунок 3.1 может служить примером указанной стратегии.

Особенность линейной по входу стратегии состоит в том, что в каждой резолюции одно из родительских предложений принадлежит базовому множеству. Такое начало нам уже знакомо по стратегии полного перебора. Но там, повинуясь другой идее, алгоритм постепенно уходит в сторону. Если же следовать стратегии, линейной по входу, то можно было бы заметить, что она приводит к заметному снижению порождаемых дизъюнктов. Отметим, что граф опровержения на рис. 3.1 соответствует стратегии, линейной по входу. Обратите внимание: в данном случае на каждом шаге резолюции здесь участвует резольвента, полученная на предыдущем шаге. Такое дерево называется дерево-лоза. Заметим, однако, что известны случаи, когда эта стратегия не приводила к желаемому результату, хотя опровержение заведомо существовало. Это означает, что стратегия, линейная по входу, не является полной, что следует учитывать при ее использовании. Так, мы сейчас рассмотрим простой пример, когда строгое следование лозе не приводит к желаемому и такому близкому результату, но небольшое изменение в алгоритме дает прекрасный результат.

Пример 3.18.

Имеется система предложений:

Соответствующее дерево-лоза приводится на рис. 3.2. Необходимые подстановки здесь очевидны.

Рис. 3.2. Линейное по входу опровержение с коррекцией алгоритма.

Среди базовых предложений не нашлось однолитерного для образования пустого дизъюнкта. Спасла положение резолюция с одним из потомков.