Основы построения и функционирования интеллектуальных информационных систем. Былкин В.Д - 28 стр.

UptoLike

ВУЗ: 

ПГУ | Пенза

Составители: 

Рубрика: 

28
Шаг 2. Переименовать, если необходимо, связанные переменные таким образом, чтобы никакая
переменная не имела бы одновременно свободных и связанных вхождений. Это условие
рассматривается и по отношению к подформулам.
Шаг 3. Удалить те квантификации, область действия которых не содержит вхождений
квантифицированной переменной.
Шаг 4. Перенести отрицания внутри формулы в соответствия со следующими правилами:
; ; ; .
Шаг 5. Перенести все квантификации в начало формулы (см. основные равносильные формулы
3...8).
Пример. Найти предварѐнную нормальную форму формулы
.
Решение.
Шаг 1:
Шаг 2:
Шаг 3:
Шаг 4:
Шаг 5: .
.
Предваренная нормальная форма включает в себя префикс, образованный кванторами и
Ǝи матрицу, под которой понимается формула, не содержащая квантификаций.
Приведение формулы ЛП к сколемовской форме (сколемизация) призвано обеспечить
дальнейшее упрощение логических представлений и облегчить введение процедур машинной
обработки в ЛП. Отправной точкой сколемизации является предваренная нормальная форма,
матрица которой приведена к конъюнктивной нормальной форме (КНФ). Цель сколемизации -
исключение Ǝ- квантификаций. Сколемовская форма получается путем применения следующей
процедуры:
1) сопоставить каждой Ǝ- квантифицированной переменной список - квантифицированных
переменных, предшествующих ей, а также некоторую еще не использованную функциональную
константу, число мест, у которой равно мощности списка. Данная константа будет представлять
сколемовскую функцию;
B
ABA ,
AxxA ~
BABA &~&
AA ~
)( xyyx
))),,(zv),((&)(( yxaRyxQxyxPx
))),,(zv),((&)(( yuaRyuQuyxPx
))),,(v),((&)(( yxaRyxQxyxPx
))),,(v),((&)(( yxaRyxQxyxPx
))),,(v),((&)(( yuaRyuQxPuyx
Шаг 2. Переименовать, если необходимо, связанные переменные таким образом, чтобы никакая
переменная не имела бы одновременно свободных и связанных вхождений. Это условие
рассматривается и по отношению к подформулам.
Шаг 3. Удалить те квантификации, область действия которых не содержит вхождений
квантифицированной переменной.
Шаг 4. Перенести отрицания внутри формулы в соответствия со следующими правилами:
 A         B, A
          B        ;    xA ~ x A ; A & B ~ A & B ; A ~ A .

Шаг 5. Перенести все квантификации в начало формулы (см. основные равносильные формулы
3...8).
Пример. Найти предварѐнную нормальную форму формулы
 x               (y                 xy ) .
Решение.

Шаг 1:      x( P( x) & y x(Q( x, y)v zR(a, x, y)))

Шаг 2:      x( P( x) & y u(Q(u, y)v zR(a, u, y)))

Шаг 3:      x( P( x) & y x(Q( x, y)vR(a, x, y)))

Шаг 4:      x( P( x) & y x(Q( x, y ) vR(a, x, y )))

Шаг 5:      x y ( p( x) & u (Q(u, y ) vR(a, u, y))) .

            x y u ( P( x) & (Q(u, y) vR(a, u, y))) .

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

Ǝи матрицу, под которой понимается формула, не содержащая квантификаций.
          Приведение формулы ЛП к сколемовской форме (сколемизация) призвано обеспечить
дальнейшее упрощение логических представлений и облегчить введение процедур машинной
обработки в ЛП. Отправной точкой сколемизации является предваренная нормальная форма,
матрица которой приведена к конъюнктивной нормальной форме (КНФ). Цель сколемизации -

исключение Ǝ- квантификаций. Сколемовская форма получается путем применения следующей
процедуры:

1) сопоставить каждой Ǝ- квантифицированной переменной список         - квантифицированных
переменных, предшествующих ей, а также некоторую еще не использованную функциональную
константу, число мест, у которой равно мощности списка. Данная константа будет представлять
сколемовскую функцию;


                                                        28

Страницы