Логическое программирование на языке Visual Prolog. Солдатова О.П - 10 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

10
называется пустым дизъюнктом-
. Так как пустой дизъюнкт не
содержит литералов, которые могли бы быть истинными при любых
интерпретациях, то пустой дизъюнкт всегда ложен.
Определение 2: Множество дизъюнктов S есть конъюнкция всех
дизъюнктов из S , где каждая переменная в S считается управляемой
квантором всеобщности.
Вследствие последнего определения, ССФ может быть представлена
множеством дизъюнктов.
Пример 2. Получить скулемовскую стандартную
форму формулы
(
∀
x) (P(x)
∧
(
∀
y)(
¬
(
∀
z)Q(x, y)
→
(
∃
u)R(u, x, y))) и представить её в
виде множества дизъюнктов.
1. Исключим связки импликации:
(
∀
x) (P(x)
∧
(
∀
y)(
¬
¬
(
∀
z)Q(x, y)
∨
(
∃
u)R(u, x, y))).
2. Удалим бесполезные кванторы:
(
∀
x) (P(x)
∧
(
∀
y)(
¬
¬
Q(x, y)
∨
(
∃
u)R(u, x, y))).
3. Применим правило двойного отрицания:
(
∀
x) (P(x)
∧
(
∀
y)(Q(x, y)
∨
(
∃
u)R(u, x, y))).
4. Переместим кванторы в начало формулы:
(
∀
x)(
∀
y)(
∃
u) (P(x)
∧
(Q(x, y)
∨
R(u, x, y))),
Получим ПНФ.
(
∀
x)(
∀
y)(
∃
u)(P(x)
∧
(Q(x, y)
∨
R(u, x, y))), у которой матрица находится
в КНФ.
Избавимся от кванторов существования в префиксе:
Так как перед (
∃
u) есть (
∀
x),(
∀
y) то переменная u заменяется
двухместной функцией f(x, y). Таким образом, мы получаем следующую
стандартную форму:
(
∀
x)(
∀
y)(P(x)
∧
(Q(x, y)
∨
R(f(x, y), x, y))).
Получим ССФ.
Отбросим кванторы всеобщности и заменим конъюнкцию на
перечисление:
{P(x), (Q(x, y)
∨
R(f(x, y), x, y))}.
Получим множество из двух дизъюнктов.
Пример 3. Получить скулемовскую стандартную форму формулы
(
∀
x)(
∃
y)(
∃
z)((
¬
P(x, y)
∧
Q(x, z))
∨
R(x, y, z)
∧
(
¬
Q(x, z)
∧
P(x, y))).
Сначала сведем матрицу к КНФ:
((
¬
P(x, y)
∨
R(x, y, z ))
∧
(Q(x, z)
∨
R(x, y, z))
∧
(
¬
Q(x, z)
∧
P(x, y))).
Затем избавимся от кванторов существования в префиксе:
Так как перед (
∃
y)(
∃
z) есть (
∀
x), то переменные y, z заменяются
соответственно одноместными функциями f(x), g(x). Таким образом, мы
получаем следующую стандартную форму:
(
∀
x)(((
¬
P(x, f(x))
∨
R(x, f(x), g(x)))
∧
(Q(x, g(x))
∨
R(x, f(x), g(x))
∧
(
¬
Q(x,
g(x))
∧
P(x, f(x)))).
Представим полученную ССФ в виде множества дизъюнктов:

Страницы