примерах.
Пример 4.1. Докажем справедливость одного из правил вывода натурального исчисления, которое называется правилом дилеммы:
A C,B C,A B;.
C
Подразумевается, что из формул над чертой выводится формула под чертой. Можно считать, что верхние формулы представляют собой посылки, а нижняя – следствие из них.
Чтобы применить аппарат АК, положим, что XA, XB и XC – логические переменные с областью значений {0, 1}. Преобразуем конъюнкцию верхних формул в D-систему в схеме отношения [XAXB XC], для чего воспользуемся соотношением (1.1):
|
|
|
|
|
|
{0} |
{1} |
||
Up[XAXB XC] = |
|
|
{0} |
{1} . |
|
|
|
|
|
|
{1} |
{1} |
|
|
|
|
|
|
|
Нижняя часть правила выражается как C-кортеж Down[XC] = [{1}]. Чтобы доказать справедливость правила методами АК, нужно проверить соотношение
Up[XAXB XC] G Down[XC].
Если, согласно приведенным в предыдущих главах алгоритмам, преобразовать Up[XAXB XC] в C-систему, то:
{1} |
{0} |
{1} |
Up[XAXB XC] = |
{1} |
. |
|
{1} |
|
В таком случае |
проверку включения Up[XAXBXC] G Down[XC] можно |
|
осуществить с помощью алгоритма полиномиальной сложности. Для этого: |
||
1) добавим фиктивные атрибуты в Down[XC]: |
||
Down[XAXB XC] = [ {1}];
2) проверим включение каждого C-кортежа из Up[XAXB XC] в Down[XAXB XC], что легко выполнить на основе известных соотношений АК (теорема 2.3). Тем самым подтверждается справедливость вывода.
Тот же результат можно получить, если использовать теорему 4.3. Для этого нужно в Up[XAXB XC] добавить еще один дизъюнкт, соответствующий
135
формуле C, и убедиться, что полученный АК-объект пуст. |
Формула C |
||||||||
моделируется D-кортежем |
|
|
|
проверяемый |
|||||
Down[XAXB XC ] = ] {0}[, тогда |
|||||||||
АК-объект будет равен D-системе |
|
|
|
|
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
|
|
{0} |
{1} |
|
|
|||
|
|
|
|
|
|
{0} |
{1} |
|
|
Up[XAXB XC] G Down[XA XB XC |
] = |
. |
|
||||||
|
{1} |
|
|
||||||
|
|
|
|
{1} |
|
|
|||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
{0} |
|
|||
Используя изложенные ранее алгоритмы вычислений, нетрудно проверить, что полученная D-система пуста. Для этого можно использовать алгоритм преобразования D-системы в альтернативный класс (подраздел 2.2).
Разработанные алгоритмы проверки правильности следствия применимы не только в рамках исчисления высказываний, но и для более широкого класса логических систем.
Пример 4.2. Данный пример приводится для иллюстрации некоторых алгоритмов логического вывода в АК. Допустим, что область значений каждой из переменных x, y, z есть множество {a, b, c, d}, а посылки интерпретируются АК-объектами, заданными в универсуме X Y Z = {a, b, c, d}3. Пусть предполагаемым следствием является импликация "Если x равно a или c, то z равно d", а обобщенное пересечение АК-объектов, отображающих посылки,
равно |
C-системе |
{b,d} {a,c} {a,d} |
Необходимо |
проверить |
||
R = |
|
. |
||||
|
|
{a,b} |
{d} |
|
|
|
корректность следствия. |
|
|
|
|
||
Запишем предполагаемое следствие |
в структурах АК. |
Утверждение |
||||
"x равно a или c", можно выразить как P1[X] = [{a, c}], а утверждение "z равно
d" – как P2[Z] = [{d}]. Соотношение P1[X] P2[Z] |
эквивалентно формуле |
|||||||
|
|
P2[Z], которая в структурах АК имеет вид |
|
|
G P2[Z] и может быть |
|||
|
P1[X] |
P1[X] |
||||||
|
|
|
|
|
|
|
|
|
|
|
{b,d} |
|
или D-кортеж ]{b, d} {d}[. |
||||
представлена как C-система T[XZ] = |
|
|||||||
|
|
|
{d} |
|
|
|
|
|
Проверку включения R[XYZ] G T[XZ] проще выполнить, если T[XZ] будет выражено как D-кортеж. Тогда можно использовать теоремы 2.16 и 2.18. Согласно теореме 4.2, следствие в данном примере корректно, поскольку соблюдается соотношение
136
|
|
|
|
|
{b,d} {a,c} {a,d} |
G ]{b, d} {d}[. |
|||
|
|
{d} |
|
|
{a,b} |
|
|
||
Такой же результат дает и теорема 4.3, если вычислить R[XYZ] G T[XZ] и показать, что результат равен пустому множеству. Тогда с помощью теоремы 2.5 получим:
|
|
|
|
|
{b,d} {a,c} {a,d} |
G [{a, c} {a, b, c}] = . |
|||
|
|
{d} |
|
|
{a,b} |
|
|
||
Значит, правильность вывода подтверждается.
Пример 4.3 [Мендельсон, 1984]. Проверить правильность логического вывода для следующего рассуждения: "Если Джонс не встречал этой ночью Смита, то либо Смит был убийцей, либо Джонс лжет. Если Смит не был убийцей, то Джонс не встречал Смита этой ночью, и убийство имело место после полуночи. Если убийство имело место после полуночи, то либо Смит был убийцей, либо Джонс лжет. Следовательно, Смит был убийцей".
Сначала выразим данное рассуждение на языке исчисления высказываний. Введем обозначения:
A – Джонс встречал этой ночью Смита; B – Смит был убийцей;
C – Джонс лжет;
D – убийство имело место после полуночи.
Тогда заданное рассуждение можно сформулировать так:
-первое предложение: A (B C);
-второе предложение: B ( A D);
-третье предложение: D (B C);
-следствие: B.
Преобразуем первые три предложения, используя формулы (1.1) и (1.2) для того, чтобы избавиться в них от импликации и строгой дизъюнкции. Получаем:
1)A (B C) = A (B C) ( B C);
2)B ( A D) = В ( A D);
3)D (B C) = D (B C) ( B C).
137
Для представления этих формул АК-объектами используем универсум
X1 X2 X3 X4 = {0, 1}4, где A = B = C = D = 1 и A = B = C = D = 0. Тогда посылки, которые являются ДНФ, выражаются C-системами:
|
|
{1} |
|
|
|
|
|
|
|
|
|
|
|
|
|
{0} |
|
||
|
|
|
|
|
|
|
|
|
|
{1} |
|
|
|
|
|
|
|
|
|
P1 |
= |
|
|
{1} |
{0} |
|
P2 |
= |
; P3 |
|
{1} |
{0} |
|
|
, |
||||
|
; |
|
|
|
|
= |
|
||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||
|
|
|
|
{0} |
{1} |
|
|
|
{0} |
{1} |
|
|
{0} |
{1} |
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
а следствие – C-кортежем S[X2] = [{1}]. Решить задачу можно двумя способами:
1)проверить соотношение (P1 G P2 G P3) G S[X2];
2)определить пустоту АК-объекта P1 G P2 G P3 G S[X2 ].
Поскольку в |
любом |
из |
этих |
способов |
присутствует выражение |
||
P1 G P2 G P3, то целесообразно вычислить соответствующий ему АК-объект. |
|||||||
После вычисления имеем: |
|
|
|
|
|
|
|
|
|
|
|
|
|
||
|
|
|
|
{1} |
{1} |
{0} |
|
P[X1X2X3X4] = P1 |
G P2 |
G P3 |
= |
{1} |
{0} |
. |
|
|
|
|
{0} |
{0} |
{1} |
{1} |
|
|
|
|
|
|
|
|
|
Для проверки включения добавим недостающие атрибуты в S:
S[X1X2X3X4] = [ {1} ].
Проверка показывает, что третий C-кортеж из P не включен в S, то есть
вывод неверный. Тот же результат получим, найдя пересечение P G S[X2 ]:
|
|
|
|
|
|
|
|
|
{1} |
{1} |
{0} |
|
|
||
|
|
{1} |
{0} |
|
|
G |
[ {0} ] = [{0} {0} {1} {1}] . |
|
|
||||||
{0} |
{0} |
{1} |
{1} |
|
|
|
|
|
|
|
|
|
|
|
|
Предложенный подход к решению задач логического вывода позволяет по-новому осмыслить суть логического следования в классической логике. Как известно, справедливость отношения A B означает, что B есть необходимое условие или свойство A. Соотношение (4.1) показывает: логическое следствие корректно не только потому, что получено на основе правил вывода, смысл которых не всегда понятен, но еще и потому, что является необходимым условием существования антецедента.
138
4.2.3. Алгоритмы решения задачи вывода произвольных следствий
Такая задача в общем виде не представляет интереса, поскольку на практике поиск возможных следствий целесообразен только при наличии перечисленных далее ограничений:
1)в следствии желательно использовать лишь небольшую часть всех переменных рассуждения;
2)состав переменных в искомом следствии нередко определяется, исходя из смыслового анализа конкретной системы рассуждений.
Применение правил вывода в качестве механизма получения следствий при заданных ограничениях часто требует перебора большого числа вариантов, так как заранее невозможно предсказать порядок применения правил.
При использовании методов АК задача существенно упрощается. Когда задано множество АК-объектов {A1, …, An}, представляющих аксиомы (или посылки), то можно найти АК-объект A = A1 G … G An. Тогда для получения любого следствия достаточно построить АК-объект Bj такой, чтобы выполнялось соотношение A G Bi.
Рассмотрим теперь формальные правила вывода следствий. Когда A – C-система (если это не так, то можно использовать алгоритмы преобразования D-кортежей или D-систем в C-системы), то сокращение числа переменных в Bi осуществимо с помощью элиминации атрибутов из A. Ясно, что при этом соотношение A G Bi будет выполняться.
При элиминации атрибутов из C-системы образуется проекция, свойства которой определяют дальнейшие действия по выводу следствий. Проекции могут быть полными, т.е. содержащими все элементарные кортежи для их схем отношения, и неполными в противном случае. Если проекция полная, то ее следствие есть частный универсум, что равносильно общезначимой формуле и интереса не представляет. Поэтому будем учитывать только неполные проекции.
Подтверждением сказанному может служить промежуточный результат из примера 4.1:
{1} |
{0} |
{1} |
Up[XAXB XC] = |
{1} |
. |
|
{1} |
|
|
|
139 |