Исчисление высказываний. Непротиворечивость и полнота.

Например, в качестве языка возьмем любые последовательности символов @, единственной аксиомой

объявим один символ @, а правило вывода будет @ ½¾ @@.

Тогда в данной теории будет выводима любая последовательность из одного или более символов @.

Одно плохо, толку в таких теориях обычно никакого нет…

А вот рассмотренная ранее аксиоматическая теория исчисления высказываний имеет ряд важных

(интересных, замечательных) свойств. Формулы этой теории можно интерпретировать как формулы

Алгебры высказываний, записанные с использованием (функционально полного набора!) операций:

Ø и ® (отрицания и импликации). Для этой теории доказано, что она полна.То есть в этой теории могут

быть выведены все тавтологии логики высказываний (которые могут быть записаны с помощью Ø и ®).

Более того, данная теория непротиворечива. То есть в этой теории не могут быть выведены какая-то

Формула Ф и ее отрицание (ØФ).

Докажем непротиворечивость этой теории.

Прямой проверкой доказывается, что все аксиомы, получаемые из схем аксиом, являются тавтологиями.

Например, для первой схемы аксиом:

А ® (В ® А)

А	В	Ф

А из тавтологий с помощью m.p. ( A , A ® B ½¾ B ) можно получить только тавтологии. А поскольку любая

полученная в этой теории формула Ф есть тавтология,

то ее отрицание ØФ было бы противоречием, которое не выводимо.

Полнота и непротиворечивость очень важные свойства. Увы, большинство более сложных

аксиоматических теорий не может похвастаться полнотой (открытый Геделем принцип неполноты). В них

могут существовать формулы, для которых невозможно доказать как выводимость, так и невыводимость…

Что же касается непротиворечивости, то это очень жесткое требование.

Стоит допустить в теории возможность хотя бы одного противоречия (для одной формулы Ф допустит

возможность вывода и ØФ), как теория становится бессмысленной, так как тогда в ней можно вывести

любую формулу. (Из ложной посылки может следовать что угодно).

11. Лемма |- А->A

Лемма: ½¾ A ® A

Ф1: Возьмем схему аксиом 2 и подставим А = А, С = А, В = А ® А, в результате получим:

(A ® ((A ® A) ® A)) ® ((A ® (A ® A)) ® (A ® A))

Ф2 : Из схемы аксиом 1, при А = А, В = А ® А, получим :

(А ® ((А ® А) ® А))

из Ф1,Ф2 по m.p. получаем Ф3: (A ® (A ® A)) ® (A ® A)

Ф4 : Из схемы аксиом 1, при А = А, В = А, получим:

(А ® (А ® А))

из Ф3, Ф4 по m.p. получаем Ф5: A ® A

Теорема дедукции.

(|- знак «выводимо», Г – множество гипотез, А - гипотеза,

индексы в [ ]- подстрочные индексы, в шпорах так написано чтобы видно было)

Если из A |- B, то |- А->B.

Если из Г, А |- B, Г |- A->B.

Теорема доказывается индукцией по длине вывода. Выводом (в данной теории) называется

последовательность формул Ф[1],...,Ф[i],...,Ф[J],...,Ф[k] где каждая следующая формула является аксиомой,

или гипотезой, или следует по правилу вывода из предыдущих. Ф[1]: Ф[1]->(А-> Ф[1]),

Ф[1]

A->Ф[1]; A|- Ф[1] => |- A-> Ф[1], если Ф[1]=А |- A->A;

A |- A => |- A->A. 2-ой шаг: пусть эта теорема справедлива для всех выводов, J<K, докажем, что она

справедлива для вывода длиной K. Ф[k] - аксиома или гипотеза. Ф[k] в выводе может оказаться функцией.

Если она совпадает с гипотезой или следует по правилу вывода из предыдущих формул первые три случая

доказываются аналогично первому. Если Ф[k] выводится по МР(модус поненс) из Ф[i] и Ф[J]: Ф[i],

Ф[i]= Ф[i] -> Ф[k].

Вывод: поскольку Ф[i] и Ф[k] – функции, которые были выведены раньше, то по МР

|- A -> Ф[i], |- A -> (Ф[i]-> Ф[k])

