Научный журнал
Современные наукоемкие технологии
ISSN 1812-7320
"Перечень" ВАК
ИФ РИНЦ = 1,021

ВЫВОД СЛЕДСТВИЙ В ИСЧИСЛЕНИИ ПРЕДИКАТОВ С ПОСТРОЕНИЕМ СХЕМЫ ВЫВОДА

Долженкова М.Л. 1 Страбыкин Д.А. 1 Чистяков Г.А. 1 Мельцов В.Ю. 1
1 ФГБОУ ВО «Вятский государственный университет»
В настоящей статье предлагается формальная постановка задачи логического вывода следствий с построением схемы. Кроме того, в работе также рассматривается метод решения данной задачи, базирующийся на операциях полного и частичного деления дизъюнктов. Процесс применения метода иллюстрируется на классическом примере о родственных связях (вариация в исчислении предикатов первого порядка). Предложенный метод обладает высокой степенью параллелизма (преимущественно AND- и ОR-уровней), что позволяет использовать его в качестве математической основы для построения специализированных интеллектуальных систем, прежде всего – систем логического прогнозирования развития ситуаций. Получаемая при этом в ходе процесса вывода схема может быть полезна как инструмент анализа и исследования сформированного прогноза. Кроме того, схема может применяться в составе модуля абдукции для выявления скрытых фактов, способных скорректировать состояние объекта наблюдения и минимизировать вероятность нежелательного прогноза. Еще одной потенциально возможной областью применения предлагаемого метода является оптимизация ресурсных затрат при решении задач чрезвычайно большой размерности путем сокращения мощности пространства состояний предметной области за счет замены статической составляющей системы динамической.
вывод следствий
база знаний
поступление новых фактов
исчисление предикатов
дедуктивный вывод
деление дизъюнктов
1. Финн В.К. Автоматическое порождение гипотез в интеллектуальных системах / В.К. Финн, Е.С. Панкратова. – М.: Либроком, 2009. – 528 с.
2. Рассел С. Искусственный интеллект. Современный подход / С. Рассел, П. Новриг. – М.: Вильямс, 2015. – 1408 с.
3. Huth M. Logic in Computer Science. Modelling and Reasoning about Systems / M. Huth, M. Ryan. – Cambridge: Cambridge University Press, 2004. – 440 p.
4. Страбыкин Д.А. Логическое прогнозирование развития ситуаций на основе дедуктивного вывода / Д.А. Страбыкин, М.Н. Томчук // Научно-технический вестник Поволжья. – 2012. – № 2. – С. 276–282.
5. Страбыкин Д.А. Метод логического прогнозирования развития ситуаций на основе абдуктивного вывода // Изв. РАН. ТиСУ. – 2013. – № 5. – С. 98–92.
6. Долженкова М.Л. Метод вывода следствий из новых фактов делением дизъюнктов в исчислении предикатов / М.Л. Долженкова, В.Ю. Мельцов, Д.А. Страбыкин, Г.А. Чистяков // Современные наукоемкие технологии. – 2016. – № 9–1. – С. 28–35.
7. Чери С. Логическое программирование и базы данных / С. Чери, Г. Готлоб, Л. Танка. – М.: Мир, 1992. – 352 с.
8. Caferra R. Logic for computer science and artificial intelligence / R. Caferra. – London: ISTE, 2011. – 544 p.
9. Mordechai B.-A. Mathematical Logic for Computer Science / B.-A. Mordechai. – London: Springer-Verlag, 2012. – 354 p.
10. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем / Ю.Г. Карпов. – СПб.: БХВ-Петербург, 2009. – 552 с.

Для эффективного решения задач в различных прикладных областях в настоящее время все чаще применяются системы искусственного интеллекта. Задавать всевозможные отношения и причинно-следственные связи между объектами лучше всего с использованием исчисления предикатов первого порядка. В подавляющем большинстве современных интеллектуальных систем для моделирования рассуждений применяется аппарат логического вывода [1, 2] – дедуктивного, индуктивного, абдуктивного, нечеткого методов рассуждений на основе аналогий и прецедентов [3]. Однако нередко в ходе моделирования сложного, многоступенчатого рассуждения требуется определить следствия, которые могут быть выведены из новых фактов, отражающих обстоятельства изменившейся внешней (окружающей) среды при заданном наборе исходных посылок [4]. Для решения поставленной задачи используется специализированный вид дедуктивного вывода – параллельный вывод логических следствий [5].

