Scientific journal
Modern high technologies
ISSN 1812-7320
"Перечень" ВАК
ИФ РИНЦ = 0,940

OUT OF NEW FACTS SEQUENCES INFERENCE METHOD BASED NOT FULLY DEFINED KNOWLEDGEBASE IN PREDICATE CALCULUS

Dolzhenkova M.L. 1 Strabykin D.A. 1
1 Vyatka State University
The paper presents the method of sequences inference in predicate calculus of the new facts in the case where the knowledge base is not fully defined. The method allows to obtain an answer to the question: «What are the sequences (deducible facts) can be obtained by having a set of basic assumptions in the changed circumstances of external environment characterized by new facts entered and what additional facts may be required to produce these sequences?». Similar problems arise in many areas of human activity: forecasting, monitoring, diagnostics, formal verification and others. The method is based on the disjuncts division operation. The paper presents: a formal statement of the problem of the sequences inference with not fully defined knowledgebase, the description of the partial and complete disjuncts division procedures, inference procedure and inference method. Working of method are illustrated by example.
sequences inference
abductive sequences
not fully defined knowledgebase
additional facts
predicate calculus
disjuncts division

В большинстве случаев на практике база знаний интеллектуальной системы строится на основе логической модели [1]. В ней содержатся исходные посылки, которые можно разделить на два класса: первый класс – данные, представляющие факты возникновения тех или иных событий, явлений (признаков, действий и т.д.), и второй класс – правила, задающие связи фактов между собой.

В ходе работы интеллектуальной системы в нее могут поступить новые факты, которые отражают изменение некоторой внешней среды. Определение возможных последствий изменений, представляемых новыми фактами, осуществляется с помощью дедуктивного вывода следствий из новых фактов с использованием базы знаний. При этом возможны случаи, когда на очередном шаге дедуктивного вывода не удается вывести следствия из-за того, что база знаний не полностью определена – в ней не хватает некоторых фактов [5].

В таких случаях используется специальный вывод, который дает возможность найти дополнительные факты, обеспечивающие успешный вывод следствий на данном шаге. Такие следствия называются в работе «абдуктивными» следствиями в отличие от «обычных» дедуктивных следствий.

Задачу вывода следствий можно сформулировать следующим образом: при заданной базе исходных посылок для некоторого (нового) набора фактов определить множество следствий (утверждений, которые будут следовать из новых фактов на основе посылок) и множество дополнительных фактов, необходимых для успешного вывода следствий. Причем объединенное множество исходных посылок, новых и дополнительных фактов не должно быть противоречивым.

Формальная постановка задачи

Предполагается, что для представления знаний используются логические выражения исчисления предикатов первого порядка. Факты и следствия представляются литералами без инверсий и переменных, а правила базы знаний – дизъюнктами, содержащими два и более литерала, в том числе один литерал без инверсии.

Задачу вывода следствий можно сформулировать следующим образом. Имеются исходные непротиворечивые посылки, заданные в виде множества дизъюнктов M^ = {D1,…,DI}. Множество M^ = MF∪M состоит из подмножества однолитеральных дизъюнктов-фактов MF и подмножества дизъюнктов-правил M. Также имеется множество новых фактов mF = {L1,…,Lp,…, LP}. Требуется определить три семейства множеств: дедуктивных следствий E = {e0,e1,…,eh,…,eH}, абдуктивных следствий E' = {e'1,…,e'h,…,e'H} и дополнительных фактов F = {f1,…,fh,…,fH}. Множество абдуктивных следствий e'h формируется на h-м шаге (h = 1,…H) вывода в тех случаях, когда на этом шаге нет дедуктивных следствий (eh, = ∅).

Множество следствий e0 состоит из фактов исходных посылок, совпадающих с новыми фактами: e0 = MF∩mF.

Множество e1 содержит дедуктивные следствия, выводимые из множества новых фактов mF с помощью множества посылок M1(M1⊆M^):mF, M1⇒e1. Причем если e1 = ∅, то определяется множество дополнительных фактов f1 и множество обеспечиваемых ими абдуктивных следствий: mF,(M1∪f1)⇒e'1.

