Главная arrow книги arrow Копия Глава 9. Логический вывод в логике первого п arrow Эффективный прямой логический вывод
Эффективный прямой логический вывод

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

и фактом American (West). Затем это частичное согласование отбрасывается и снова формируется во второй итерации (в которой данное правило согласуется успешно). Было бы лучше сохранять и постепенно дополнять частичные согласования по мере поступления новых фактов, а не отбрасывать их.

В rete-алгоритме была впервые предпринята серьезная попытка решить эту проблему. Алгоритм предусматривает предварительную обработку множества правил в базе знаний для формирования своего рода сети потока данных (называемой rete-сетью), в которой каждый узел представляет собой литерал из предпосылки какого-либо правила. По этой сети распространяются операции связывания переменных и останавливаются после того, как в них не удается выполнить согласование с каким-то литералом. Если в двух литералах некоторого правила совместно используется какая-то переменная (например, в примере доказательства преступления), то варианты связывания из каждого литерала пропускаются через узел проверки равенства. Процессу связывания переменных, достигших узла η-арного литерала, такого как Sells (х, у, z), может потребоваться перейти в состояние ожидания того, что будут определены связывания для других переменных, прежде чем он сможет продолжаться. В любой конкретный момент времени состояние rete-сети охватывает все частичные согласования с правилами, что позволяет избежать большого объема повторных вычислений.