3.    Могут быть наложены ограничения на язык представления, например, путем устранения функциональных символов или применения только хорновских выражений. Например, язык Progol оперирует с хорновскими выражениями с использованием обратного логического следствия. Идея этого метода состоит в том, что ограничение логического следствия:

должно быть преобразовано в такую логически эквивалентную форму:

Исходя из этой формы представления, для вывода гипотезы Hypothesis можно использовать процесс, аналогичный обычной дедукции Prolog с помощью хорновских выражений, в котором применяется отрицание как недостижение цели. Поскольку данный метод ограничивается хорновскими выражениями, он является неполным, но может оказаться более эффективным, чем полная резолюция. Кроме того, при обратном логическом следствии появляется возможность использовать полный логический вывод [717].

4.     Логический вывод может осуществляться с помощью проверки по модели, а не с помощью доказательства теоремы. В системе Progol [1098] для ограничения поиска используется определенная форма проверки по модели. Это означает, что в этой системе, как и в программировании множества ответов, вырабатываются все возможные значения логических переменных, которые затем проверяются на совместимость.

5.   Логический вывод может осуществляться с помощью базовых пропозициональных выражений, а не выражений в логике первого порядка. Система Linus [897] действует по принципу преобразования теорий логики первого порядка в выражения пропозициональной логики, поиска для этих выражений решений с помощью пропозициональной обучающейся системы, а затем обратного преобразования. Как было показано на примере алгоритма SATplan в главе 11, при решении некоторых задач может оказаться более эффективной организация работы с помощью пропозициональных формул.