Формальная постановка задачи логического вывода следствий представлена в работе [6]. Дополнительный интерес может представлять схема, полученная в ходе вывода, которая отражает информацию обо всех возможных траекториях изменения состояния исследуемой системы в прошлом, настоящем и будущем, поэтому в ходе вывода формируется описание O схемы логического вывода в виде семейства множеств O = {f1,f2,…,fh,…,fH-1}∪{s+}, где fh – множество литералов, полученных при формировании описания схемы на h-м шаге вывода, s+ – множество конечных следствий, из которых не могут быть выведены новые следствия (s+⊆MS).

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

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

1. Персона (Per) мужского пола, являющаяся родителем (P), называется отцом (F).

2. Отец одного из родителей является дедушкой (GF).

3. Две различные (N) персоны с общим родителем находятся в отношении родных братьев или сестер (S).

4. Родная сестра родителя является тетей (A).

Имеются следующие факты: Виктор (с) – отец Ольги (d), Антонина (b) – персона женского пола (f). Новые факты: Виктор – сын Семена (a), Виктор и Антонина – это не один и тот же человек.

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

1) F(x,y)[1,+] ∨ Per(x,m)[+,1] ∨ P(x,y)[+,1];

2) GF(x,y)[2,+] ∨ F(x,z)[+,2] ∨ P(z,y)[+,2];

3) S(x,y)[3,+] ∨ P(z,x)[+,3] ∨ P(z,y)[+,3] ∨ N(x,y)[+,3];

4) A(x,y)[4,+] ∨ Per(x,f)[+,4] ∨ P(z,y)[+,4] ∨ S(x,z)[+,4];

5) P(a,b)[5,+];

6) P(c,d)[6,+];

7) Per(a,m)[7,+];

8) Per(b,f)[8,+];

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

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

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

2.1. Выполнение 1-й процедуры вывода. v1 = <M,R1,∅,o1,p1,R2,e1,f1>.

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

Дизъюнкты D1, D2, D3 и D4 делятся на выводимый дизъюнкт R1.

1. Дизъюнкт D1 с помощью W-процедуры делится на выводимый дизъюнкт R1: D1WR1 = (F(x,y)[1,+] ∨ Per(x,m)[+,1] ∨ P(x,y)[+,1])W(P(a,c)[9,+] ∨ N(b,c)[9,+]). Вычисляется матрица «производных» μ[D1,R1] подготовительного шага полного деления дизъюнктов.

 

F(x,y)[1,+]

Per(x,m)[+,1]

P(x,y)[+,1]

P(a,c)[9,+]

1

1

Δ13

N(b,c)[9,+]

1

1

1

В матрице l13 = {a/x,c/y}, D13 = F(a,c)[1,+] ∨ Per(a,m)[+,1] = b1, поэтому принимается q = 0, и определяется множество n = {<b1,d1,g1>} (g1 = {P(a,c)[9,{a/x,c/y}1]}). Возможно продолжение частичного деления дизъюнктов. Остаток-делитель d1* = 0, а d1 = P(a,b)[5,+] ∨ P(c,d)[6,+] ∨ Per(a,m)[7,+] ∨ Per(b,f)[8,+].

Дизъюнкт b1 = F(a,c) ∨ dol.wmfPer(a,m) с помощью w-процедуры делится на выводимый дизъюнкт d1. Вычисляется матрица «производных» μ[b1,d1] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

F(a,c)[1,+]

Per(a,m)[+,1]

P(a,b)[5,+]

1

1

P(c,d)[6,+]

1

1

Per(a,m)[7,+]

1

Δ32

Per(b,f)[8,+]

1

1

В матрице D32 = F(a,c)[1,+] = b1.1, однако остаток-делитель d1.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S1 = {F(a,c)[{a/x,c/y}1,+]} и семейство множеств литералов описания схемы G1 = {{P(a,c)[9,{a/x,c/y}1], Per(a,m)[7,1]}}, Q1 = 0.

2. Дизъюнкт D2 с помощью W-процедуры делится на выводимый дизъюнкт R1: D2WR1 = (GF(x,y)[2,+] ∨ F(x,z)[+,2] ∨ P(z,y)[+,2])W(P(a,c)[9,+] ∨ N(b,c)[9,+]). Вычисляется матрица «производных» μ[D2,R1] подготовительного шага полного деления дизъюнктов.

 

GF(x,y)[2,+]

F(x,z)[+,2]

P(z,y)[+,2]