Множество eh + 1 (h = 1,…,H-1) содержит дедуктивные следствия, выводимые из множества новых фактов mF и ранее полученных дедуктивных sh = sh-1∪eh (s0 = e0) и абдуктивных s'h = s'h-1e'h (s'0 = ∅) следствий с помощью множества посылок Mh + 1 (Mh + 1⊆M^) и множества дополнительных фактов jh = jh-1∪fh: mF,(sh∪s'h),(Mh + 1∪jh)⇒eh + 1. Если eh + 1 = ∅, то определяется множество дополнительных фактов fh + 1 и множество обеспечиваемых ими абдуктивных следствий: mF,(sh∪s'h), (Mh + 1∪jh + 1)⇒e'h + 1, здесь jh + 1 = jh∪fh + 1.

При этом множество M^∪mF?M f – должно быть совместно (M f = f1∪…∪fH).

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

Частичное и полное деление дизъюнктов

Частичное деление дизъюнктов выполняется с помощью специальной процедуры образования остатков, которая является одной из основных процедур, используемых в методе логического вывода следствий в исчислении предикатов. Процедура предполагает, что посылки и заключение представлены в виде дизъюнктов. Для удобства описания процедуры введем ряд обозначений. w = <b, d, q, n, s> – процедура частичного деления, в которой: b – остаток-делимое (дизъюнкт посылки), используемый для получения остатков; d – остаток-делитель (дизъюнкт заключения), участвующий в образовании остатков; s – множество следствий, полученное в процессе выполнения процедуры; q – частный признак продолжения деления дизъюнктов: «0» – дальнейшее деление возможно; «1» – продолжение деления невозможно; n = {<bt, dt>, t = 1,...,T} – множество пар, состоящих из нового остатка-делимого bt и соответствующего ему остатка-делителя dt, сформированных в результате применения процедуры w. Обозначим также через n^ множество новых остатков-делимых: n^ = {bt, t = 1,...,T}.

Полное деление дизъюнктов направлено на получение множества следствий S из множества новых фактов mF и множества u, включающего ранее полученные следствия S ° и дополнительные факты f °, на основании исходного дизъюнкта D. При отсутствии следствий, в процессе полного деления дизъюнктов вычисляется минимальный конечный остаток s. Остаток-делимое b считается конечным остатком, если он содержит меньше литералов, чем исходный дизъюнкт D, и его дальнейшее частичное деление на остаток-делитель невозможно.

Множество следствий S находится путем полного деления дизъюнкта D на дизъюнкт d. Полное деление дизъюнктов осуществляется с помощью процедуры W = <D,d,u,Q,S,s>, в которой Q – признак решения, имеющий два значения: «0» – следствия найдены, «1» – дизъюнкт d не имеет следствий на основании дизъюнкта D.

Формирование множества следствий S производится путем многократного применения w-процедур и состоит из ряда шагов. На каждом шаге w-процедуры применяются к имеющимся остаткам-делимым и остаткам-делителям, образуя новые остатки-делимые и новые остатки-делители, которые используются в качестве исходных данных на следующем шаге. Процесс заканчивается, когда на очередном шаге обнаруживается, что во всех w-процедурах данного шага сформированы признаки, свидетельствующие о невозможности продолжения деления дизъюнктов (q = 1).

Описание действий, составляющих процедуру, представлено в [3]. Следует учесть, что в случае получения на подготовительном шаге признака q = 1 принимается s = 0. Иначе s выбирается на заключительном шаге из остатков, содержащих наименьшее число литералов.

Процедура вывода следствий

Процедура вывода следствий формирует дедуктивные и абдуктивные следствия, а также дополнительные факты, необходимые для вывода абдуктивных следствий, в случаях, когда дедуктивные следствия на текущем шаге получить невозможно. При отсутствии дедуктивных следствий в результате выполнения процедур полного деления дизъюнктов может быть сформировано N ≥ 1 минимальных конечных остатков. Для продолжения логического вывода достаточно n (1 ≤ n ≤ N) абдуктивных следствий и соответствующих им дополнительных фактов. Перед выполнением логического вывода задается максимальное число абдуктивных следствий nmax, которые могут быть использованы на шаге вывода. При этом, чем меньше n, тем меньше логический вывод отличается от дедуктивного. Однако чем больше n, тем больше следствий будет получено в процессе логического вывода.

