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

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

В разделе 9.1 представлены правила логического вывода для кванторов и показано, как можно свести вывод в логике первого порядка к выводу в пропозициональной логике, хотя и за счет значительных издержек. В разделе 9.2 описана идея унификации и показано, как эта идея может использоваться для формирования правил логического вывода, которые могут применяться непосредственно к высказываниям в логике первого порядка. После этого рассматриваются три основных семейства алгоритмов вывода в логике первого порядка: прямой логический вывод и его применение к дедуктивным базам данных и продукционным системам рассматриваются в разделе 9.3; процедуры обратного логического вывода и системы логического программирования разрабатываются в разделе 9.4; а системы доказательства теорем на основе резолюции описаны в разделе 9.5. Вообще говоря, в любом случае следует использовать наиболее эффективный метод, позволяющий охватить все факты и аксиомы, которые должны быть выражены в процессе логического вывода. Но следует учитывать, что формирование рассуждений с помощью полностью общих высказываний логики первого порядка на основе метода резолюции обычно является менее эффективным по сравнению с формированием рассуждений с помощью определенных выражений с использованием прямого или обратного логического вывода.