P(a,c)[9,+]

1

1

Δ13

N(b,c)[9,+]

1

1

1

В матрице l13 = {a/z,c/y}, D13 = GF(x,c)[2,+] ∨ F(x,a)[+,2] = b1, поэтому принимается q = 0, и определяется множество n = {<b1,d1,g1>} (g1 = {P(a,c)[9,{a/z,c/y}2]}). Возможно продолжение частичного деления дизъюнктов. Остаток-делитель d1* = 0, а d1 = P(a,b)[5,+] ∨ P(c,d)[6,+] ∨ Per(a,m)[7,+] ∨ Per(b,f)[8,+].

Дизъюнкт b1 = GF(x,c) ∨ dol.wmfF(x,a) с помощью w-процедуры делится на выводимый дизъюнкт d1. Вычисляется матрица «производных» μ[b1,d1] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

GF(x,c)[2,+]

F(x,a)[+,2]

P(a,b)[5,+]

1

1

P(c,d)[6,+]

1

1

Per(a,m)[7,+]

1

1

Per(b,f)[8,+]

1

1

В матрице все производные равны единице, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов следствий нет: S2 = ∅, G2 = ∅, Q2 = 1.

3. Дизъюнкт D3 с помощью W-процедуры делится на выводимый дизъюнкт R1: D3WR1 = (S(x,y)[3,+] ∨ P(z,x)[+,3] ∨ P(z,y)[+,3] ∨ N(x,y)[+,3])W(P(a,c)[9,+] W N(b,c)[9,+]). Вычисляется матрица «производных» μ[D3,R1] подготовительного шага полного деления дизъюнктов.

 

S(x,y)[3,+]

P(z,x)[+,3]

P(z,y)[+,3]

N(x,y)[+,3]

P(a,c)[9,+]

1

Δ12

Δ13

1

N(b,c)[9,+]

1

1

1

Δ24

В матрице l12 = {a/z,c/x}, D12 = S(c,y)[3,+] ∨ P(a,y)[+,3] ∨ N(c,y)[+,3] = b1, l13 = {a/z,c/y}, D13 = S(x,c)[3,+] ∨ P(a,x)[+,3] ∨ N(x,c)[+,3] = b2, l24 = {b/x,c/y}, D24 = S(b,c)[3,+] ∨ P(z,b)[+,3] ∨ P(z,c)[+,3] = b3, поэтому принимается q = 0, и определяется множество n = {<b1,d1,g1>, <b2,d2,g2>, <b3,d3,g3>} (g1 = {P(a,c)[9,{a/z,c/x}3]}, g2 = {P(a,c)[9,{a/z,c/y}3]}, g3 = {N(b,c)[9,{b/x,c/y}3]}). Возможно продолжение частичного деления дизъюнктов, d1 = d2 = P(a,b)[5,+] ∨ P(c,d)[6,+] ∨ Per(a,m)[7,+] ∨ Per(b,f)[8,+] ∨ P(a,c)[9,+] ∨ N(b,c)[9,+], d3 = P(a,b)[5,+] ∨ P(c,d)[6,+] ∨ Per(a,m)[7,+] ∨ Per(b,f)[8,+] ∨ P(a,c)[9,+].

Вычисляется матрица «производных» μ[b1,d1] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

S(c,y)[3,+]

P(a,y)[+,3]

N(c,y)[+,3]

P(a,b)[5,+]

1

Δ12

1

P(c,d)[6,+]

1

1

1

Per(a,m)[7,+]

1

1

1

Per(b,f)[8,+]

1

1

1

P(a,c)[9,+]

1

Δ52

1

N(b,c)[9,+]

1

1

1

В матрице l12 = {c/y}, D12 = S(c,c)[3,+] ∨ N(c,c)[+,3], l52 = {b/y}, D52 = S(c,b)[3,+] ∨ N(c,b), q = 1. Дальнейшее частичное деление дизъюнктов невозможно.

Вычисляется матрица «производных» μ[b2,d2] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

S(x,c)[3,+]

P(a,x)[+,3]

N(x,c)[+,3]

P(a,b)[5,+]

1

Δ12

1

P(c,d)[6,+]

1

1

1

Per(a,m)[7,+]

1

1

1

Per(b,f)[8,+]

1

1

1

P(a,c)[9,+]

1

Δ52

1

N(b,c)[9,+]

1

1

Δ63

