В этой главе приведен анализ логического вывода в логике первого порядка и многих алгоритмов его выполнения. • В первом подходе используется правило логического вывода для конкретизации кванторов в целях преобразования задачи логического вывода в форму пропозициональной логики. Как правило, этот подход характеризуется очень низким быстродействием. • Использование унификации для выявления подходящих подстановок для переменных позволяет устранить этап конкретизации в доказательствах первого порядка, в результате чего этот процесс становится гораздо более эффективным. В поднятой версии правила отделения унификация применяется для получения естественного и мощного правила логического вывода — обобщенного правила отделения. В алгоритмах прямого логического вывода и обратного логического вывода это правило применяется к множествам определенных выражений. Обобщенное правило отделения является полным применительно к определенным выражениям, но проблема логического следствия остается полуразрешимой. Для программ Datalog, состоящих из определенных выражений без функций, проблема логического следствия разрешима. Прямой логический вывод используется в дедуктивных базах данных, где он может сочетаться с реляционными операциями баз данных. Он также применяется в продукционных системах, которые обеспечивают эффективное обновление при наличии очень больших наборов правил. Прямой логический вывод для программ Datalog является полным и выполняется за время, определяемое полиномиальной зависимостью. Обратный логический вывод используется в системах логического программирования, таких как Prolog, в которых реализована сложная технология компиляции для обеспечения очень быстрого логического вывода. Недостатками обратного логического вывода являются излишние этапы логического вывода и бесконечные циклы; эти недостатки можно устранить путем запоминания. Обобщенное правило логического вывода на основе резолюции позволяет создать полную систему доказательства для логики первого порядка с использованием баз знаний в конъюнктивной нормальной форме. Существует несколько стратегий сокращения пространства поиска для систем с резолюцией без потери полноты. Эффективные средства автоматического доказательства теорем на основе резолюции использовались для доказательства интересных математических теорем, а также для проверки и синтеза программных и аппаратных средств.
|