A -> (Ф[i] -> Ф[k]) -> ((A -> Ф[i]) -> (A -> Ф[k]) => A -> Ф[k]

Вывод:из предположения, что А |- Ф[k]=> |- A -> Ф[k]

Пример:доказать спомощью дедукции принцип силлогизма(S): A ->B, B -> C |- A -> C

A ->(B ->C), B |- A ->C, A -> (B ->C), B |- по МР => B ->C;

A -> (B-> C), B |- A ->C.

Следствие: А ->В; B ->C |- A->C A ; А ->В; B ->C|- A->C A ; А ->В; B; B ->C|- C

C |- A->C

Система Генцена

В ее основе лежит понятие секвенции.

Секвенции имеют вид

антецедент - A₁, A₂, ... A_{n ½¾} B₁, B₂, ... B_n - сукцедент

Содержательно это равносильно выражению:

A₁ & A₂& ...& A_n ® B₁Ú B₂Ú ...Ú B_n

Аксиома (схема аксиом) в системе Генцена единственная и она имеет вид:

A½¾ A

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

(Из секвенций над чертой выводимы секвенции под чертой, а Г обозначает какое-то множество формул).

1) A, Г½¾ В 1)¢ Г½¾ A; Г½¾ А® В

Г½¾ А®B Г½¾ В

2) Г½¾ А; Г½¾ B 2)¢ Г½¾ А&В

Г½¾ А & В Г½¾ А

3) Г½¾ А 3)¢ Г, A½¾ B; Г, С½¾ B; Г½¾ A Ú В

Г½¾ A Ú B Г½¾ В

4) Г, А½¾ 4)¢ Г½¾ А; Г½¾ А

Г½¾ А Г½¾

5) Г, A, B½¾ C

Г, B, A½¾ C

6) A, A½¾ B 6)¢ A½¾ B, B

A½¾ B A½¾ B

7) Г½¾ B 7)¢ Г½¾ A

Г, A½¾ B Г½¾ A, B

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

Задаем язык

а) Символы:

-служебные ->, ⌐, (, ), V, Ǝ

-вещественные переменные х,у, z

-вещественные const a,b,c

- функциональныеые символы f; g; h

-предикатные символы R; Q;P

б)Термы

const или переменные – терм

t1,……..,tm f(t1,……..,tm)

в)Формулы t1,……..,tn , P(t1,……..,tn) – формула A,B, ⌐A, (A), A->B, VxA, ƎxB

Аксиомы

1. А->(B->A)

2. (A->(B->ℓ)) ->((A->B) ->(A->ℓ))

3. (⌐B->⌐A) ->((⌐B->A) ->B)

4.VxA(x) ->A(t)

5.A(t) ->ƎxA(x)

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

1. A; A->B_½¾B

2. B->A(x)_½¾B->VxA(x)

3.A(x)

Терм t называется свободным для переменной х в формуле А, если никакое свободное вхождение

переменной х в формулу А не лежит в области действия от такого квант. переменной у, входящей в терм t

Примеры:

1.y св. х в Р(х)

У несв. х в VyP(x) нарушается статус переменной у

VyP(у)

2.f(x,z) св. x VyP(x,y) ->Q(x)

ƎzVyP(x,y) -> Q(x)

15. Метод резолюции.

Метод резолюций - аксиоматическая теория первого порядка, которая использует доказательство от

противного, и, следовательно, не использует аксиоматику исчисления предикатов (которая находится в

области тождественно истинных формул).

1. Язык метода резолюции - язык дизъюнктов :

2. Аксиомы только собственные.

3. Правило вывода - резолюция

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

Традиционный силлогизм: A ® B, B ® C ½¾ A ® C

Применительно к дизъюнктивной записи можно представить как

A Ú B A Ú B Ú D

B Ú C или "обобщенный" вариант B Ú C Ú E

A Ú C A Ú C Ú D Ú E

Унификация: Унификация также не противоречит здравому смыслу. Она позволяет заменить переменную х

на терм t. То есть вместо переменной могут быть подставлены константа или другая переменная (из той же

области), или функция, область значений которой совпадает с областью определения х.

a(const)®xy(из той же области)

­

f(z)

Вывод здесь заключается в том, что в систему добавляется отрицание формулы (дизъюнкта!), которую

необходимо вывести. Вывод состоит в последовательном применении резолюции до получения пустого

дизъюнкта ð. Это будет, с точки зрения интерпретации, означать, что не существует никакой модели

(«мира»), в которой бы была справедлива исходная система законов (дизъюнктов).

А коль скоро доказательство выполняется методом от противного, то значит первоначальная формула

(дизъюнкт) действительно выводима (и, значит, справедлива) в данной теории.

Пример(Метод резолюций) : Можно сказать, что это прообраз или предельно упрощенный вариант

«системы искусственного интеллекта».

Пусть мир описывается двумя аксиомами:

Миша повсюду ходит за Леной А1."x(B(Л, x) ® B(M, x))

Лена в школе А2.B(Л, Ш)

Требуется доказать (ответить на вопрос)

Где Миша? А3. $х B(M, x) ?