В матрице l12 = {b/x}, D12 = S(b,c)[3,+] ∨ N(b,c)[+,3] = b2.1, l52 = {c/x}, D52 = S(c,c)[3,+] ∨ N(c,c)[+,3] = b2.2, l63 = {b/x}, D63 = S(b,c)[3,+] ∨ P(a,b)[+,3] = b2.3, поэтому принимается q = 0, и определяется множество n = {<b2.1,d2.1,g2.1>, <b2.2,d2.2,g2.2>, <b2.3,d2.3,g2.3>} (g2.1 = {P(a,c)[9,{a/z,c/y}3], P(a,b)[5,{b/x}3]}, g2.2 = {P(a,c)[9,{a/z,c/y}3], P(a,c)[9,{c/x}3]}, g2.3 = {P(a,c)[9,{a/z,c/y}3], N(b,c)[9,{b/x}3]}). Возможно продолжение частичного деления дизъюнктов, d2.1 = N(b,c)[9,+], d2.2 = N(b,c)[9,+], d2.3 = P(a,b)[5,+] ∨ P(a,c)[9,+].

Вычисляется матрица «производных» μ[b2.1,d2.1] второго выполнения основного шага процедуры полного деления дизъюнктов.

 

S(b,c)[3,+]

N(b,c)[+,3]

N(b,c)[9,+]

1

Δ12

В матрице D12 = S(b,c)[3,+] = b2.1.1, однако остаток-делитель d2.1.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S3 и семейство множеств литералов описания схемы G3, Q3 = 0.

Вычисляется матрица «производных» μ[b2.2,d2.2] второго выполнения основного шага процедуры полного деления дизъюнктов.

 

S(c,c)[3,+]

N(c,c)[+,3]

N(b,c)[9,+]

1

1

В матрице все производные равны единице, поэтому принимается q = 1.

Вычисляется матрица «производных» μ[b2.3,d2.3] второго выполнения основного шага процедуры полного деления дизъюнктов.

 

S(b,c)[3,+]

P(a,b)[+,3]

P(a,b)[5,+]

1

Δ12

P(a,c)[9,+]

1

1

В матрице D12 = S(b,c)[3,+] = b2.3.1, однако остаток-делитель d2.2.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S3 и семейство множеств литералов описания схемы G3, Q3 = 0.

Вычисляется матрица «производных» μ[b3,d3] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

S(b,c)[3,+]

P(z,b)[+,3]

P(z,c)[+,3]

P(a,b)[5,+]

1

Δ12

1

P(c,d)[6,+]

1

1

1

Per(a,m)[7,+]

1

1

1

Per(b,f)[8,+]

1

1

1

P(a,c)[9,+]

1

1

D53

В матрице l12 = {a/z}, D12 = S(b,c)[3,+] ∨ P(a,c)[+,3], l53 = {a/z}, D53 = S(b,c)[3,+] ∨ P(a,b)[+,3], поэтому принимается q = 0, и определяется множество n = {<b3.1,d3.1,g3.1>, <b3.2,d3.2, g3.2>} (g3.1 = {N(b,c)[9,{b/x,c/y}3], P(a,b)[5,{a/z}3]}, g3.2 = {N(b,c)[9,{b/x,c/y}3], P(a,c)[9,{a/z}3]}). Возможно продолжение частичного деления дизъюнктов, d3.1 = P(a,c)[9,+], d3.2 = P(a,b)[5,+].

Вычисляется матрица «производных» μ[b3.1,d3.1] второго выполнения основного шага процедуры полного деления дизъюнктов.

 

S(b,c)[3,+]

P(a,c)[+,3]

P(a,c)[9,+]

1

Δ12

В матрице D12 = S(b,c)[3,+] = b3.1.1, однако остаток-делитель d3.1.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S3 и семейство множеств литералов описания схемы G3, Q3 = 0.

Вычисляется матрица «производных» Δ[b3.2,d3.2] второго выполнения основного шага процедуры полного деления дизъюнктов.

 

S(b,c)[3,+]

P(a,b)[+,3]

P(a,b)[5,+]

1

Δ12

В матрице D12 = S(b,c)[3,+] = b3.2.1, однако остаток-делитель d3.2.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S3 = {S(b,c)[{a/z,b/x,c/y}3,+]} и семейство множеств литералов описания схемы G3 = {{N(b,c)[9,{b/x,c/y}3], P(a,c)[9,{a/z}3], P(a,b)[5,3]}}, Q3 = 0.

