Цепочка с прямым порядком рассуждений

И наконец, в самую последнюю очередь мы остановимся на теме, которой

мы уже кратко касались раньше: цепочка с прямым порядком рассуждений. Как

вы узнали, выполнение цепочки с обратным порядком рассуждений начинается

с предположения истинности гипотезы и последующих попыток подтвердить ее

с помощью правил и фактов, находящихся в базе правил. Цепочка с прямым

порядком рассуждений выполняется по-другому.

В этом случае мы начинаем с рассмотрения выражений истинность кото-

рых уже известна, т.е. с фактов базы данных. Затем мы посмотрим, смогут

ли эти факты подтвердить одно из правил базы данных. Если такое правило

есть, то оно включается в базу данных как еще один факт и возможно позво-

лит подтвердить еще несколько правил, которые в свою очередь становятся

фактами и т.д. до тех пор, пока будут установлены все факты.

Мы не дадим полное решение задачи. Однако, пользуясь перефразировкой

мысли из области Искусственного Интеллекта мы "Проиллюстрируем принципы,

не являющиеся законченным примером". Наш пример будет очень узким.

Есть два основных способа преобразования правила в факт, про который

известно, что он подтвержден, существующими в базе данных фактами:

1. Убрать правило и установить соответствующий ему факт.

2. Oтметить правило как подтвержденное.

Мы покажем как выполнить эти предположения, введя оптимизацию, в ко-

торой каждому правилу приписан свой собственный номер. Этот номер с по-

мощью предиката базы данных, который называется proven(<rule_no>), будет

указывать, подтверждено ли правило как факт.

Это не только ускоряет работу (алгоритм цепочки с прямым порядком

рассуждений очень сильно загружает процессор), но и позволяет снова на-

чать считать правило неподтвержденным после того, как его пометили, что

оно было подтверждено. Если бы мы применяли к правилу основной предикат

retract, то где-то пришлось бы накапливать удаленные правила, чтобы их

можно было внести снова.

Но почему может возникнуть необходимость в изменениях после того,

как правило было подтверждено? Это связано с объединением переменных.

Предположим, в базе правил содержится следующее:

numb(1).

numb(2).

rule(N):- numb(N).

pred:- rule(5).

Мы просматриваем правила, чтобы узнать, можно ли их подтвердить. На-

ходим rule(N) (правило(N)). Пытаемся доказать его, выясняя все ли термы

тела доступны в виде фактов, и находим numb(1), что позволяет установить

rule(1) как факт. Теперь имеем:

numb(1).

numb(2).

rule(1).

pred:- rule(5).

Ищем следующие правила и находим pred; попытка подтвердить содержи-

мое тела pred будет безуспешна, т.к. отсутствует факт, отмеченный как

rule(5). В этом месте у нас должна быть возможность вернуться к предыду-

щему утверждению, где rule еще не было установлено как факт, и попытаться

сделать что-либо другое; а именно, попытаться подтвердить numb(N) с по-

мощью факта numb(X) вместо numb(1).

numb(1).

numb(X).

rule(N):- numb(N).

pred:- rule(5).

Это позволит установить

numb(1).

numb(2).

rule(N).

pred:- rule(5).

с разделяемыми N и X. Нахождение pred позволит установить это как факт,

т.к. тело pred подтверждается соответствием rule(5) и rule(N).

Мы будем использовать предикат clause(integer, sTerm, sTerm) вместе

с пердикатом proven(integer) чтобы представлять и делать отметки в базе

правил, и версию unify_body, совпадающую с той, которую использовали в

цепочке с обратным порядком рассуждений, но исключим отсечение:

predicates

nondeterm unify_body(sTerm, Env, integer)

clauses

unify_body(cmp(",",[Term1, Term2]), Env):- !,

unify_body(Term1, Env),

unify_body(Term2, Env).

unify_body(cmp(";",[ATerm,_]), Env):-

unify_body(ATerm, Env).

unify_body(cmp(";",[_,ATerm]), Env):- !,

unify_body(ATerm, Env),

unify_body(cmp("not;",[_,ATerm]), Env):- !,

unify_body(ATerm, Env),

unify_body(cmp("not",_),_):- !,

unify_body(STerm, Env),

unify_body(cmp(PID, ATermList), Env,_):-

unify_terml(Call, ATermList), Env,_),

call(cmp(PID, Env).

unify_body(atom(PID), Env,_):-

call(cmp(PID, [], Env).

Минимальная версия call окажется еще более короткой:

predicates

nondeterm call(string, ATermList)

clauses

call(ID, ATermList):-

clause(cmp(ID, ATermList), atom("true)),

free(Env),

unify_term1(ATermList, ATermList, Env).

Единственной задачей unify_body и call является выяснение, содержат-

ся ли все подцели тела как факты в базе данных. В таком случае правило

оказывается истинным.