Системы прямой дедукции. Системы обратной дедукции.

Системы прямой дедукции

В системах прямой дедукции новые знания получают, применяя выводы к фактам и правилам. Алгоритм завершает работу при получении некоторого знания, эквивалентного цели (или непосредственно влекущего ее). Для иллюстрации системы прямой дедукции обратимся снова к предыдущему примеру. Докажем теорему

(Факт (1) Факт (2) Правило (1)) Цель (1).

· Этап(1):

Преобразуем Факт(1) и Правило (1)) в дизъюнкты, чтобы применить затем метод резолюций. С помощью резолюции выводим новое правило (2), используя обозначение

Факт(1) Правило (1)

Правило (2)

Факт(1): Правило (1):

Проф(Инфо, Жак_2)

Правило (2):

· Этап (2): из Факта (2) и Правила (2) резолюцией выводим новый

Факт(3):

Факт(2): Правило(2)

Студ(Мат, Мари_4)

Факт(3): Экзам(Жак_2, Мари_4)Равно(Инфо,Мат)=Л

(Отношение Равно(Инфо,Мат)=Л должно быть явно указано в БД)

· Этап (3):

Факт(3) соответствует Цели(1). Следовательно, она подтверждена. Аналогично выведем утверждение Л из Факта(3) и отрицания Цели(1):

Факт(3): Цель(1):

Экзам(Жак_2, Мари_4) Экзам(Жак_2, Мари_4)

Систему прямой дедукции можно трактовать как систему, в которой применяется теорема о прямой дедукции: Если F1, F2, … , Fn, G - логические выражения, то G является логическим следствием из F1, F2, … , Fn тогда и только тогда, когда логическое выражение(F1 … FnG) тождественно ложно, т.е. невыполнимо. Правила вывода и стратегии, используемые в системах прямой дедукции, графически представимы И/ИЛИ - деревьями.

Системы обратной дедукции

В системах обратной дедукции выводы применяют к цели и к правилам, чтобы построить новые частичные цели. Алгоритм завершает работу, когда все частичные цели соответствуют фактам. Такую систему можно толковать с логической точки зрения как систему, в которой применяется теорема об обратной дедукции, которая гласит: Если F1, F2, … , Fn, G - логические выражения, то G является логическим следствием из F1, F2, … , Fn тогда и только тогда, когда логическое выражение (тождественно истинно, т.е. общезначимо.

В системах обратной дедукции правила и цели преобразуют в конъюнкты, чтобы применить затем правило согласия

· Этап (1): из Цели (1) и отрицания Правила(1), используя правило согласия, выводим новую Цель (2):

Цель(1) Правило(1)

Экзам(Жак_2. Мари_4)

Цель(2):

· Этап (2): из Цели (2) и отрицания Факта(1), с помощью правила согласия, выводим Цель (3):

Цель(2): Факт(1):

Проф(Инфо, Жак_2)

Цель (3):

Студ(z, Мари_4)Равно(Инфо, z)

· Этап (3): из Цели (3) и отрицания Факта(2) выводим теорему:

Цель (3): Факт(2):

Студ(z, Мари_4)Равно(Инфо, z) Студ(Мат, Мари_4)

Равно(Инфо,Мат)=И

Друзья! Приглашаем вас к обсуждению. Если у вас есть своё мнение, напишите нам в комментарии.