Метод обратного исключения для логических задач заключается в последовательном исключении нежелательных вариантов решения. 14

Алгоритм метода: 2

1. На первом шаге каждый предикат целевой формулы, содержащий переменные, подвергается возможной замене на соответствующий факт базы знаний. 2 Новая полученная целевая формула рекурсивно анализируется по точно такому же алгоритму. 2
2. После того как все возможные подобные замены произведены, для каждого предиката целевой формулы ищется соответствующее правило базы знаний, согласно которому данный предикат можно заменить последовательностью других предикатов, составляющих условие правила. 2 Новая формула также рекурсивно подвергается точно такой же процедуре, начиная с первого шага. 2
3. Процесс продолжается до тех пор, пока целевая формула не превратится в аксиому, то есть все её предикаты не станут тождественно равными какому-либо факту базы знаний. 2 Если какой-либо предикат становится невозможно упростить, заменив его фактом либо применив к нему правило, то анализ такой целевой формулы также прекращается, так как она становится заведомо ложной. 2

Таким образом, целевая формула разбивается на части, которые заменяются новыми формулами, истинность которых легче установить в рамках заданных фактов. 2