Недетерминированный алгоритм решения множества уравнений

Вход: множество уравнений .

Выход: множество уравнений в разрешённой форме .

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

Начало цикла:

I. если существует уравнение вида: t = x, где t – не переменная, а x – переменная, то заменить это уравнение на x = t; в противном случае

II. если существует уравнение вида: x = x, где x – переменная, то удалить это уравнение из системы уравнений; в противном случае

III. если существует уравнение вида: s = t, в котором s и t не являются переменными, то если корневые функции термов s и t различны, тогда возвращается «отказ», в противном случае осуществить преобразование редукции термов;

IV. если существует уравнение вида: x = t, такое, что переменная x не входит в другие уравнения системы и терм t отличен от x, то если переменная x входит в t, тогда возвращается «отказ», в противном случае осуществить преобразование элиминации переменной.

Конец цикла. (Возвращается «успех», преобразованная система уравнений будет искомым унификатором.)

Здесь под элиминацией переменной понимается переход от системы уравнений к системе, полученной после подстановки x = t.

Пример

Рассмотрим систему, состоящую из одного уравнения:

((a Ç b) È d) È (a Ç b) = (c È (a Ç b) È (a Ç b)}

1) Применяем случай III, делаем редукцию, получаем: h = {(a Ç b) È d) = c È (a Ç b), a Ç b = a Ç b}.

2) Применяем случай III, получаем: h = {a Ç b = с, d = a Ç b, a Ç b = a Ç b}.

3) Применяем случай III для последнего уравнения и повторяем 2 раза случай II, это приводит к h = {a Ç b = с, d = a Ç b}.

4) Применяем случай I, получаем ответ: h = {c = a Ç b, d = a Ç b}.

Предикаты и отношения

Функция n переменных, принимающая значения 0 и 1, называется n-местным предикатом. Каждому отношению соответствует предикат, равный характеристической функции подмножества R. Ясно, что определение n-местного предиката на множестве А равносильно заданию отношения:

Пусть и – предикаты. Конъюнкцией P и Q называется предикат , дизъюнкцией – предикат , отрицание определяется с помощью предиката .

Для предикатов определяются кванторы существования и всеобщности. Пусть – n-местный предикат. Запись: означает, что существует , для которого =1, запись: означает, что =1 для всех . Аналогично определяются предикаты и , при . В этих случая говорят, что переменная связана квантором. Предикаты и будут зависеть от n-1 переменных. В случае, когда , положим и . Тем самым мы определим предикаты и для любых символов переменных x. Отношение, соответствующее предикату будет проекцией отношения, определяемого P, на область , оно будет равно объединению по всем aÎA отношений, определяемых предикатами . Предикату соответствует отношение, равное пересечению этих отношений. Таким образом,

;

.

Язык логики предикатов

Определим синтаксис языка первого порядка. Алфавит языка первого порядка состоит из логических символов Ú, Ø, $, =, из символов переменных и из нелогических символов. К логическим символам отнесём символы скобок и запятой. В качестве символов переменных будем использовать также x, y, z, u, v и т.д. Логические символы одинаковы для всех языков первого порядка. Нелогическими называются символы операций, символы предикатов и символы констант. Язык первого порядка L задаётся как множество нелогических символов. Если L = Æ, то L называется языком чистого равенства.

Каждому s Î L ставится в соответствие #(s) Î w. Если s – константа, то #(s) = 0. Если R – символ предиката, такого, что #(R) = n, то R называется символом n-местного предиката. Если f – символ операции, и #(f) = n, то f называется символом n-арной операции. Для предикатов и операций число #(R) (соответственно #(f)) больше 0, и оно называется местностью (соответственно арностью). Объединение множеств символов операций и констант составляет множество функциональных символов, позволяющее строить термы языка L на множестве .

К предикатам языка L мы всегда относим бинарный предикат (равенство). Определим формулы языка L.

Атомной формулой языка L называется выражение вида: , где – термы языка L, а R Î L – символ n-местного предиката. В частности, выражение будет атомарной формулой для любых термов языка L. Множество всех формул языка L определяется как наименьшее множество выражений, которое содержит все атомные формулы и удовлетворяет условиям: если q и y – формулы, а x – переменная, то выражения , Øq, $xq – формулы. Формулы q и y называются подформулами формулы , формула q – подформулой формул Øq и $xq.

Будем предполагать, что другие логические связки служат сокращениям:

(q & y) для Ø(Øq Ú Øy),

(q ® y) для (Øq Ú y),

" x q для Ø$ x Øq.

Формула Øx = y обычно записывается как x ¹ y. Примеры формул:

" x $ y P (x, y, x È z), $ x (y £ x ® y = x).

Замена переменных

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

" y (y = z) ® $ z (z < x)

первое вхождение переменной z свободно, а второе – связанное. Переменная x является свободной, а y – связанной. Формальное определение свободных и связанных переменных следующее:

1) все вхождения переменных в атомных формулах свободны;

