ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Journal influence

Higher Attestation Commission (VAK) - К1 quartile
Russian Science Citation Index (RSCI)

Bookmark

Next issue

2
Publication date:
17 June 2024

The method of parallel logical inference of consequences for propositional calculus

The article was published in issue no. № 2, 2012 [ pp. 142 ]
Abstract:A method for new facts obtaining from the current knowledge base and incoming facts is offered. A substantial and a formal statements of the problem, a formal description of the inference procedure and a description of the offered method are considered. The method operation is illustrated by an example of consequences inference.
Аннотация:Предлагается метод получения новых фактов из текущей базы знаний на основе поступивших фактов. Приводятся содержательная и формальная постановки задачи, формальное описание процедуры вывода и описание предлагаемого метода. Работа метода иллюстрируется примером вывода следствий.
Authors: (favt_agalakov@vyatsu.ru) - , (strabykin@mail.ru) - , Ph.D, (m.tomchuk@mail.ru) - , Ph.D
Keywords: parallel computing, output logical consequences, inference
Page views: 10015
Print version
Full issue in PDF (5.19Mb)
Download the cover in PDF (1.31Мб)

Font size:       Font:

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

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

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

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

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

Пусть исходная БЗ представлена множеством дизъюнктов MP={D1, D2, …, Di, …, DI}; новые факты заданы множеством литералов MF={L1, L2, …, Lp, …, LP}, а результат логического вывода – множеством литералов MR={R1, R2, …, Rl, …, RL}. Тогда формально задачу логического вывода следствий можно описать следующим образом.

Требуется определить множество фактов MR, которые могут быть выведены из базы исходных посылок MP и множества новых фактов MF.

Вывод следствий. Для вывода следствий текущего шага используется специальная процедура V+={MP, MF, q, p, M1, MR}, в которой MP={D1, D2, …, Di, …, DI} – множество текущих фактов и правил (множество дизъюнктов исходных посылок); MF={L1, L2, …, Lp, …, LP} – множество литералов новых фактов; q – признак наличия решения, который может принимать одно из следующих значений: 0 – получены факты-следствия, 1 – из множеств MP и MF новые факты не могут быть выведены; p – признак возможности продолжения вывода: 0 – дальнейший вывод возможен, 1 – вывод завершен; M1 – новое множество дизъюнктов исходных секвенций; MR={R1, R2, …, Rl, …, RL} – множество фактов-следствий из посылок MP и фактов MF.

Процедура применима, если MP≠Æ и каждый дизъюнкт множества MP содержит хотя бы один литерал. В процедуре выполняются следующие действия.

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

2.     Все дизъюнкты исходных секвенций делятся на дизъюнкт F, образуя остатки bi=Di¸F [Вожегов Д.В., Страбыкин Д.А.]. Если все остатки bi равны единице или содержат литералы с инверсией, дальнейший вывод невозможен, принимается q=1, p=1 и производится переход к п. 5. В противном случае выполняется п. 3.

3.     Формируется множество следствий MR, в которое включаются однолитеральные остатки bi, содержащие литералы без инверсии. Устанавливается значение признака q=1.

4.     Формируется новое множество исходных секвенций M1=MP–M0, где M0 – подмножество дизъюнктов множества MP, для которых выполняется условие D¸F=L, где L – любой литерал без инверсии. Если получено непустое множество, устанавливается значение признака p=0 (возможно продолжение вывода), в противном случае принимается p=1 (вывод завершен).

5.     Конец процедуры.

Метод логического вывода следствий. Данный метод базируется на процедуре вывода следствий и состоит из ряда шагов, на каждом из которых выполняется набор процедур вывода V+, причем результаты выполнения процедуры i-го шага становятся исходными данными для процедуры i+1-го шага. Процесс заканчивается в случае, если дальнейший вывод следствий из конъюнктов невозможен (получено значение признака q=0 или p=1).

1.     Определяются начальные значения: h=1, M10=MP–Mфакт, MF1=MF+Mфакт, где Mфакт – подмножество однолитеральных дизъюнктов множества исходных посылок.

2.     Выполняются процедуры вывода текущего шага V+h={M1h-1, MFh, qh, ph, M1h, MRh}.

3.     Формируется новое множество фактов: MFh+1=MFhÈMRh (повторения одного и того же литерала во множество MFh+1 не включаются).

4.     Проверяется признак окончания вывода: если ph=0, вывод продолжается: h увеличивается на единицу и производится переход к п. 2, иначе выполняется п. 5.

5.     Формируются результаты вывода: общий признак решения  и множество следствий MR=MFh+1–MF1.

6.     Строится схема вывода логических следствий: на схему помещаются вершины, содержащие номера правил из множества исходных посылок, соединенные в соответствии с суперпозицией правил в выводе. Дуги, входящие в вершины схемы, помечаются обозначениями литералов, составляющих антецедент правила. Исходящие дуги соответствуют литералам-следствиям.

Можно отметить, что в каждой процедуре вывода деление дизъюнктов исходных посылок на дизъюнкт F может производиться параллельно.

Пример вывода следствий. Пусть база исходных посылок задана множеством секвенций:

ABC; 1D; CDE; EVL; 1P;

LR; MPN; 1S; RU; NV;

SRX; XZ.

Необходимо установить, какие следствия можно вывести из фактов MF={A, B, M}.

1. Определяются начальные значения: h=1, M10={       }, MF1={A, B, M, D, P, S}.

Подпись:  2. Выполняется процедура вывода V+1, результатами которой становятся признаки q1=0, p1=0 и множества M11={      }, MR1={C, N}.

3. Формируется новое множество фактов: MF2={A, B, M, D, P, S, C, N}.

4. Проверяется признак окончания вывода: если p1=0, вывод продолжается.

Далее выполняются процедуры второго и последующих шагов. Результаты процедур вывода сведены в таблицу.

Шаг h

Процедура

Признаки ph, qh

Факты MFh

Следствия шага MRh

1

V+1

0, 0

A, B, M, D, P, S

C, N

2

V+2

0, 0

A, B, M, D, P, S, C, N

E, V

3

V+3

0, 0

A, B, M, D, P, S, C, N, E, V

L

4

V+4

0, 0

A, B, M, D, P, S, C, N, E, V, L

R

5

V+5

0, 0

A, B, M, D, P, S, C, N, E, V, L, R

U, X

6

V+6

1, 0

A, B, M, D, P, S, C, N, E, V, L, R, U, X

Z

-

-

-

A, B, M, D, P, S, C, N, E, V, L, R, U, X, Z

-

Таким образом, в результате вывода получено 9 фактов-следствий: C, N, E, V, L, R, U, X, Z. Причем следствия Z и U являются конечными, так как дальнейший вывод из них невозможен. Вывод закончился на шестом шаге с признаком Q=0. Схема вывода следствий показана на рисунке (обозначения фактов множества MF выделены курсивом).

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

Метод обладает глубоким параллелизмом, что дает возможность эффективно применять его при реализации интеллектуальных систем на современных высокопроизводительных параллельных вычислительных платформах.

Литература

Вожегов Д.В., Страбыкин Д.А. Метод параллельного дедуктивного логического вывода с определением фактов // Науч.-технич. вестн. Поволжья. 2011. № 1. С. 97–99.


Permanent link:
http://swsys.ru/index.php?page=article&id=3132&lang=en
Print version
Full issue in PDF (5.19Mb)
Download the cover in PDF (1.31Мб)
The article was published in issue no. № 2, 2012 [ pp. 142 ]

Perhaps, you might be interested in the following articles of similar topics: