Наконец, стоит отметить, что если заданный набор WFF-формул может допускать несколько интерпретаций, в которых эти WFF-формулы принимают истинные значения, то он (в общем случае) может иметь несколько моделей. Таким образом, база данных в общем случае может иметь несколько различных моделей, так как с модельно-теоретической точки зрения она является просто набором WFF-формул. Подробности приводятся в разделе 23.5.

Ставдартная форма

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

Ниже кратко изложен весь процесс конвертирования, а более подробное описание представлено в [23.10]. Все этапы этого процесса демонстрируются на основе следующей WFF-формулы.

FORALL X ( р ( X ) AND EXISTS у ( FORALL z { q { у, z ) ) ) )

В этой формуле р и gявляются предикатами, а. х, уи z - переменными.

1. Сначала следует, как это было сделано в разделе 23.3, исключить из записи символы => . В рассматриваемом примере данная операция не оказывает никакого влияния на вид WFF-формулы.

2. Далее нужно использовать законы Де Моргана, а также тот факт, что две смежные операции NOT нейтрализуют одна другую, но применять эти операции по отноще-нию к термам, а не к общим WFF-формулам. В рассматриваемом примере эта операция не оказывает никакого влияния на вид WFF-формулы.

3. Теперь необходимо конвертировать WFF-формулу в предваренную нормальную форму, перенося кванторы в начало формулы (и систематически переименовывая переменные в случае необходимости).

FORALL X ( EXISTS у ( FORALL Z ( р( х ) AND q( у, Z ) ) ) )

4. Обратите внимание, что если содержащая кванторы WFF-формула, такая как EXISTS V ( г ( V ) ),

эквивалентна другой WFF-формуле, например г ( а ),

с некоторой (неизвестной) константой а, то в исходной WFF-формуле утверждается, что такая константа существует, хотя ее значение неизвестно. Точно так же WFF-формула

FORALL U ( EXISTS v ( s ( u, v ) ) ) эквивалентна WFF-формуле FORALL u ( s ( u, f ( u ) ) )

для некоторой неизвестной функции /, универсально квантифицированной переменной и. Константа а и функция / в этих примерах называются в честь ученого-логика Сколема (Skolem) соответственно константой Сколема (Skolem constant) и функцией Сколема, где константа Сколема- это просто функция Сколема без аргументов. Таким образом, на следующем этапе необходимо исключить излишнюю квантификацию, заменяя соответствующие квантифицированные переменные произвольными функциями Сколема всех универсально квантифицированных переменных, которые предшествуют данному квантору в WFF-формуле.

FORALL X ( FORALL Z ( р ( х ) AND q ( f ( х ), z ) ) )

5. Теперь все переменные универсально квантифицированы; следовательно, можно принять соглашение, что все они неявно универсально квантифицированы, и опустить явные кванторы.

р ( X ) AND q ( f ( X ), Z )

6. Далее необходимо конвертировать WFF-формулу в конъюнктивную нормальную форму, т.е. в набор предложений, объединенных с помощью операции AND и, вероятно, содержащих связки NOT и OR, но только не связку AND. В рассматриваемом примере WFF-формула уже находится в такой форме.

7. Разместим каждое предложение в отдельной строке и опустим все связки AND. Р ( X )

q ( f ( X ), Z )

Это и есть стандартная форма, эквивалентная оригинальной WFF-формуле.

Замечание. Из описанной выше процедуры следует, что общий вид WFF-формулы в стандартной форме представляет собой набор предложений, размещенных в отдельных строках с приведенным ниже синтаксисом.

NOT Al OR NOT Л2 OR ... OR NOT Am OR Bl OR B2 OR ... OR Bn

Здесь все Aw В являются неотрицаемыми термами. Тот же синтаксис можно представить в другом виде.

А1 AND А2 AND ... AND ЛЛ1 => BJ OR В2 OR ... OR Вл

Если в этой записи присутствует по крайней мере один член В (л = О или п = 1), то она в честь ученого-логика Альфреда Хорна (Alfred Horn) называется предложением Хорна.

Использование правила резолюции

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

l.MOTHER OF( Anne, Betty ) 2. MOTHER OF( Betty, Celia )

Кроме того, дана WFF-формула ( дедуктивная аксиома ), которая, по сути, является предложением Хорна.

3.M0THER 0F( X, у ) AND MOTHER OF( у, z ) =>

GRANDMOTHER OF( х, Z )

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

4. NOT MOTHER OF( х, у ) OR NOT MOTHER OF( у, Z ) OR

GRANDMOTHER OF( x, Z )

Далее необходимо показать, как доказывается утверждение, что Анна является бабушкой Селии, т.е. как ответить на запрос Является ли Анна бабушкой Селии? . Для этого нужно начать с отрицания заключения, которое требуется доказать, и принять его как дополнительную предпосылку.

5. NOT GRANDMOTHER OF( Anne, Celia )

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

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

Для того чтобы проиллюстрировать описанный выше процесс, обратимся к примеру. Прежде всего следует обратить внимание на то, что строки в пп. 4 и 5 содержат термы GRANDMOTHER OF(x,z) и NOT GRANDMOTHER OF ( Anne, Celia) соответственно. Таким образом, в строке п. 4 нужно подставить значение Аппе вместо х и значение Celia - вместо Z. После совмещения получится такой результат.

6. NOT MOTHER OF( Anne, у ) OR NOT MOTHER OF( у, Celia )

Строка п. 2 содержит выражение MOTHER OF(Betty, Celia), поэтому можно подставить значение Betty вместо у в строке п. 6 и после совмещения получить новое выражение.

7. NOT MOTHER OF( Anne, Betty )

Совместив строки в пп. 7 и 1, получим пустое множество предложений [ ], т.е. противоречие. Следовательно, результатом выполнения исходного запроса будет ответ Да, Анна является бабушкой Селии .

Теперь можно проанализировать, как будет выполняться запрос Кто является внучкой Анны? . Сложность поставленной задачи заключается, прежде всего, в том, что системе ничего не известно о внучках, она обладает информацией только о бабушках. В этом случае можно было бы добавить еще одну дедуктивную аксиому, согласно которой Z является внучкой х тогда и только тогда, когда х является бабушкой z (предполагается, что в рассматриваемой базе данных не содержатся сведения о мужчинах). Тогда исходный запрос можно перефразировать - Чьей бабушкой является Анна? - и использовать тот же набор предпосылок, что и прежде.