Какие существуют методы автоматизированного логического вывода?

Некоторые методы автоматизированного логического вывода (АЛВ):

• Прямой логический вывод. img.avalon.ru К нему относятся, например, метод резолюций (эффективность, полнота, гибкость, но формирование избыточных дизъюнктов) и алгоритм DPLL (простота и эффективность, но применим только для логики высказываний). img.avalon.ru
• Обратный логический вывод. img.avalon.ru К нему относятся обратный метод Маслова (эффективный, можно совмещать с другими методами, но не является полным) и алгоритм FOL-BC-Ask (простота реализации, но неэффективность, не является полным). img.avalon.ru
• Направления поиска вывода. disser.spbu.ru Выделяют два направления: сверху вниз (от аксиом к доказываемой формуле) и снизу вверх (от доказываемой формулы к аксиомам). disser.spbu.ru
• Стратегии поиска вывода. disser.spbu.ru Например, удаление избыточных ветвей дерева поиска вывода или использование фиксированного порядка применений правил вывода. disser.spbu.ru
• Стратегия поглощения. disser.spbu.ru Одна из основных стратегий поиска вывода для разных методов АЛВ, позволяющая исключать из рассмотрения избыточные ветви дерева поиска вывода. disser.spbu.ru