4. Дизъюнкт D4 с помощью W-процедуры делится на выводимый дизъюнкт R1: D4WR1 = (A(x,y)[4,+] ∨ Per(x,f)[+,4] ∨ P(z,y)[+,4] ∨ S(x,z)[+,4])W(P(a,c)[9,+] ∨ N(b,c)[9,+]). Вычисляется матрица «производных» μ[D4,R1] подготовительного шага полного деления дизъюнктов.

 

A(x,y)[4,+]

Per(x,f)[+,4]

P(z,y)[+,4]

S(x,z)[+,4]

P(a,c)[9,+]

1

1

Δ13

1

N(b,c)[9,+]

1

1

1

1

В матрице l13 = {a/z,c/y}, D13 = A(x,c)[4,+] ∨ Per(x,f)[+,4] ∨ S(x,a)[+,4] = b1, поэтому принимается q = 0, и определяется множество n = {<b1,d1,g1>}. Возможно продолжение частичного деления дизъюнктов. Остаток-делитель d1* = 0, а d1 = P(a,b)[5,+] ∨ P(c,d)[6,+] ∨ Per(a,m)[7,+] ∨ Per(b,f)[8,+].

Вычисляется матрица «производных» μ[b1,d1] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

A(x,c)[4,+]

Per(x,f)[+,4]

S(x,a)[+,4]

P(a,b)[5,+]

1

1

1

P(c,d)[6,+]

1

1

1

Per(a,m)[7,+]

1

1

1

Per(b,f)[8,+]

1

Δ42

1

В матрице l42 = {b/x}, D42 = A(b,c)[4,+] ∨ S(b,a)[+,4] = b1.1, однако остаток-делитель d1.1 = 0, поэтому принимается q = 1.

Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов следствий нет: S4 = ∅, Q4 = 1.

Анализируются признаки решений Q1, Q2, Q3, Q4 выполненных W-процедур. Поскольку Q1 = 0, Q3 = 0, то принимается p1 = 0 и выполняется следующее действие.

2.1.2. Формируется множество следствий и множество литералов описания схемы для выводимого дизъюнкта. Множество e1 образуется путем объединения множеств следствий, полученных при выполнении W-процедур: e1 = S1∪S3 = {F(a,c)[{a/x,c/y}1,+], S(b,c)[{a/z,b/x,c/y}3,+]}. Множество f1 образуется путем включения в него литералов из элементов множеств G1 и G3, соответствующих элементам множества e1, f1 = {P(a,c)[9,{a/x,c/y}1], Per(a,m)[7,1], N(b,c)[9,{b/x, c/y}3], P(a,c)[9,{a/z}3], P(a,b)[5,3]}.

2.1.3. Формируется новый выводимый дизъюнкт. Выводимый дизъюнкт R2 представляет собой дизъюнкцию литералов множества следствий e1: R2 = F(a,c)[{a/x,c/y}1,+] ∨ S(b,c)[{a/z,b/x,c/y}3,+].

2.1.4. Формируется новое множество следствий: С1 = c1∪e1 = {F(a,c)[{a/x,c/y}1,+], S(b,c)[{a/z,b/x,c/y}3,+]}.

2.1.5. Фиксируются результаты выполнения процедуры. Поскольку p1 = 0, то вывод может быть продолжен для дизъюнкта R2 = F(a,c)[{a/x,c/y}1,+] ∨ S(b,c)[{a/z,b/x,c/y}3,+].

Формирование семейства следствий и проверка признаков. Производится формирование семейства множеств следствий s1 = s0∪{e1} = {{F(a,c)[{a/x,c/y}1,+], S(b,c)[{a/z,b/x,c/y}3,+]}} и семейства множеств литералов описания схемы вывода O = O∪{f1} = {{P(a,c)[9,{a/x,c/y}1], Per(a,m)[7,1], N(b,c)[9,{b/x, c/y}3], P(a,c)[9,{a/z}3], P(a,b)[5,3]}}. Формирование общего признака продолжения вывода P1 = P0∪p1 = 0. Поскольку P1 = 0, то принимается h = 2, с2 = С1 и производится переход к п. 2.2

2.2. Выполнение 2-й процедуры вывода. v2 = <M,R2,mF,o2,p2,R3,e2,f2>.

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

Дизъюнкты D2 и D4 делятся на выводимый дизъюнкт R2.

