Предваренные (пренексные) нормальные формы исчисления предикатов.

Теоремы о логическом следствии

Определение 18. Выводом формулы G из формул U₁, U₂,…, U_n называется последовательность формул F₁, F₂,…, F_n такая, что F_m есть G, а любая F_i либо аксиома, либо одна из формул U_i , либо формула, непосредственно выводимая из предшествующих ей формул.

Вследствие законов ассоциативности скобки в выражениях, связанных отношениями дизъюнкции и конъюнкции могут быть опущены, при этом выражение F₁ Ъ F₂ Ъ…Ъ F_n называется дизъюнкцией формул F₁, F₂,…, F_n, а выражение F₁ Щ F₂ Щ…Щ F_n называется конъюнкцией формул F₁, F₂,…, F_n.

Теорема 1. Пусть даны формулы F₁, F₂,…, F_n и формула G. G есть логическое следствие F₁, F₂,…, F_n тогда и только тогда, когда формула ((F₁ Щ F₂ Щ…Щ F_n)®G) общезначима.

Теорема 2. Пусть даны формулы F₁, F₂,…, F_n и формула G. G есть логическое следствие F₁, F₂,…, F_n тогда и только тогда, когда формула (F₁ Щ F₂ Щ…Щ F_n ЩШG) противоречива.

Замечание.

Для того чтобы доказать, что данная формула является тавтологией, достаточно доказать, что ее отрицание является противоречием:

Ш((F₁ Щ F₂ Щ…Щ F_n)®G)=

Ш(Ш(F₁ Щ F₂ Щ…Щ F_n) Ъ G)=

(F₁ Щ F₂ Щ…Щ F_n) Щ ШG).

Теоремы 1 и 2 очень важны. Из них следует, что доказательство логического следствия одной формулы из конечного множества формул эквивалентно доказательству того факта, что некоторая связанная с конечным множеством формула общезначима или противоречива.

Определение 19. Литерал (литера) есть атом или отрицание атома.

Определение 20.Формула F находится в конъюнктивной нормальной форме тогда и только тогда, когда F имеет вид: F₁ Щ F₂ Щ…Щ F_n, n >=1, где каждая из F₁, F₂,…, F_n есть дизъюнкция литералов.

Определение 21. Формула F находится в дизъюнктивной нормальной форме тогда и только тогда, когда F имеет вид: F₁ Ъ F₂ Ъ…Ъ F_n, n >=1, где каждая из F₁, F₂,…, F_n есть конъюнкция литералов.

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

Определение 22: Формула F логики предикатов находится в предваренной нормальной форме, тогда и только тогда, когда формула F имеет вид:

(K₁x₁)…(K_nx_n) (M), где каждое (K_ix_i), i = 1,…,n, есть или ("x_i) или ($x_i), и M есть формула, не содержащая кванторов. (K₁x₁)…(K_nx_n) называется префиксом, а M – матрицей формулы F.

Алгоритм преобразования формул в ПНФ.

Шаг 1. Используем законы законы 1 и 2 исчисления высказываний для того, чтобы исключить логические связки импликации и эквивалентности.

Шаг 2. Многократно используем закон двойного отрицания, законы де Моргана и законы 5 и 6 исчисления предикатов, чтобы внести знак отрицания внутрь формулы.

Шаг 3. Переименовываем связанные переменные, если это необходимо.

Шаг 4. Используем законы 1, 2, 3, 4, 7,8, 9 и 10 до тех пор, пока все кванторы не будут вынесены в самое начало формулы, чтобы получить ПНФ.

Пример 6. Приведем формулу ("x) P(x) ® ($x) Q(x) к ПНФ:

("x) P(x) ® ($x) Q(x)=Ш(("x) P(x))Ъ ($x) Q(x)(по закону 1 логики высказываний)

=($ x)( Ш P(x)) Ъ ($ x) ) Q(x)( по закону 5 логики предикатов)

=($ x)( Ш P(x) Ъ Q(x))( по закону 8 логики предикатов), что и есть ПНФ исходной формулы.

Пример 7. Привести формулу ("x) ("y)(($z)(P(x, z)Ù P(y, z))® ($u) Q(x, y, u)) в ПНФ:

("x) ("y)(($z)(P(x, z)Ù P(y, z))® ($u) Q(x, y, u))

= ("x) ("y)(Ø(($z)(P(x, z)Ù P(y, z))) Ú ($u) Q(x, y, u))(исключаем ®)

=("x) ("y)(("z) (Ø P(x, z) Ú Ø P(y, z)) Ú ($u) Q(x, y, u))(по закону 6 законам де Моргана)

= ("x)("y)("z)($u) (Ø P(x, z) Ú Ø P(y, z)) Ú Q(x, y, u))(закон 3)