Процедура вывода следствий имеет следующий вид:

wh = <M, R, o, o', r, p, R1, e, e', f, nmax>,

где M = {D1,D2,…,Di,…,DI} – множество исходных дизъюнктов; Di = Li1∨Li2∨…Lij∨…∨LiJj – i-й дизъюнкт, состоящий из литералов Lij; R = dolg.wmfL1∨dolg.wmfL2∨...∨dolg.wmfLk∨...∨dolg.wmfLK – выводимый дизъюнкт, состоящий из инверсий литералов Lk ранее полученных следствий, а на первом шаге – новых фактов; p – признак продолжения вывода: «0» – дальнейший вывод возможен; «1» – вывод завершен; o = <c, C> – пара множеств текущих дедуктивных следствий, состоящая из множеств следствий, образованных до выполнения (c) и после выполнения (C) процедуры; e – множество дедуктивных следствий для выводимого дизъюнкта (C = c∪e); o' = <c',C'> – пара множеств текущих абдуктивных следствий, состоящая из множеств следствий, образованных до выполнения (c') и после выполнения (C') процедуры; e' – множество абдуктивных следствий для выводимого дизъюнкта (C' = c'∪e'); r = <g,G> – пара множеств дополнительных фактов, состоящая из множеств фактов, образованных до выполнения (g) и после выполнения (G) процедуры; f – множество дополнительных фактов, полученных для выводимого дизъюнкта после выполнения процедуры (G = g∪f); nmax – максимальное число абдуктивных следствий, используемых на шаге вывода.

Процедура вывода использует в качестве субпроцедуры ранее рассмотренную W-процедуру полного деления дизъюнктов.

Процедура вывода применима, если M ≠ ∅ и Ji, K ≥ 1 (i = 1,...,I), иначе сразу устанавливается признак p = 1, e = e' = f = ∅, C = c, C' = c', G = g и производится переход к п. 5. В процедуре выполняются следующие действия.

1. Выполняется полное деление дизъюнктов:

1) дизъюнкты исходных секвенций Di (i = 1,...,I) с помощью W-процедур делятся на выводимый дизъюнкт R: Wi = W = <Di,R,ui,Qi,Si,si>.

2) анализируются результаты выполненных W-процедур.

А) Если есть признаки решений Qi равные нулю, то выполняется п. 2.

Б) если все признаки решений Qi равны единице и есть минимальные конечные остатки si, то принимается e = ∅ и производится переход к п. 3.

В) если все признаки решений Qi равны единице и нет минимальных конечных остатков, то принимается p = 1, e = ∅, e' = ∅, f = ∅ и производится переход к п. 5.

2. Формируется множество дедуктивных следствий для выводимого дизъюнкта. Множество e образуется путем объединения множеств Si дедуктивных следствий, сформированных при выполнении W-процедур, и исключения следствий c∅c', полученных ранее. Если из множества e будут исключены не все литералы, то принимается e' = ∅, f = ∅, p = 0 и производится переход к п. 4, иначе устанавливается e = ∅ и выполняется следующий пункт.

3. Формируется множество абдуктивных следствий и множество дополнительных фактов для выводимого дизъюнкта. Множество e' образуется путем включения в него положительных литералов из N (N ≥ 1) конечных остатков si, полученных при выполнении W-процедур, унифицируемых хотя бы с одним литералом посылок множества M, и исключения следствий cc', полученных ранее. Если из множества e' будут исключены все литералы, то принимается e' = ∅, f = ∅, p = 1 и производится переход к п. 6, иначе устанавливается p = 0, корректируется множество следствий e' и формируется множество дополнительных фактов f.

Коррекция множества e' выполняется путем исключения следствий, в тех случаях, когда число следствий превышает заданную величину nmax. В результате коррекции сохраняется не более n ≤ nmax следствий, соответствующих минимальным конечным остаткам с наименьшим числом литералов.

Элементами множества дополнительных фактов f являются инверсии отрицательных литералов минимальных конечных остатков si, положительные литералы которых остались, как следствия, во множестве e' после исключения литералов и коррекции множества. Выполняется следующий пункт.