Вопрос (доказываемую формулу с добавленным знаком вопроса) $х B(M, x)? преобразуем в . $х B(M, x)

(отрицание вопроса). Далее задвигаем отрицание за квантор, производим сколемизацию и добавляем

специальный «предикат ответа», который будет аккумулировать процесс унификации).

В результате получаем дизъюнкт: . B(M, x) Ú Отв(М, x)

Вся система (две аксиомы и вопрос) будет состоять из трех дизъюнктов:

Д1: B(Л, x) Ú B(M, x)

Д2:B(Л, Ш)

Д3: B(M, x) Ú Отв(M, x)

Вывод:

Резолюция Д1-Д2 дает Д4: B(M,Ш)

Резолюция Д4-Д3 дает Д5: ðÚОтв(M,Ш)

То есть. предикат ответа (при получении пустого дизъюнкта) можно интерпретировать как «Миша в школе».

(Интерпретация ответа в системе искусственного интеллекта остается за человеком).

Язык ПРОЛОГ

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

свободных переменных дизъюнктов. В Прологе используются только хорновские дизъюнкты,то есть

дизъюнкты, в которых не больше одного положительного предиката. В Прологе их называют обычно

предложениями или клозами.

То есть исходные аксиомы могут иметь в общем случае вид A₁ & A₂ & ... & A_n ® B

что при переводе в дизъюнкты будет ØA₁ Ú ØA₂ Ú ... ÚØA_n Ú B

Дизъюнкт, состоящий только из отрицательных предикатов - вопрос. А дизъюнкт, состоящий лишь из одного

положительного предиката – факт.

Примеры программы на Прологе.

1. append ([ ], L, L).

2. append ([ x | L1], L2, [x | L3]) :- append (L1, L2, L3).

Здесь [ ] выделяют список.

| - отделяет голову (первый элемент списка) от хвоста списка.

Добавим к предложениям, описывающим функцию append, вопрос: “Какой получится список при

объединении списков [a, b] и [c, d]?

3. ?-append ([a, b], [c, d], z).

Выполнение программы:

2 – 3: 4: append ([a | b], [c, d], [a | z1]) :- append ( [b], [c, d], z1).

2 – 4: 5: append ([b | [ ]], [c, d], [b | z2]) :- append ( [ ], [c, d], z2).

5 – 1: 6: append ([ ], [c, d], [c, d]).

В результате получим искомое z.

z2 = [c, d]; z1 = [b | z2] = [b, c, d]

z = [a, z1] = [a, b, c, d].

Даже на такой скромной модели можно решаить не одну, а ряд задач, Например, вопрос 3`: “ Какой список

надо добавить к [a, b])., чтобы получился список [a, b, c, d]).?“

3`. ?-append ([a, b], z, [a, b, c, d]).

Обращение списка:

обращение ([], []).

обращение ([Y | T], L) :- обращение (T, Z), append (Z, [H], L).

?- обращение ([a, b, c], X).

Понятие алгоритма.

Алгоритм -это строгое предписание по выполнению последовательности шагов, приводящее к решению

задачи данного типа. Понятие алгоритма относится к понятиям фундаментальным и неопределяемым.

Свойства алгоритмов:

1. Массовость.

2. Пошаговость.

3. Элементарность отдельных шагов (что такое «элементарно» каждый Ватсон понимает по-своему).

4. Детерминированность (точно известно, что нужно делать после каждого шага).

5. Эффективность (алгоритм должен привести к решению за конечное число шагов).

Главное разочарование программистов относительно теории алгоритмов состоит в том, что классическая

теория алгоритмов не занимается «правилами построения алгоритмов». На законный вопрос, чем же

она тогда занимается, можно достойно ответить: она занимается более важной проблемой – проблемой

алгоритмическойразрешимости. То есть занимается определением того, возможно ли вообще построить

алгоритм для решения задач данного типа.

Другими словами, существуют алгоритмически не разрешимые задачи, на алгоритмизацию которых не стоит

тратить время. Например,

невозможно построить функцию

F(х) = │1, если в числе p есть последовательность из х подряд цифр 5

í0, иначе.

Любопытна в связи с этим теорема:

Теорема:Алгоритмически неразрешимых задач больше, чем алгоритмически разрешимых.

Доказательство:Мощность множества функций (если угодно – задач) даже заведомо ограничено:

f

N ® N

не менее, чем континуум- À₁

Количество же вычислимых функций (если угодно – алгоритмов) счетно, т.е. À₀.

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

русского алфавита. А полученные конечные строки можно расположить в лексикографическом (алфавитном)

порядке, то есть пересчитать.

Таким образом, À₁ - À₀ = À₁