ЛОГИЧЕСКИЙ ВЫВОД В ЛОГИКЕ ПЕРВОГО ПОРЯДКА
В этой главе будут определены эффективные процедуры получения ответов на вопросы, сформулированные в логике первого порядка.
В главе 7 определено понятие логического вывода и показано, как можно обеспечить непротиворечивый и полный логический вывод для пропозициональной логики. В данной главе эти результаты будут дополнены для получения алгоритмов, позволяющих найти ответ на любой вопрос, сформулированный в логике первого порядка и имеющий ответ. Обладать такой возможностью очень важно, поскольку в логике первого порядка можно сформулировать практически любые знания, приложив для этого достаточные усилия.
В разделе 9.1 представлены правила логического вывода для кванторов и показано, как можно свести вывод в логике первого порядка к выводу в пропозициональной логике, хотя и за счет значительных издержек. В разделе 9.2 описана идея унификации и показано, как эта идея может использоваться для формирования правил логического вывода, которые могут применяться непосредственно к высказываниям в логике первого порядка. После этого рассматриваются три основных семейства алгоритмов вывода в логике первого порядка: прямой логический вывод и его применение к дедуктивным базам данных и продукционным системам рассматриваются в разделе 9.3; процедуры обратного логического вывода и системы логического программирования разрабатываются в разделе 9.4; а системы доказательства теорем на основе резолюции описаны в разделе 9.5. Вообще говоря, в любом случае следует использовать наиболее эффективный метод, позволяющий охватить все факты и аксиомы, которые должны быть выражены в процессе логического вывода. Но следует учитывать, что формирование рассуждений с помощью полностью общих высказываний логики первого порядка на основе метода резолюции обычно является менее эффективным по сравнению с формированием рассуждений с помощью определенных выражений с использованием прямого или обратного логического вывода.
СРАВНЕНИЕ МЕТОДОВ ЛОГИЧЕСКОГО ВЫВОДА В ПРОПОЗИЦИОНАЛЬНОЙ ЛОГИКЕ И ЛОГИКЕ ПЕРВОГО ПОРЯДКА
В этом и следующих разделах будут представлены идеи, лежащие в основе современных систем логического вывода. Начнем описание с некоторых простых правил логического вывода, которые могут применяться к высказываниям с кванторами для получения высказываний без кванторов. Эти правила естественным образом приводят к идее, что логический вывод в логике первого порядка может осуществляться путем преобразования высказываний в логике первого порядка, хранящихся в базе знаний, в высказывания, представленные в пропозициональной логике, и дальнейшего использования пропозиционального логического вывода, а о том, как выполнять этот вывод, нам уже известно из предыдущих глав. В следующем разделе указано одно очевидное сокращение, которое приводит к созданию методов логического вывода, позволяющих непосредственно манипулировать высказываниями в логике первого порядка.