1. Дизъюнкт D2 с помощью W-процедуры делится на выводимый дизъюнкт R2: D3WR2 = (GF(x,y)[2,+] ∨ F(x,z)[+,2] ∨ P(z,y)[+,2])W(F(a,c)[{a/x,c/y}1,+] ∨S(b,c)[{a/z,b/x,c/y}3,+]). Вычисляется матрица «производных» μ[D2,R2] подготовительного шага полного деления дизъюнктов.

 

GF(x,y)[2,+]

F(x,z)[+,2]

P(z,y)[+,2]

F(a,c)[{a/x,c/y}1,+]

1

Δ12

1

S(b,c)[{a/z,b/x,c/y}3,+]

1

1

1

В матрице l12 = {a/x,c/z}, D12 = GF(a,y)[2,+] ∨ P(c,y)[+,2] = b1, поэтому принимается q = 0, и определяется множество n = {<b1,d1,g1>} (g1 = {F(a,c)[{a/x,c/y}1,{a/x,c/z}2]}). Возможно продолжение частичного деления дизъюнктов. Остаток-делитель d1* = 0, а d1 = P(a,b)[5,+] ∨ P(c,d)[6,+] ∨ Per(a,m)[7,+] ∨ Per(b,f)[8,+] ∨ P(a,c)[9,+] ∨ N(b,c)[9,+].

Вычисляется матрица «производных» μ[b1,d1] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

GF(a,y)[2,+]

P(c,y)[+,2]

P(a,b)[5,+]

1

1

P(c,d)[6,+]

1

Δ22

Per(a,m)[7,+]

1

1

Per(b,f)[8,+]

1

1

P(a,c)[9,+]

1

1

N(b,c)[9,+]

1

1

В матрице l22 = {d/y}, D22 = GF(a,d)[2,+] = b1.1, однако остаток-делитель d1.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S2 = {GF(a,d)[{a/x,c/z,d/y}2,+]} и семейство множеств литералов описания схемы G3 = {{F(a,c)[{a/x,c/y}1,{a/x,c/z}2], P(c,d)[6,{d/y}2]}}, Q3 = 0.

2. Дизъюнкт D4 с помощью W-процедуры делится на выводимый дизъюнкт R2: D4WR2 = (A(x,y)[4,+] ∨ Per(x,f)[+,4] ∨ P(z,y)[+,4] ∨ S(x,z)[+,4])W(F(a,c)[{a/x,c/y}1,+] ∨ S(b,c)[{a/z,b/x,c/y}3,+]).Вычисляется матрица «производных» μ[D4,R2] подготовительного шага полного деления дизъюнктов.

 

A(x,y)[4,+]

Per(x,f)[+,4]

P(z,y)[+,4]

S(x,z)[+,4]

F(a,c)[{a/x,c/y}1,+]

1

1

1

1

S(b,c)[{a/z,b/x,c/y}3,+]

1

1

1

Δ24

В матрице l24 = {b/x,c/z}, D42 = A(b,y)[4,+] ∨ Per(b,f)[+,4] ∨ P(c,y)[+,4] = b1, поэтому принимается q = 0, и определяется множество n = {<b1,d1,g1>} (g1 = {S(b,c)[{a/z,b/x,c/y}3,{b/x,c/z}4]}). Возможно продолжение частичного деления дизъюнктов. Остаток-делитель d1* = 0, а d1 = P(a,b)[5,+] ∨ P(c,d)[6,+] ∨ Per(a,m)[7,+] ∨ Per(b,f)[8,+] ∨ P(a,c)[9,+] ∨ N(b,c)[9,+].

Вычисляется матрица «производных» μ[b1,d1] первого выполнения основного шага процедуры полного деления дизъюнктов.

 

A(b,y)[4,+]

Per(b,f)[+,4]

P(c,y)[+,4]

P(a,b)[5,+]

1

1

1

P(c,d)[6,+]

1

1

Δ23

Per(a,m)[7,+]

1

1

1

Per(b,f)[8,+]

1

Δ42

1

P(a,c)[9,+]

1

1

1

N(b,c)[9,+]

1

1

1

В матрице l23 = {d/y}, D23 = A(b,d)[4,+] ∨ Per(b,f)[+,4] = b1.1, D42 = A(b,y)[4,+] ∨ Per(b,f)[+,4] = b1.2, поэтому принимается q = 0, и определяется множество n = {<b1.1,d1.1,g1.1>, <b1.2,d1.2,g1.2>} (g1.1 = {S(b,c)[{a/z,b/x,c/y}3,{b/x,c/z}4], P(c,d)[6,{d/y}4]}, g1.2 = {S(b,c)[{a/z,b/x,c/y}3,{b/x,c/z}4], Per(b,f)[8,4]}). Возможно продолжение частичного деления дизъюнктов, d1.1 = Per(b,f)[8,+], d1.2 = P(c,d)[6,+].

