В этой главе приведен анализ логического вывода в логике первого порядка и многих алгоритмов его выполнения.

•    В первом подходе используется правило логического вывода для конкретизации кванторов в целях преобразования задачи логического вывода в форму пропозициональной логики. Как правило, этот подход характеризуется очень низким быстродействием.

•    Использование унификации для выявления подходящих подстановок для переменных позволяет устранить этап конкретизации в доказательствах первого порядка, в результате чего этот процесс становится гораздо более эффективным.

В поднятой версии правила отделения унификация применяется для получения естественного и мощного правила логического вывода — обобщенного правила отделения. В алгоритмах прямого логического вывода и обратного логического вывода это правило применяется к множествам определенных выражений.

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

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

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

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

Недостатками обратного логического вывода являются излишние этапы логического вывода и бесконечные циклы; эти недостатки можно устранить путем запоминания.

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

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