Метод резолюций и стратегии поиска опровержений

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