4. Формируется новый выводимый дизъюнкт. Выводимый дизъюнкт R1 представляет собой дизъюнкцию инверсий литералов множества следствий e∪e'.

5. Формируются новые пары множеств следствий и дополнительных фактов. В паре множеств текущих дедуктивных следствий o = <c,C> множество C образуется в результате объединения множества следствий с, полученного до выполнения процедуры, и множества следствий e, полученного для выводимого дизъюнкта: С = c∪e. Аналогично в паре множеств текущих абдуктивных следствий o' = <c',C'> формируется новое множество С' = c'∪e', а в паре множеств дополнительных фактов r = <g,G> множество G = g∪f.

6. Фиксируются результаты выполнения процедуры. Если признак p = 1, то дальнейший вывод следствий невозможен, а если p = 0, то вывод может быть продолжен. При непустом множестве следствий e∪e' в процессе выполнения процедуры будет сформирован новый выводимый дизъюнкт R1, а если успешным был абдуктивный вывод, то и множество дополнительных фактов f.

Метод логического вывода следствий

Метод вывода следствий основан на процедуре вывода следствий и состоит из ряда шагов, на каждом из которых выполняется процедура вывода v, причем результаты выполнения процедуры текущего шага становятся исходными данными для процедуры следующего шага. Процесс заканчивается в случае, если дальнейший вывод следствий невозможен (получено значение признака P = 1).

Обозначим через h номер шага вывода, а через P – общий признак продолжения вывода (P = 0 – продолжение вывода возможно, P = 1 – продолжение вывода невозможно). Тогда описание метода может быть представлено в следующем виде.

1. Определение начальных значений: h = 1, M ≠ ∅, mF ≠ ∅, nmax = D. Формирование выводимого дизъюнкта R1, состоящего из литералов Lk, представляющих собой инверсии литералов множества mF. Определение начального множества литералов дедуктивных следствий e0, представляющих собой новые факты mF, совпадающих после применения унифицирующих подстановок с фактами MF, имеющимися в исходных посылках: e0 = MF∩mF, s0 = {e0}, c1 = e0. Определение начального множества абдуктивных следствий: p0 = ∅, c'1 = ∅. j0 = ∅. Установка начального значения общего признака продолжения вывода: P0 = 0.

2. Выполнение h-й процедуры вывода:

wh = <M,Rh,oh,o'h,rh,ph,Rh + 1,eh,e'h,fh,D>.

3. Формирование семейств следствий и дополнительных фактов, проверка признаков. Производится пополнение семейств множеств дедуктивных sh = sh-1∪{eh} и абдуктивных ph = ph-1∪{e'h} следствий, а также семейства дополнительных фактов jh = jh-1∪{fh}. Формируется общий признак продолжения вывода Ph = Ph-1∪ph. Если Ph = 0, то принимается сh + 1 = Ch, с'h + 1 = C'h и вывод продолжается. Производится увеличение h на единицу и переход к п. 2, иначе вывод завершается (h = H). Полученные дедуктивные следствия содержатся в семействе множеств sH, а абдуктивные – в семействе множеств pH. Общее множество следствий MS получается путем объединения множеств семейств sH и pH.

Применение метода вывода следствий рассмотрим на примере о родственных связях, представленном в работе [6]. Исходными данными являются следующие предложения.

Отец (F) – это персона (Per) мужского пола, являющаяся родителем (P). Дед (GF) – это отец родителя. Родные братья или сестры (S) – это две различных (N) персоны, которые имеют общего родителя. Тетя (A) – это персона, которая является родной сестрой родителя. Известно, что Владимир (с) является родителем Натальи (d), и Виктория (b) – женщина (f). Новыми фактами является то, что Владимир – ребенок Дмитрия (a), и Владимир и Виктория – разные люди.

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

1) F(x, y) ∨dolg.wmfPer(x, m) ∨dolg.wmfP(x, y);

2) GF(x, y) ∨dolg.wmfF(x, z) ∨dolg.wmfP(z, y);

3) S(x ,y) ∨dolg.wmfP(z, x) ∨dolg.wmfP(z, y) ∨dolg.wmfN(x, y);