2) свободные вхождения x в Øq есть в точности свободные вхождения x в q;

3) свободные вхождения x в состоят из свободных вхождений x в q и свободных вхождений x в y;

4) если x и y – различные переменные, то свободные вхождения x в формулу
$ y q соответствуют свободным вхождениям x в формулу q;

5) в формуле $ x q нет свободных вхождений переменной x.

Запись: q(x) указывает на то, что формула q содержит свободные вхождения переменной x. Если c – символ константы, то q(с) означает формулу, полученную заменой всех свободных вхождений x в q на с. Например, если q(x) = $y((y = x) & " x (x = y)), то q(c) = $y((y = c) & " x (x = y).

Мы пишем: для указания того, что q содержит свободные переменные среди . Применяется запись: для обозначения формулы, в которой все свободные вхождения каждой из переменных формулы q заменяются на терм , . Таким образом, q(с) является сокращением обозначения q(х/с).

Формула, не содержащая свободных переменных, называется предложением.

Может случиться, что при замене переменной термом нарушается очевидный принцип, согласно которому замена переменной в равных формулах даёт равные формулы. Например, пусть t = f(y), q(z) = $y(y < z). Тогда после замены получаем: . С другой стороны, q(z) = $x(x < z), и, значит, . Получаем не равные формулы. Поэтому перед подстановкой терма в формулу q(х) связанные переменные, содержащиеся в будем переименовывать на символы, не встречающиеся в .

Другой выход следующий: терм t называется свободным для переменной x в формуле q(х), если никакое свободное вхождение x в q не лежит в области действия кванторов и , где входит в t. В этом случае замена q(х/t) допускается.

При подстановках констант противоречия не возникают.

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

Исчисление предикатов

Для того чтобы определить формальную теорию, связанную с языком первого порядка, введём логические аксиомы и правила вывода языка L. Логические аксиомы подразделяются на 3 группы:

1) Аксиомы предложений: всякая формула q языка L, которая может быт получена из некоторой тавтологии исчисления высказываний K (описанного в разд. 3 с помощью аксиом К1 – К10) в результате подстановки формул языка L на место высказывательных символов, есть логическая аксиома языка L. Всякая такая формула называется тавтологией языка первого порядка L.

2) Аксиомы кванторов

· если q и y – формулы языка L, то имеют место следующие аксиомы:

("x (q ® y)) ® (q ® "x y), если х не входит свободно в q;

("x (q ® y)) ® (($ x q) ® y), если х не входит свободно в y;

· для каждой формулы q(х) и терма t, свободного для x, имеют место кванторные аксиомы:

" х q(х) ® q(t);

q(t) ® $ х q(х).

3) Аксиомы равенства

t = t для любого терма t;

(t = s) & q(t) ® q(s), для любых формул q(х) и термов s, t, для которых х свободна в q, а s и t свободны для х (здесь q(t) означает формулу q(x/t)).

Правила вывода

(MP) Из формул q и q ® y выводится y (Modus Ponens).

(Gen) Из формулы q выводится " x q (правило обобщения).

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

Запись: å q означает, что существует вывод формулы q из логических аксиом и формул из множества å. Если Æ q, то q – теорема исчисления предикатов L. Множество å называется противоречивым, если для каждой формулы q языка L существует вывод: å q. В противном случае å называется непротиворечивым. Предложение q называется непротиворечивым, если множество {q} непротиворечиво. Множество формул å называется максимально непротиворечивым, если оно не является собственным подмножеством некоторого непротиворечивого множества.

Легко доказать следующие свойства непротиворечивых множеств:

1) Множество å непротиворечиво, если и только если каждое его конечное подмножество непротиворечиво.

2) Пусть q – предложение. Тогда множество å È {q} противоречиво, если и только если å Øq.

3) Пусть å – максимально непротиворечивое множество. Тогда для любых предложений q и y имеет место:

(i) å q, если и только если q Î å;

(ii) q Ï å, если и только если Øq Î å;

(iii) (q & y) Î å, если и только если q Î å и y Î å;

4) Каждое непротиворечивое множество предложений содержится в некотором максимальном непротиворечивом множестве предложений.

Теорема (о непротиворечивости исчисления предикатов). Нет формул q исчисления предикатов L, для которых существуют выводы: q и Øq.

Доказательство. Каждой формуле q поставим в соответствие формулу h(q) исчисления высказываний K, множество символов P которого состоит из предикатов RÎL. Формулу h(q) определим по индукции:

1) для атомных формул;

2) , ,

,

, для любых формул ;

3) h("xq) = h(q), h($xq) = h(q).

Для всякой логической аксиомы q формула h(q) будет тавтологией в K. Если бы для некоторой формулы q существовали выводы q и Øq, то формулы h(q) и Øh(q) были бы тавтологиями в исчислении высказываний. Поскольку исчисление высказываний непротиворечиво, это невозможно. Стало быть, нет формул q, для которых существуют выводы: q и Øq.