Обратная цепочка
Обратная цепочка (также англ. backward reasoning — «обратное рассуждение») — метод вывода знаний, который описывается как движение от цели к исходным данным. Обратная цепочка используется в автоматические системы доказательства теорем, машинах вывода, ассистентах доказательства и других приложениях искусственного интеллекта[1].
В теории игр обратная цепочка используется для анализа (более простых) подигр и поиска решения всей игры в процессе, известном как обратная индукция. В шахматах аналогичная стратегия известна как ретроградный анализ, который применяется для вычисления таблиц эндшпиля в компьютерных шахматах.
В логическом программировании обратная цепочка реализуется при помощи разрешения SLD. Оба подхода основаны на правиле вывода modus ponens. Обратная цепочка является одним из двух наиболее используемых методов логического вывода с помощью правил вывода и логических импликаций; вторым методом является прямая цепочка. Обычно системы, реализующие обратную цепочку, используют стратегию поиска в глубину (например, Prolog)[2].
Применение
Обратная цепочка начинается с перечня целей (или гипотез) и движется обратно — от следствия к основанию, чтобы определить, подтверждают ли какие-либо данные выбранные следствия. Машина вывода, использующая обратную цепочку, будет искать среди правил вывода такое, где следствие (часть Тогда) совпадает с искомой целью. Если основание (Если) этого правила не известно как истинное, то оно добавляется к списку целей (чтобы подтвердить изначальную цель, требуется также предоставить данные, подтверждающие новую подцель).
Например, пусть новый питомец по имени Фриц доставлен в непрозрачной коробке, и о нём известно два факта:
- Фриц квакает
- Фриц ест мух
Цель — узнать, зелёный ли Фриц, используя базу правил из четырёх правил:
- Если X квакает и X ест мух — тогда X лягушка.
- Если X чирикает и X поёт — тогда X канарейка.
- Если X лягушка — тогда X зелёный.
- Если X канарейка — тогда X жёлтый.
Используя обратную цепочку, машина вывода может установить, что Фриц зелёный, за четыре шага. Начальный запрос формулируется как цель, которую требуется доказать: «Фриц зелёный».
1. Фриц подставляется вместо X в правило №3 — проверяем, совпадает ли следствие с целью, правило преобразуется в:
Если Фриц лягушка — тогда Фриц зелёный.
Поскольку следствие совпадает с целью («Фриц зелёный»), далее необходимо установить истинность основания («Фриц лягушка»). Это основание становится новой целью:
Фриц лягушка.
2. Опять подставляя Фриц вместо X, правило №1 становится:
Если Фриц квакает и Фриц ест мух — тогда Фриц лягушка.
Так как следствие совпадает с текущей целью («Фриц лягушка»), необходимо проверить основание («Фриц квакает и ест мух»). Оно становится следующей целью:
Фриц квакает и Фриц ест мух.
3. Эта цель — конъюнкция двух утверждений, поэтому машина вывода разбивает её на две подцели, которые обе должны быть доказаны:
Фриц квакает Фриц ест мух.
4. Для доказательства обеих подцелей машина вывода отмечает, что оба факта заданы изначально, следовательно, их конъюнкция истинна:
Фриц квакает и Фриц ест мух,
что означает истинность основания правила №1 и, следовательно, следствия:
Фриц лягушка,
а значит, истинно и основание правила №3, значит, верно и его следствие:
Фриц зелёный.
Таким образом, машина вывода может доказать, что Фриц зелёный. Правила №2 и №4 не понадобились.
Стоит отметить, что цели всегда сопоставляются только с утверждёнными версиями следствия импликаций (а не с их отрицанием, как в правиле modus tollens), и когда есть совпадение, в качестве новой цели рассматривается основание (а не результат, как при утверждении следствия утверждение следствия). В конечном счёте, цель должна совпасть с известными фактами (обычно определяемыми как следствия правил, чьи основания всегда истинны). Таким образом, используемое правило вывода — modus ponens.
Поскольку перечень целей определяет, какие правила будут выбраны и использованы, метод называется целенаправленным (goal-driven) — в отличие от данно-ориентированного вывода по прямой цепочке. Обратная цепочка часто применяется в экспертных системах.
Языки программирования, такие как Prolog, Knowledge Machine и ECLiPSe, поддерживают обратную цепочку в своих машинах вывода.
Примечания
Литература
- Russell, Stuart. Artificial Intelligence: A Modern Approach : [англ.] / Stuart Russell, Peter Norvig. — Prentice Hall, 2009. — ISBN 978-0-13-604259-4.