5.1.8. Хорновские дизъюнкты

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

Пример хорновского дизъюнкта: (p  q  r  s). Очевидно, что он эквивалентен формуле (p  q  r)  s. Часто хорновские дизъюнкты задаются перечислением составляющих их литер: (p, q, r, s).

Хорновский дизъюнкт называется точным, если он содержит позитивную литеру, наряду с негативными. Такой дизъюнкт представляет некоторое правило при описании предметной области.

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

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

Пусть необходимо проверить формулу, называемую целью, выводима ли она из множества фактов и правил предметной области. Выводимая формула представляется негативным дизъюнктом. Получаем множество хорновских дизъюнктов. Применение к нему резолюций есть реализация доказательства методом от противного: исходя из фактов, правил и отрицания цели, приходим к противоречию – пустому дизъюнкту. Если S – множество хорновских дизъюнктов, то возможное число резолюций не больше числа литер в S.

Рассмотрим пример:

S = {p  r  t, q, r, t  p  r, t  q, p  q  r}.

В этом множестве q, r – факты; t  q, p  r  t, t  p  r – последовательно выводимые правила; p  q  r – дизъюнкт цели.

Воспользуемся алгоритмом Блейка.

Выполнив операцию резолюции над первым и третьим дизъюнктами, получаем множество дизъюнктов с меньшим числом символов:

{p  t, q, r, t  p  r, t  q, p  q  r}.

Выполнив операцию резолюции над вторым и третьим дизъюнктами, имеем

{p  t, q, r, t  p, t  q, p  q  r}.

Далее выполняем операцию резолюции над вторым и пятым дизъюнктами и операцию поглощения дизъюнктов:

{p  t, q, r, t, p  q  r}.

Выполняем операцию резолюции над первым и четвертым дизъюнктами:

{p, q, r, t, p  q  r},

над первым и пятым, над вторым и пятым – имеем

{p, q, r, t, r}.

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

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

КАДР

5.2. Исчисление предикатов

5.2.1. Словарь

Основными символами языка являются переменные, функциональные константы (функциональные константы, зависящие от пустого множества аргументов, называют индивидными константами), предикатные константы (предикатные константы, зависящие от пустого множества аргументов, являются элементарными высказываниями), связки (, , , , ~), кванторы общности  (для всех) и квантор существования  (существует). Скобки применяются для определения порядка действия связок и для задания области действия кванторов.

Договоримся использовать следующие обозначения:

x, y, z,… – переменные,

a, b, c,… – индивидные константы,

f, g, h,… – функциональные константы,

p, q, r,… – элементарные высказывания,

P, Q, R,… – предикатные константы.

КАДР