Обратная цепочка (или обратное рассуждение ) — это метод вывода , который в просторечии описывается как работа в обратном направлении от цели. Он используется в автоматизированных средствах доказательства теорем , машинах вывода , помощниках по доказательству и других приложениях искусственного интеллекта . [1]
В теории игр исследователи применяют его к (более простым) подиграм , чтобы найти решение игры, в процессе, называемом обратной индукцией . В шахматах это называется ретроградным анализом , и он используется для создания баз таблиц шахматных эндшпилей для компьютерных шахмат .
Обратная цепочка реализуется в логическом программировании с помощью разрешения SLD . Оба правила основаны на правиле вывода modus ponens . Это один из двух наиболее часто используемых методов рассуждения с правилами вывода и логическими выводами ; второй — прямая цепочка . Системы обратной цепочки обычно используют стратегию поиска в глубину , например Пролог . [2]
Обратная цепочка начинается со списка целей (или гипотезы ) и работает в обратном направлении от консеквента к антецеденту , чтобы увидеть, поддерживают ли какие-либо данные какой-либо из этих консеквентов. [3] Механизм вывода , использующий обратную цепочку, будет искать правила вывода , пока не найдет одно с консеквенцией ( предложение then ), которое соответствует желаемой цели. Если антецедент ( предложение If ) этого правила не известен как истинный, то он добавляется в список целей (для подтверждения цели необходимо также предоставить данные, подтверждающие это новое правило).
Например, предположим, что новый питомец Фриц доставлен в непрозрачной коробке вместе с двумя фактами о Фрице:
Цель состоит в том, чтобы решить, зеленый ли Фриц, на основе базы правил , содержащей следующие четыре правила:
С помощью обратного рассуждения машина вывода может определить, зеленый ли Фриц, за четыре шага. Для начала запрос формулируется как утверждение цели, которое необходимо доказать: «Фриц зеленый».
1. Фриц заменяется на X в правиле №3, чтобы проверить, соответствует ли его последовательность цели, поэтому правило №3 становится следующим:
Если Фриц — лягушка, то Фриц зеленый.
Поскольку консеквент соответствует цели («Фриц — зеленый»), механизму правил теперь необходимо проверить, можно ли доказать антецедент («Фриц — лягушка»). Таким образом, антецедент становится новой целью:
Фриц — лягушка
2. Снова заменив X на Fritz, правило №1 будет выглядеть следующим образом:
Если Фриц квакает, а Фриц ест мух – Тогда Фриц – лягушка
Поскольку консеквент соответствует текущей цели («Фриц — лягушка»), механизм вывода теперь должен проверить, можно ли доказать антецедент («Фриц квакает и ест мух»). Таким образом, антецедент становится новой целью:
Фриц квакает, а Фриц ест мух.
3. Поскольку эта цель представляет собой объединение двух утверждений, машина вывода разбивает ее на две подцели, обе из которых должны быть доказаны:
Фриц каркает Фриц ест мух
4. Чтобы доказать обе эти подцели, машина вывода видит, что обе эти подцели были заданы как исходные факты. Следовательно, союз верен:
Фриц квакает, а Фриц ест мух.
следовательно, антецедент правила № 1 истинен, и консеквент должен быть истинным:
Фриц — лягушка
следовательно, антецедент правила № 3 истинен, и консеквент должен быть истинным:
Фриц зеленый
Таким образом, этот вывод позволяет машине вывода доказать, что Фриц зеленый. Правила №2 и №4 не использовались.
Обратите внимание, что цели всегда соответствуют подтвержденным версиям последствий импликаций (а не отрицаемым версиям, как в modus tollens ), и даже в этом случае их антецеденты тогда рассматриваются как новые цели (а не выводы, как при подтверждении консеквента ). которые в конечном итоге должны соответствовать известным фактам (обычно определяемым как последствия, антецеденты которых всегда верны); таким образом, используемое правило вывода — это modus ponens .
Поскольку список целей определяет, какие правила выбираются и используются, этот метод называется целенаправленным , в отличие от прямого вывода на основе данных . Подход обратной цепочки часто используется экспертными системами .
Языки программирования, такие как Prolog , Knowledge Machine и ECLiPSe, поддерживают обратную цепочку в своих механизмах вывода. [4]