Вычисляется матрица «производных» μ[b1.1,d1.1] второго выполнения основного шага процедуры полного деления дизъюнктов.

 

A(b,d)[4,+]

Per(b,f)[+,4]

Per(b,f)[8,+]

1

Δ12

В матрице D12 = A(b,d)[4,+] = b1.1.1, однако остаток-делитель d1.1.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S4, и семейство множеств литералов описания схемы G4, Q4 = 0.

Вычисляется матрица «производных» μ[b1.2,d1.2] второго выполнения основного шага процедуры полного деления дизъюнктов.

 

A(b,d)[4,+]

Per(b,f)[+,4]

P(c,d)[6,+]

1

Δ12

В матрице l12 = {d/y}, D12 = A(b,d)[4,+] = b1.2.1, однако остаток-делитель d1.2.1 = 0, поэтому принимается q = 1. Дальнейшее частичное деление дизъюнктов невозможно. В процессе полного деления дизъюнктов получено множество следствий S4 = {A(b,d)[{b/x,c/z,d/y}4,+]}, и семейство множеств литералов описания схемы G4 = {{S(b,c)[{a/z,b/x,c/y}3,{b/x,c/z}4], P(c,d)[6,{d/y}4], Per(b,f)[8,4]}}, Q4 = 0.

Анализируются признаки решений Q2 и Q4 выполненных W-процедур. Поскольку Q2 = 0, Q4 = 0, то принимается p2 = 0 и выполняется следующее действие.

2.2.2. Формируется множество следствий и множество литералов описания схемы для выводимого дизъюнкта. Множество e2 образуется путем объединения множеств следствий, полученных при выполнении W-процедур: e2 = S2∪S4 = {GF(a,d)[{a/x,c/z,d/y}2,+], A(b,d)[{b/x,c/z,d/y}4,+]}. Множество f2 образуется путем включения в него литералов из элементов множеств G2 и G4, соответствующих элементам множества e2, f2 = {F(a,c)[{a/x,c/y}1,{a/x,c/z}2], P(c,d)[6,{d/y}2], S(b,c)[{a/z,b/x,c/y}3,{b/x,c/z}4], P(c,d)[6,{d/y}4], Per(b,f)[8,4]}.

2.2.3. Формируется новый выводимый дизъюнкт. Выводимый дизъюнкт R3 представляет собой дизъюнкцию инверсий литералов множества следствий e2: R3 = GF(a,d)[{a/x,c/z,d/y}2,+] ∨ A(b,d)[{b/x, c/z, d/y}4,+].

2.2.4. Формируется новое множество следствий: С2 = c2∪e2 = {F(a,c)[{a/x,c/y}1,+], S(b,c)[{a/z,b/x,c/y}3,+], GF(a,d)[{a/x,c/z,d/y}2,+], A(b,d)[{b/x, c/z, d/y}4,+]}.

2.2.5. Фиксируются результаты выполнения процедуры. Поскольку p2 = 0, то вывод может быть продолжен для дизъюнкта R3 = GF(a,d)[{a/x,c/z,d/y}2,+] ∨ A(b,d)[{b/x, c/z, d/y}4,+].

Формирование семейства следствий и проверка признаков. Производится формирование семейства множеств следствий s2 = s1∨{e2} = {{F(a,c)[{a/x,c/y}1,+], S(b,c)[{a/z,b/x,c/y}3,+]}, {GF(a,d)[{a/x,c/z,d/y}2,+], A(b,d)[{b/x, c/z, d/y}4,+]}} и семейства множеств литералов описания схемы вывода O = O∨{f2} = {{P(a,c)[9,{a/x,c/y}1], Per(a,m)[7,1], N(b,c)[9,{b/x,c/y}3], P(a,c)[9,{a/z}3], P(a,b)[5,3]}, {F(a,c)[{a/x,c/y}1,{a/x,c/z}2], P(c,d)[6,{d/y}2], S(b,c)[{a/z,b/x, c/y}3,{b/x,c/z}4], P(c,d)[6,{d/y}4], Per(b,f)[8,4]}}. Формирование общего признака продолжения вывода P2 = P1∨p2 = 0. Поскольку P2 = 0, то принимается h = 3, с3 = С2 и производится переход к п. 2.3.