4) A(x, y) ∨dolg.wmfPer(x, f) ∨dolg.wmfP(z, y) ∨dolg.wmfS(x, z);

5) P(c, d);

6) Per(b, f);

Новые факты: P(a, c), N(b, c).

Логический вывод будет состоять из следующих шагов.

Определение начальных значений: h = 1, M = {D1, D2, D3, D4}, mF = {P(a, c), N(b, c)}, nmax = 3. Формирование выводимого дизъюнкта R1 = dolg.wmfP(a, c)dolg.wmfN(b, c), состоящего из литералов, представляющих собой инверсии литералов множества mF. Определение множества следствий e0, совпадающих с фактами MF, имеющимися в исходных посылках: e0 = MF∩mF = ∅, s0 = {e0}, c1 = e0 = ∅. Определение начального множества абдуктивных следствий: p0 = ∅, c'1 = ∅. j0 = ∅. Установка начального значения общего признака продолжения вывода: P0 = 0.

Результаты выполнения процедур вывода представлены в таблице. Полное описание выполняемых действий содержится в работе [7].

Результаты выполнения процедур вывода

Делимое

Признак решения

Минимальный конечный остаток

Признак продолжения вывода

Множество следствий

Семейства множеств следствий

Общий признак продолжения вывода

Процедура вывода w1 (R1 = dolg.wmfP(a, c)∨dolg.wmfN(b, c))

D1

Q1 = 1

s1 = F(a, c)∨dolg.wmfPer(а, m)

p1 = 0

e'1 = {F(a, c)}

f1 = {Per(а, m)}

s1 = ∅

p1 = {F(a, c), S(b, c)},

j1 = {Per(а, m), P(а, b)}

P1 = 0

D2

Q2 = 1

   

D3

Q3 = 1

s3 = S(b, c)dolg.wmfP(a, b)

e'3 = {S(b, c)}

f3 = {P(а, b)}

D4

Q1 = 1

s4 = A(b, c)dolg.wmfS(b, a)

 

Процедура вывода w2 (R2 = dolg.wmfF(a, c)dolg.wmfS(b, c))

D2

Q2 = 0

 

p2 = 0

s2 = {GF(a, d)}

s2 = {GF(a, d), A(b, d)}

p2 = {F(a, c), S(b, c)},

j2 = {Per(а, m), P(а,b)}

P2 = 0

D4

Q4 = 0

s4 = {A(b, d)}

Процедура вывода w 3 (R3 = dolg.wmfGF(a, d)∨dolg.wmfA(b, d))

Ни одно из правил не делится на выводимый дизъюнкт

p3 = 0

 

s3 = {GF(a, d), A(b, d)}

p3 = {F(a, c), S(b, c)},

j3 = {Per(а, m), P(а, b)}

P3 = 1

Общее множество следствий получается путем объединения множеств семейства s3 и p3: MS = {F(a,c), S(b,c), GF(a,d), A(b,d)}.

Таким образом, в процессе вывода следствий было установлено, что если Дмитрий – мужчина (Per(a,m)) и он является родителем Виктории (P(a,b)), то Дмитрий является отцом Владимира (F(a,c)), Владимир и Виктория – единокровные брат и сестра (S(b,c)), у Дмитрия есть внучка Наталья (GF(a,d)), а у Натальи – тетя Виктория (A(b,d)).

Заключение

Предложенный метод логического вывода позволяет находить следствия в ситуациях, когда база знаний, представленная формулами исчисления предикатов первого порядка, не полностью определена. При этом осуществляется построение множества дополнительных фактов, наличие которых обеспечивает получение абдуктивных следствий, формирование которых происходит только в том случае, если дедуктивный вывод на очередном шаге завершается безрезультативно. Особенности метода обусловлены его первоначальной ориентацией на задачи логического прогнозирования развития ситуаций [4].

Метод обладает многоуровневым параллелизмом (параллельная унификация пар литералов, одновременное и независимое формирование остатков и единовременное деление дизъюнктов базы знаний на выводимый дизъюнкт), что позволяет эффективно применять его при реализации интеллектуальных систем на современных высокопроизводительных параллельных вычислительных платформах [2, 8].

Работа выполнена при финансовой поддержке РФФИ (проект № 15-01-02818a).