План лекций (очень подробный), страница 5

f(xj1,...,xjm), где f - новый m-местный функциональный символ; и т.д.

для всех кванторов существования (в произвольном порядке).

Т13. Если a - формула в пнф, а b - соответствующая ей формула в

снф, то формулы a и b одновременно невыполнимы. Д.: показывается, что

формулы a и b одновременно имеют модель: это следует из соответствия

между семантикой квантора существования, которому предшествуют кванто-

ры общности по переменным xj1,...,xjm и всюду определенной функции

f(xj1,...,xjm).

Ключевые слова к $5: эквивалентность (рефлекcивность, симметрич-

ность, транзитивность); собственно эквивалентность; одновременная об-

щезначимость; противоречивость=невыполнимость; одновременная невыпол-

нимость; конъюнктивная/предваренная/скулемовская нормальные формы;

$6. Метод резолюций (r-метод).

Метод резолюций - это машинно-ориентированный метод установления

общезначимости формул: составляющие его преобразования просты и не

требуют "творчества", но зато лишены сколько-нибудь ясного содержа-

тельного смысла (в противоположность натуральному выводу, моделирующе-

му содержательное доказательство: см. таблицу).

і Методы доказательства і n і g і r і

Г———————————————————————Е————Е————Е————ґ

і Содержательный смысл і ++ і +- і -- і

Г———————————————————————Е————Е————Е————ґ

і Простота действий і -- і +- і ++ і

Метод резолюций можно рассматривать как доказательство общезначи-

мости "от противного": отрицание рассматриваемой (замкнутой) формулы

приводится к противоречию.

Т14. Замкнутая формула общезначима тогда и только тогда, когда ее

отрицание невыполнимо. Д.: следует из определений.

Замечание. Для незамкнутых формул Т14 не верна.

Метод резолюций существенно опирается на эквивалентные преобразо-

вания: формула a, общезначимость которой следует установить, замыкает-

ся кванторами общности; отрицание полученной формулы приводится снача-

ла к предваренной нормальной форме, а затем к скулемовской нормальной

форме, в то время как бескванторная часть формулы приводится к конъюн-

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

ется в виде множества этих дизъюнктов. К этому множеству добавляются

новые дизъюнкты, получаемые по r-правилам (правилам метода резолюций)

из уже существующих. Вывод заканчивается, когда удается получить "пус-

той" дизъюнкт (состоящий из 0 литер и эквивалентный Б). В таком случае

формула a называется r-выводимой (|-r a). Для упрощения вида r-правил

используется представление дизъюнкта в виде множества литер, например,

a(x)vїb(a)vїb(a) ---> {a(x),їb(a)}. Подстановкой называется множество

б = {x1:=t1,...,xn:=tn}; aб означает результат одновременной замены

в выражении a переменных x1,...,xn на термы t1,...,tn (a может быть

термом, бескванторной формулой, множеством литер). Подстановка б, та-

кая что aб = bб, называется унификатором выражений a и b, а процесс

построения такой подстановки - унификацией.

Пусть С1, С2 - множества литер. r-правила:

r1. С1/c1б;

r2. c1; c2 / (c1-{l1})u(c2-{l2}), если l1 и l2 - контрарная пара

литер (одна литера - атом, а другая - отрицание этого атома); дизъ-

юнкт, получаемый в результате применения этого правила, называется ре-

зольвентой дизъюнктов С1 и С2.

Замечание. Применение правила r1 позволяет выполнить: 1) перео-

бозначение переменных в дизъюнкте; 2) склейку нескольких литер дизъюн-

кта в одну, например, a(x)va(a){x:=a} / a(a); 3) унификацию атомов из

разных дизъюнктов с целью получения контрарной пары литер l1 и l2 для

последующего применения правила r2.

t15. Метод резолюций корректен (|-r a => |=a). Д. По Т8-14 форму-

ла a общезначима <=> соответствующее множество дизъюнктов В1 невыпол-

нимо; дальше применениями r-правил выполняется преобразование

В1->b2->...->bm, причем bm содержит Б, так что отношение bm|=Б выпол-

нено. Поскольку r-правила сохраняют невыполнимость, Вi|=Б <=> bi+1|=Б.

Т16. Метод резолюций полон (|=a => |-r a). Д. Пусть a - замкнутая

формула и |=a. Тогда їa эквивалентна некоторой формуле b в снф и кнф,

причем b|=Б, |=їb и существует g-вывод формулы їb. "Разбирая" этот вы-

вод (удаляя из него контрарные пары), построим вывод пустого дизъюнкта

по r-правилам.

Ключевые слова к $6: метод резолюций=r-метод; унификатор=унифици-

рующая подстановка, унификация; множество дизъюнктов, множество литер,

контрарная пара.

$7. Эрбрановские интерпретации.

Логику высказываний (ЛВ) можно рассматривать как частный случай

логики предикатов (ЛП): в ЛВ все предикаты 0-местные и, следовательно,

могут принимать только одно истинностное значение (истина/ложь) в каж-

дой данной интерпретации. Поэтому с точки зрения ЛВ неразличимы мно-

жества, на которых строятся интерпретации, и можно (условно) считать,

что всегда рассматривается одно и то же множество, а разные интерпре-

тации отличаются друг от друга истинностными значениями 0-местных пре-

дикатов. Следовательно, множество всех интерпретаций формулы ЛВ конеч-

но и ее общезначимость может быть установлена полным перебором (пост-

роением истинностной таблицы), т.е. безо всякого логического вывода. В

ЛП понятие общезначимости учитывает различные (в том числе бесконеч-

ные) множества, и на них по-разному интерпретируются не только преди-

каты, но и функции. Но использование эрбрановских интерпретаций (ЭИ)

позволяет упростить эту ситуацию (см. таблицу).

Интерпретация: і множество і функции і предикаты і

———————————————Е—————————————Е—————————— ———Е————————————ґ

ЛВ і одно і нет і интерпрет. і

і (условное) і і по-разному і

———————————————Е—————————————Е—————————— ———Е————————————ґ

ЛП і много і интерпрет. і интерпрет. і

і і по-разному і по-разному і

———————————————Е—————————————Е—————————— ———Е————————————ґ

ЛП і одно і интерпрет. і интерпрет. і

с учетом ЭИ і і одинаково і по-разному і

———————————————Б—————————————Б—————————— ———Б————————————Щ

ЭИ - это интерпретация формулы на множестве, называемом ее эрбра-

новским универсумом, и именно, множестве всех термов, которые можно

построить из констант и функций данной формулы (если нет констант,

фиксируется какая-либо произвольная); такие термы называются основны-

ми. Функции интерпретируются так, чтобы значением каждого терма был он

сам. Предикаты интерпретируются как истинностные функции на множестве

термов. Основное свойство эрбрановской интерпретации: в ней истинност-

ное значение любой атомарной формулы без переменных p(t1,...,tn) сов-

падает с p^('t1',...,'tn'), где 't1',...,'tn' - элементы эрбрановского

универсума. Эрбрановский базис формулы - это множество всех атомарных

формул, которые можно построить из предикатов этой формулы и термов ее

эрбрановского универсума; такие атомы называются основными. Каждую ЭИ

можно задать как подмножество эрбрановского базиса (атомарная формула

истинна в данной ЭИ <=> принадлежит подмножеству). Основной пример

дизъюнкта С - это дизъюнкт Сб, где б - подстановка термов из эрбра-