л = -.[(CfeX = -.S)fe--i-,C].

Следовательно,

Ищем дизъюнкты:

{Chx = В) = {С VXV -пВ), (С) = С. Таким образом,

Ar = {(-,CV--iX VS),C}. Резольвента для (-.С V -Х V и С - это (-.X V -iS). Поэтому

АГ = {(С V -.X V -.В), С, (Х V

Процесс останавливается. Пустой резольвенты нет. Формула -iC не является логическим следствием формулы {СХ = -iS).

1.3.2. Метод резолюций в логике предикатов

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

Еош формула Л не содержит предикатов и знаков операций (функций), то фактически имеем формулу исчисления высказываний, поскольку предикаты можно рассматривать как пропозициональные переменные. Следовательно, метод резолюций не требует существенных изменений. В случае, если формула А содержит кванторы, то ее надо привести к предваренной форме (§1.2.5), а затем устранить кванторы, вводя сколемовские функции. Появятся, естественно, при этом знаки операций (функций). Затем полученную формулу приводят к конъюнктивной нормальной форме и ищут резольвенты для дизъюнктов.

Что делать, если два контрарных литерала, в данном случае они имеют вид Р{..) и ~iP(..), содержат два разных терма? Например, Vi=Viy Р(а, х) и Vj = Vj V ~.Р(о, /(b)). В этом случае проводят их унификацию, т.е. замену термов. В нашем примере она имеет вид:1:

Vi<x\f{h) >=ЩуР{а,х)\ < x\f{b) >= Vi < x\f{b) > VP(a, /(b)),

Сиыволическая запись

.A(ti) <tit3 > означает замену в формуле Л терма ti на терм ta.

2?у < x\f{b) >= Щу~.Р(а,т)\ < х\т >=

= Vj<x\f{h)>y~.P{a,m).

Далее ищется резольвента:

V\<x\f{h)>\J Vr <x\f{b)>-

CфopмyJшpyeм более строго правила замены термов и понятие унификации.

Замена - это пара вида < x\t >, где х - переменная, at - терм. Применение замены < x\t > к терму to, входящему в некоторую формулу, определяется индуктивно:

• X < x\t >= t, если X - переменная;

• а < x\t >= а, если а - константа (фиксированный объект из М при интерпретации

• f{h,...,tn) <x\t >= f{h <x\t >,...,tn < x\t >).

Таким образом, унификация двух последовательностей термов tl,tn li Tl,Тп - это замена < x\t > такая, что

ti < x\t >= Тг < x\t > (г = \,...п).

Резольвента для дизъюнктов T>i = Vi \J P{ti), Vi = Vi \J ~iP{t2) ищется с помощью унификации термов ti, fa:

V, <x\t>\/ Vj < x\t >

Пример 1.5. Имеем два дизъюнкта

t>i=p{z)vr{x), v2 = ~np{f{x)) v q{y). Очевидна замена

Г>1 < z\f{x) >= lp{z) V -.r{x)] < z\f{x) >= F(/(x)) V -Я(х), Pa < z\f{x) >= hF(/(x)) V q{y)] < z\f{x) >= -F(/(x)) V q{y). Тогда резольвента для t>i и т>2 есть дизъюнкт -r{x) V q{y)-Пример 1.6. Для дизъюнктов

Di=p{f{x))vr{x), Г>2 = -F(g(x)) V q{y)

нет унификации.

Глава 2

Формальные теории (исчисления)

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

Формальная теория - это игра со знаками, игра со словами и предложениями, составленными из знаков. При этом имеется в виду, что правила составления слов из знаков и правила игры со словами и предложениями заранее оговорены, точно и строго прописаны. В основе формальной теории - язык, на котором «разговаривает теория». На первое место выходит синтаксис этого языка, т.е. способ построения формул, в противопоставление семантике.

Синтаксис [< гр. syntajcis составление] - 1) характерные для конкретных языков средства и правила создания речевых единиц; 2) раздел грамматики, изучающий способы соединения слов в словосочетания и предложения, соединение предложений в сложные предложения 140].

Семантика [< гр. semanticos обозначающий] - 1) смысловая сторона единиц языка, словосочетаний; 2) раздел логики, исследующий отношения логических знаков к понятиям и предметам действительности [40].