Теоретические сведения - polpoz.ru o_O
Главная
Поиск по ключевым словам:
страница 1
Похожие работы
Название работы Кол-во страниц Размер
Краткие теоретические сведения 1 50.63kb.
Группа: бмт1-81 Студент: Абрамова И. В. Краткие теоретические сведения... 1 50.04kb.
Дисциплины автоматизация делопроизводства 1 47.99kb.
Операционная система Linux Теоретические сведения 1 153.65kb.
Конспект урока русского языка Тема: «Имя числительное» (повторительно-обобщающий... 1 54.72kb.
«Логарифмы» дисциплины математика, примеры решения упражнений, набор... 1 109.98kb.
Разработка урока по алгебре и началам математического анализа по... 1 36.28kb.
Теоретические основы электротехники 1 209.02kb.
Перевод (устный и письменный) на протяжении всего курса обучения... 2 292.79kb.
Теоретические основы концепции триады небо-человек-земля (человек-природа-социум) 1 56.79kb.
, «сведения», 1 52.18kb.
1 Íàçíà÷åíèå è îáëàñòü ïðèìåíåíèÿ Таблица №1 1 41.68kb.
1. На доске выписаны n последовательных натуральных чисел 1 46.11kb.

Теоретические сведения - страница №1/1

Лекция № 5


Преобразование формул логики предикатов

в клаузальную форму.

Цель занятия: получить практические навыки преобразования формул исчисления предикатов из стандартной формы в клаузальную.

Теоретические сведения


В логике предикатов, как и в логике высказываний, приведение формул к некоторой нормальной (канонической) форме позволяет упростить алгоритмы проверки их свойств и, в конечном счете, решение проблемы дедукции. Однако в логике предикатов задача приведения к нормальной форме является более сложной вследствие более богатого синтаксиса языка, в частности, из-за наличия квантификаций, свободных и связанных вхождений одной и той же переменной и др.

Преобразование формул логики предикатов из стандартной формы в клаузальную выполняется в три этапа:

1. Преобразование в предваренную форму.

2. Получение замкнутой формы и сколемизация.

3. Преобразование матрицы в КНФ.

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

12...n M,

где символ i означает либо -квантификацию, либо -квантификацию для i=1,...n, а M - матрица. Квантификации в префиксе относятся к различным переменным и их порядок, в общем случае, имеет значение.

Для любой формулы логики предикатов существует логически эквивалентная ей предваренная форма. Алгоритм получения предваренной формы для произвольной формулы логики предикатов включает следующие шаги:

1. Исключение связок импликации и эквивалентности.

2. Переименование (если необходимо) связанных переменных таким образом, чтобы никакая переменная не имела бы одновременно свободных и связанных вхождений. Это должно быть выполнено для всех подформул рассматриваемой формулы.

3. Удаление квантификаций, область действия которых не содержит вхождений квантифицированной переменной.

4. Сужение области действия отрицаний и снятие двойных отрицаний. При этом помимо законов де Моргана и инволюции используются следующие тождества:

(xA) = x(A);

(xA) = x(A).

5. Перенос всех квантификаций в начало формулы. Для этого используются следующие правила:

(xA & xB) = x(A & B);

(xA  xB) = x(A  B);

(xA & B) = x(A & B), если формула B не содержит x;

(xA & B) = x(A & B), если формула B не содержит x.

(xA  B) = x(A  B), если формула B не содержит x;

(xA  B) = x(A  B), если формула B не содержит x.

При выполнении этого шага некоторые связанные переменные могут быть переименованы. Например, формула xP(x) & xQ(x) будет сначала преобразована в xP(x) & yQ(y), после чего применены правила преобразования



Пример. Преобразовать в предваренную форму следующую формулу:

yx(Q(x, y)  P(y))  (R(v) & vzwS(v, z))

Решение.

1. Исключение связок импликации и эквивалентности:

yx(Q(x, y)  P(y))  (R(v) & vzwS(v, z))

2. Переименование.

yx(Q(x, y)  P(y))  (R(v) & uzwS(u, z))

3. Удаление ненужных квантификаций:

yx(Q(x, y)  P(y))  (R(v) & uzS(u, z))

4. Сужение области действия отрицаний и снятие двойных отрицаний:

y(x(Q(x, y)  P(y)))  (R(v) & uzS(u, z))

yx((Q(x, y)  P(y)))  (R(v) & uzS(u, z))

yx(Q(x, y) & P(y))  (R(v) & uzS(u, z))

yx(Q(x, y) & P(y))  (R(v) & uzS(u, z))

5. Перенос квантификаций в начало формулы.

y[x(Q(x, y) & P(y))  R(v) & uzS(u, z)]

yx[Q(x, y) & P(y)  R(v) & uzS(u, z)]

yxu[Q(x, y) & P(y)  R(v) & zS(u, z)]

yxuz[Q(x, y) & P(y)  R(v) & S(u, z)]

Получена предваренная форма.

Предваренная форма в общем случае может содержать свободные переменные. Однако, при анализе выполнимости достаточно оперировать только замкнутыми формулами, т.е. формулами не содержащими свободных переменных. Действительно, если A - формула, содержащая свободные переменные x0, ..., xn, которая (после переименования) не содержит ни одного связанного вхождения этих переменных, то замкнутая формула x1...xnA выполнима тогда и только тогда, когда выполнима формула A. Нàïðèìåð, фîðìóëà yx[Q(x, y) & S(u, z)] после преобразования в замкнутую форму примет вид: uzyx [Q(x, y)& S(u, z)].

Всякой замкнутой формуле A можно поставить в соответствие формулу SA, не содержащую кванторов существования, такую, что формулы A и SA либо обе выполнимы, либо обе невыполнимы. Таким образом, проверка невыполнимости формулы A может быть сведена к проверке невыполнимости формулы SA. Форма SA называется сколемовской формой. Алгоритм получения сколемовской формы (сколемизация) из замкнутой предваренной формы включает следующие шаги:

1. Сопоставить каждой -квантифицированной переменной список предшествующих ей в префиксе -квантифицированных переменных и некоторый функциональный символ, местность которого равна мощности полученного списка.

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

3. Удалить из формулы все -квантификации.

Сколемизируем формулу в предваренной форме, полученную в рассмотренном выше примере:

yxuz[Q(x, y) & P(y)  R(v) & S(u, z)]

1.Поставим в соответствие каждой -квантифицированной переменной функциональную форму от предшествующих ей в префиксе -квантифицированных переменных:

x - f(y);

z - g(y, u).

2. Подставим в формулу функциональные формы:

yxuz[Q(f(y), y)&P(y)  R(v)&S(u, g(y, u))].

3. Удалим -квантификации:

yu[Q(f(y), y)&P(y)  R(v)&S(u, g(y, u))].

Получили сколемовскую форму.

Таким образом, сколемовская форма - это замкнутая предваренная форма, префикс которой содержит только -квантификации. Клаузальная форма - это сколемовская форма, матрица которой является КНФ. Преобразование матрицы в КНФ выполняется так же, как и в логике предикатов. Для нашего примера после применения правил дистрибутивности получим следующую клаузальную форму:

yu[(Q(f(y), y)R(v)) & (Q(f(y), y)S(u, g(y, u))) & (P(y)R(v)) & (P(y) S(u, g(y, u)))].

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



{(Q(f(y),y)R(v)), (Q(f(y),y)S(u,g(y,u))), (P(y)R(v)), (P(y)S(u,g(y,u))}.

Для доказательства невыполнимостьи этого множества можно использовать метод резолюций.


izumzum.ru