Пример логического вывода

Рассмотрим пример логического вывода с модификацией посылок.

Задано исходное множество посылок M:

AB;

BC;

CE;

EN;

LD;

FG;

IJ;

G&JK;

KL.

Также задано множество выводимых заключений m, состоящее из двух подмножеств m_p и m_n: 1) AEm_p; 2) FCm_p; 3) BEm_n; 4) FNm_n.

Требуется модифицировать исходное множество посылок M таким образом, чтобы заключения из подмножества m_p выводились из М, а заключения из подмножества m_n — не выводились.

Исходные данные представлены схемой на рис. 1.

Рис. 1. Исходные посылки для примера модификации

Исходные посылки представляются в виде дизъюнктов:

B (D₁);

C (D₂);

E (D₃);

N (D₄);

D (D₅);

G (D₆);

J (D₇);

K (D₈);

L (D₉).

Аналогично представляются заключения:

1) E (d₁); 2) C (d₂); 3) E (d₃); 4) N (d₄).

Процесс модификации посылок является циклическим и состоит из ряда шагов.

Цикл 1

Шаг 1. Все заключения, принадлежащие множеству m, с помощью проверочного дедуктивного вывода делятся на четыре класса:

d^pp=d₁=E (логически следует из множества М и принадлежит m_p);

d^np=d₂=C (не выводится из исходных посылок и принадлежит m_p);

d^pn=d₃=E (принадлежит подмножеству m_n и выводится из М);

dⁿⁿ=d₄=N (принадлежит подмножеству m_n и не выводится из М).

Шаг 2. Находятся множества посылок, соответствующие классам n/p и p/n. Для заключения d₂=C, входящего в класс n/p, сгенерируем семейство множеств ^np добавляемых дизъюнктов. При добавлении любого из множеств этого семейства дедуктивный логический вывод заключения d₂ должен оканчиваться успешно. Семейство множеств ^np будем генерировать с помощью метода добавления посылок.

Для заключения d₂ и множества М результатом данного метода будет являться следующее семейство множеств:

^np=[M^*₁, M^*₂, M^*₃, M^*₄, M^*₅, M^*₆, M^*₇, M^*₈],.

где M^*₁={C}, M^*₂={B}, M^*₃={A, J}, M^*₄={A, I}, M^*₅={A, J}, M^*₆={A, I}, M^*₇={A, J}, M^*₈={A, I}.

Заключение

d₃=E входит в класс p/n, следовательно, нужно найти семейство таких множеств дизъюнктов, при удалении любого из которых из множества М заключение d₃ перестает быть логическим следствием исходных посылок. Создавать семейство множеств ^pn удаляемых дизъюнктов будем при помощи метода удаления посылок. Результатом этого метода для множества М и заключения d₃ будет следующее семейство множеств:

^pn=[,], где ={C}, ={E}.

Шаг 3. Определяются множества посылок из семейств множеств ^np, которые можно включить во множество исходных посылок без влияния на отсутствие выводимости заключений класса n/n.

Чтобы найти такие множества, будем последовательно добавлять каждое множество из семейства ^np во множество М и выполнять проверочный дедуктивный вывод заключения, входящего в класс n/n. После неудачной проверки (то есть заключение класса n/n стало выводиться) нужно удалить включенное множество. Иначе поиск множеств заканчивается.

Последовательно включая по одному множества M^*₁-M^*₈ во множество М и производя проверочный вывод заключения d₄=N, получаем, что ни одно из множеств семейства ^np не удовлетворяет требованиям выводимости заключения d₄. Следовательно, на данном шаге ни одно из этих множеств не добавляется к множеству М.

Заключение

d₂ остается в классе n/p.

Шаг 4. Находятся такие множества посылок семейств ^pn, которые можно удалить без влияния на выводимость заключений класса p/p.

Чтобы найти такие множества, будем последовательно удалять множества семейства ^pn из множества исходных посылок и осуществлять проверку с помощью дедуктивного логического вывода, выводится ли заключение d₁=E, принадлежащее классу р/р. Если заключение перестает выводиться, то текущее множество удаляется из множества исходных посылок. Удаляя сначала множество ={C}, а затем множество ={E}, получаем, что при удалении любого из этих множеств заключение d₁ перестает выводиться из множества М. То есть на данном шаге ни одно из этих множеств нельзя удалять из множества исходных посылок.

Заключение

d₃ остается в классе p/n.

Шаг 5. Проверяется, имеются ли заключения в классах p/n и n/p. Заключения в данных классах присутствуют, следовательно, вывод продолжается. Проверяется, имеет ли место ситуация зацикливания. Действительно, множество М исходных посылок на пятом шаге не изменилось по сравнению с первым шагом данного цикла, следовательно, возникло зацикливание.

Для разрешения ситуации зацикливания применяем способ безусловной модификации. Для добавления во множество исходных посылок выбирается множество M^*₈={A, I}. После добавления множества M^*₈ множество исходных посылок М принимает вид, показанный на рис. 2.

Рис. 2. Схема исходных посылок после первого цикла

Циклы 2 и 3

В начале второго цикла имеет место следующее разделение на классы:

классу p/p принадлежат заключения d₁=E, d₂=C.

классу p/n принадлежат заключения d₃=E, d₄=N.

В ходе выполнения второго и третьего циклов выясняется, что при удалении дизъюнктов E и N заключения класса p/n перейдут в требуемый класс n/n. Однако при этом перестанет выводиться заключение d₁=E.

Множество исходных посылок М после третьего цикла принимает вид, показанный на рис. 3.

Рис. 3. Схема исходных посылок после третьего цикла

Цикл 4

Классы заключений в начале четвертого цикла выглядят следующим образом:

1) р/р: d₂=C; 2) n/p: d₁=E; 3) n/n: d₃=E, d₄=N.

Определяется, что для перевода заключения d₁ в класс р/р требуется добавить дизъюнкт E.

Таким образом, результатом метода модификации посылок является модифицированное множество исходных посылок М (рис. 4):

B (D₁);

C (D₂);

D (D₅);

G (D₆);

J (D₇);

K (D₈);

L (D₉);

A (D₁₀);

I (D₁₁);

E (D₁₂).

Рис. 4. Схема модифицированного множества исходных посылок