2.3. Выполнение 3-й процедуры вывода. v3 = <M,R3,mF,o3,p3,R4,e3,f3>.

Ни одно из правил, содержащихся в базе знаний, не делится на выводимый дизъюнкт.

Принимается e3 = ∅, f3 = ∅, C3 = c3, p3 = 1.

2.3.1. Фиксируются результаты выполнения процедуры. Поскольку p3 = 1, то вывод не может быть продолжен.

3. Формирование семейства следствий и проверка признаков. Производится формирование семейства множеств следствий s3 = s2∪{e3} = {{F(a,c)[{a/x,c/y}1,+], S(b,c)[{a/z,b/x,c/y}3,+]}, {GF(a,d)[{a/x,c/z,d/y}2,+], A(b,d)[{b/x, c/z, d/y}4,+]}} и семейства множеств литералов описания схемы вывода O = O∪{f3} = {{P(a,c)[9,{a/x,c/y}1], Per(a,m)[7,1], N(b,c)[9,{b/x,c/y}3], P(a,c)[9,{a/z}3], P(a,b)[5,3]}, {F(a,c)[{a/x,c/y}1,{a/x,c/z}2], P(c,d)[6,{d/y}2], S(b,c)[{a/z,b/x,c/y}3,{b/x,c/z}4], P(c,d)[6,{d/y}4], Per(b,f)[8,4]}}. Формирование общего признака продолжения вывода P3 = P2∪p3 = 1. Поскольку P3 = 1, то вывод завершается. Полученные следствия содержатся в семействе множеств s3, а общее множество следствий получается путем объединения множеств семейства s3: MS = {F(a,c)[{a/x,c/y}1,+], S(b,c)[{a/z,b/x,c/y}3,+], GF(a,d)[{a/x,c/z,d/y}2,+], A(b,d)[{b/x, c/z, d/y}4,+]}. Конечное описание схемы вывода следствий формируется как O = {{P(a,c)[9,{a/x,c/y}1], Per(a,m)[7,1], N(b,c)[9,{b/x,c/y}3], P(a,c)[9,{a/z}3], P(a,b)[5,3]}, {F(a,c)[{a/x,c/y}1,{a/x,c/z}2], P(c,d)[6,{d/y}2], S(b,c)[{a/z,b/x, c/y}3,{b/x, c/z}4], P(c,d)[6,{d/y}4], Per(b,f)[8,4]}, {GF(a,d)[{a/x, c/z,d/y}2,+], A(b,d)[{b/x, c/z, d/y}4,+]}}.

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

dolgen1.wmf

Схема вывода

В ходе решения задачи было показано, что Семен – отец Виктора (F(a,c)), Виктор и Антонина – брат и сестра (S(b,c)), а у Семена имеется внучка Ольга (GF(a,d)), Антонина является тетей Ольги (A(b,d)).

Анализ полученной в ходе осуществления вывода схемы позволяет сделать следующие заключения. Применение предлагаемого метода, в сравнении с классическими методами резолюций Робинсона и обратного вывода Маслова, позволяет сократить число шагов до двух раз с одновременным ростом трудоемкости выполняемых операций. Тем не менее существенный выигрыш в общем времени решения задачи может быть достигнут за счет внутреннего параллелизма, заложенного в базовой операции метода – операции деления дизъюнктов. При этом предварительные результаты экспериментов, проведенных на тестовом наборе сгенерированных машинным способом задач, показали, что в случае ориентации только на AND-параллелизм сокращение временных затрат составляет порядка 21 %. Совмещение AND- и OR-уровней увеличивает выигрыш до 34 %.

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


Библиографическая ссылка

Долженкова М.Л., Страбыкин Д.А., Чистяков Г.А., Мельцов В.Ю. ВЫВОД СЛЕДСТВИЙ В ИСЧИСЛЕНИИ ПРЕДИКАТОВ С ПОСТРОЕНИЕМ СХЕМЫ ВЫВОДА // Современные наукоемкие технологии. – 2018. – № 3. – С. 47-54;
URL: http://top-technologies.ru/ru/article/view?id=36935 (дата обращения: 22.09.2020).

Предлагаем вашему вниманию журналы, издающиеся в издательстве «Академия Естествознания»
(Высокий импакт-фактор РИНЦ, тематика журналов охватывает все научные направления)

«Фундаментальные исследования» список ВАК ИФ РИНЦ = 1.074