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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

9
Алгоритм преобразования формулы в ПНФ известен. При помощи
законов эквивалентных преобразований логики высказываний можно свести
матрицу к КНФ.
Алгоритм преобразования формул в ДНФ и КНФ.
Шаг 1. Используем законы эквивалентных преобразований исчисления
высказываний для того, чтобы исключить логические связки импликации и
эквивалентности.
Шаг 2. Многократно используем закон двойного отрицания, и законы
де Моргана, чтобы внести знак отрицания внутрь формулы.
Шаг 3. Несколько раз используем дистрибутивные законы и другие
законы, чтобы получить НФ.
Алгоритм преобразования формулы (K
1
x
1
)…(K
n
x
n
) (M), где каждое
(K
i
x
i
), i = 1,…,n, есть или (
∀
x
i
) или (
∃
x
i
), и M есть КНФ в скулемовскую
нормальную форму (СНФ) приведен ниже.
Алгоритм преобразования ПНФ в ССФ.
Шаг 1. Представим формулу в ПНФ (K
1
x
1
)…(K
n
x
n
) (M), где M есть
КНФ. Пусть K
r
есть квантор существования в префиксе (K
1
x
1
)…(K
n
x
n
),
1<=r<=n.
Шаг 2. Если никакой квантор всеобщности не стоит левее K
r
– выберем
новую константу c, отличную от других констант, входящих в M, заменим
все x
r
в M на c и вычеркнем K
r
x
r
из префикса. Если K
1
,…K
i
– список всех
кванторов всеобщности, встречающихся в M левее K
r
, 1< i<r, выберем
новый i –местный функциональный символ f, отличный от других
функциональных символов, заменим все x
r
в M на f(x
1
, x
2
,…x
i
) и вычеркнем
K
r
x
r
из префикса.
Шаг 3. Применим шаг 2 для всех кванторов существования в префиксе.
Последняя из полученных формул есть скулемовская стандартная форма
формулы. Константы и функции, используемые для замены переменных
квантора существования, называются скулемовскими функциями.
Пример 1. Получить ССФ для формулы (
∃
x)(
∀
y)(
∀
z)(
∃
u)(
∀
v)(
∃
w) (P(x, y,
z, u, v, w).
В этой формуле левее (
∃
x) нет никаких кванторов всеобщности, левее
(
∃
u) стоят (
∀
y) и (
∀
z), а левее (
∃
w) стоят (
∀
y), (
∀
z) и (
∀
v).
Следовательно, мы заменим переменную x на константу a, переменную
u - на двухместную f(y, z), переменную w - на трехместную функцию
g(y, z, v). Таким образом, мы получаем следующую стандартную форму
написанной выше формулы:
(
∀
y)(
∀
z)(
∀
v)(P(a, y, z, f(y, z), g(y, z, v)).
Определение 1: Дизъюнктом называется дизъюнкция литералов.
Дизъюнкт, содержащий r литералов, называется r- литеральным
дизъюнктом. Однолитеральный дизъюнкт называется единичным
дизъюнктом. Если дизъюнкт не содержит никаких литералов, то он

Страницы