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

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

(9.1)

Затем применим правило конкретизации высказывания с квантором всеобщности к первому высказыванию, используя все возможные подстановки базовых термов из словаря этой базы знаний— в данном случае {х/John} и {х/Richard}. Мы получим следующие высказывания:

и отбросим высказывание с квантором всеобщности. Теперь база знаний становится по сути пропозициональной, если базовые атомарные высказывания (King {John), Greedy {John) и т.д.) рассматриваются как пропозициональные символы. Поэтому теперь можно применить любой из алгоритмов полного пропозиционального вывода из главы 7 для получения таких заключений, как Evil {John).

Как показано в разделе 9.5, такой метод пропозиционализации (преобразования в высказывания пропозициональной логики) может стать полностью обобщенным; это означает, что любую базу знаний и любой запрос в логике первого порядка можно пропозиционализировать таким образом, чтобы сохранялось логическое следствие. Таким образом, имеется полная процедура принятия решения в отношении того, сохраняется ли логическое следствие... или, возможно, такой процедуры нет. Дело в том, что существует такая проблема: если база знаний включает функциональный символ, то множество возможных подстановок базовых термов становится бесконечным! Например, если в базе знаний упоминается символ Father, то существует возможность сформировать бесконечно большое количество вложенных термов, таких как Father {Father {Father {John) ) ). А применяемые нами пропозициональные алгоритмы сталкиваются с затруднениями при обработке бесконечно большого множества высказываний.