prosdo.ru
добавить свой файл
1

МЛ1. Формальные (аксиоматические) теории. Их разрешимость. Натуральное исчисление.

Формальная теория состоит из:


  1. Алфавит – счетное множество символов.

Конечные последовательности этих символов – слова.

  1. Формулы – подмножества выражений

Обычно существует эффективная процедура, определяющая является ли выражение формулой

  1. Аксиомы – подмножества формул

  2. Конечное множество отношений (правила вывода).

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

В некоторых системах существует подстановка подстановка в формулу А выражение В вместо b. Аналогично вместо b B.

Выводом называется последовательность формул , где - либо аксиома, либо выведена из предыдущих формул по одному из правил вывода.

Говорят, что F – теорема, если существует в конце которого стоит F.

Пусть - набор формул.

Если F выводима из подмножества , то говорят, что (F выводима из Г).


МЛ2. Основные проблемы формальных теорий. Непротиворечивость исчисления высказываний. Полнота исчисления высказываний. Независимость системы аксиом.
Непротиворечивость:

А) непротиворечивость относительно преобразования , Теория наз непротивореч относительно преобраз-я A->A! если или не явл-ся теоремой форм теории.


Б) Если не всякая формула А является теоремой – абсолютная непротиворечивость

В) Непротиворечивость в смысле Поста – если любая пропозициональная переменная не является теоремой.
Теорема: всякая теорема является тавтологией.

Теорема: всякая тавлогией является теоремой (то есть существует и выводима)

Полнота: Пусть имеется формула


  • Либо она доказана

  • Либо присоединяется в качестве аксиомы – тогда теория становится противоречивой

А) Полнота относительно преобразования :

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

Б) -//- противоречива в абсолютном смылсе

В) -//- противоречива по Посту

Независимость:

Если аксиома не может быть выведена в теории как теорема, то она не зависит от других аксиом и правил вывода.

МЛ3. Исчисление предикатов первого порядка. Кванторы. Область истинности предиката.

Предикат – высказывательная форма.

Терм

1) константа

2) переменная

3) если термы

4) других термов нет

Квантор навешивается на переменную.

Кванторы: Всеобщности( ); Существования( ); Существует единственный ; Существует бесконечно много .

Правила

  • Одноименные кванторы можно менять местами


  • , причем обратное неверно



МЛ4. Интерпретация формальной теории. Модель формальной теории.

, где

D – множество значений всех переменных и констант (обл итерпр-ции)

Г – соответствие, которое любому предикатному символу ставит в соответствие некоторое отношение, а любой функции – некоторую функцию Di->D

  1. Предикативная формула истинна в некоторой интерпретации, если для любого набора значений из D формула – истинное высказывание

  2. -//- ложна -//- - ложное высказывание

  3. -//- выполнима, если существует хотя бы один набор из D для которого формула – истинное высказывание

  • истина ложна

  • A не может быть И и Л одноврем

  • и истина истина

  • ложна истина ложна

  • ложна ложна ложна

A & N истина -> A истина и N истина

МЛ5. Теорема Чёрча. Теорема Гёделя о полноте

Теорема Чёрча:

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


То есть теория исчисления предикатов первого порядка неразрешима.
Лемма 1.

Если замкнутая формула не выводима в некоторой теории К, то – новая теория K’. K’ – непротиворечива.

Лемма 2.

Все аксиомы (А1 – А5) теории первого порядка являются логически общезначимыми.

Лемма 3.

Правила вывода МР и Gen из логически общезначимых формул производят логически общезначимые.

А1:

A2:

A3:

A4: если t свободна для x в

А5: x не входит свободно в



МЛ6. Общие свойства алгоритмов. Машина Тьюринга

Алгоритм – четкое предписание, однозначно определяющее некоторую последовательность действий, которые за конечное число операций приводят к некоторому заранее известному результату.

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

Свойства:

  1. Детерминированность (определенность каждого последующего шага)

  2. Массовость (решается класс задач)

  3. Направленность (результат должен быть получен за конечное число шагов)


Машина Тьюринга:

  1. Алфавит А = {λ, }, λ – пустой символ.
  2. Множество состояний Q = { }, – начальное,– конечное.


  3. Бесконечная лента с головкой. Одна ячейка ленты – один символ.

  4. Работа машины определяется программой, состоящей из команд вида:

- {П, Л, Н}. q – состояния, a – символы, П, Л, Н – право, лево, на месте соответственно.


МЛ7. Вербальные переменные, предикаты и алгоритмы.
Вербальная переменная - переменная, значениями которой является различные слова в некотором алфавите.

Любой символ алфавита – литера.

Литерная переменная – переменная, значениями которой являются литеры.

Если алфавит состоит из единственного символа, то все переменные называются натуральными.

Предикат - называется вербальным предикатом, если - вербальные переменные.
Вербальный алгоритм – алгоритм работающий над словами в некотором алфавите.

Говорят что алгоритм применим к слову Р , если он за конечное число шагов перерабатывает P в Q. Пишут

слова P Q в алф A граф-ки одинковые.

Если алфавит состоит из | или 1 то все верб перемен наз натуральн.

Пустое слово λ не содержит ни одно символа 1) любой пуст слово = любому пустому слову 2) пуст слово явл словом в любом алф-те, в т ч из одного |

МЛ8. Тезис Чёрча и принцип нормализации.

Тезис Чёрча:

Числовая функция тогда и только тогда алгоритмически вычислима, когда она частично рекурсивна .

Функция f заданная на некотором множестве слов алфавита A, называется нормально вычислимой, если найдется такое расширение B данного алфавита (AB) и такой нормальный алгоритм в B , что каждое слово VА) из области определения f этот алгоритм переработает в f(V).


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

(по Дубине)

Тезис Чёрча :

Любая эффективно вычислимая функция может быть представлена как - вычислимая функция.


  • истина истина

  • Любая тавтология истинна в любой интерпретации

  • Замкнутая форма истинна либо ложна в некоторой интерпретации

  • Пусть есть наборы и , совпадающий с S по . Тогда истинен на S истинен на S’

Замкнутая формула – формула, не содержащ перемен. Она либо ист, либо ложн в данн I.

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

Интерпретации M и M’, если существует такое отображение :

Моделью называется интерпретация, в которой истинны все модели теории. Множество моделей теории называется классом моделей.

Область истинности - набор всех значений переменных предиката, при которых он превращается в истинное высказывание. Короче А с крышечкой)



















и , тогда





Формальная теория разрешима, если существует алгоритм, позволяющий для любой формулы определить – является ли она теоремой.

Примером формальной теории является натуральное исчисление.

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



Натуральное исчисление

1)

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

3) аксиом нет

4) МР , УК , ВД , ВК

УД

Квазипрямой вывод




  1. гип

  2. УК 1

  3. A гип

  4. МР 2, 3

  5. УК 1

  6. МР3,4



Принцип Нормализации:

Для любого вербального алгоритма существует вполне эквивалентный ему нормальный алгоритм.





Машина Тьюринга в зависимости от текущего состояния и символа в текущей ячейке:

  1. Затирает текущий символ ai и записывает символ aj.

  2. Переходит из состояния qs в qe.

  3. Передвигает головку вправо (влево, либо оставляет на месте).


Машина всегда начинает работу в начальном состоянии и завершает работу по достижению конечного состояния.
Пусть в начале работа МТ на ленте было написано слово (последовательность символов из А). По окончанию - слово . Говорят, что МТ переработала слово в слово .
Тезис Тьюринга:

Для нахождения значений функции, заданной в некотором алфавите, тогда и только тогда существует какой-нибудь алгоритм, когда функция является вычислимой по Тьюрингу, то есть когда она может вычисляться на подходящей машине Тьюринга.

Терм t свободен для xi, если она не лежит в области действия квантора ни по какой xj для любого своего свободного вхождения.

Теорема Геделя о полноте:


  1. Любая теорема исчисления предикатов первого порядка является логически общезначимой.

  2. Любая логически общезначимая формула – теорема исчисления предикатов первого порядка.

Док-во из лемм 1-3.


МЛ9. Нормальные алгорифмы (НА), применимость. Естественная сложность НА, число шагов.Арифметические алгорифмы.

Алфавит – любое непустое множество.

Буква - элемент алфавита.

Слово – последовательность букв.

Пусть слово-

Если А и B - два алфавита и AB, то B - расширение А

Одно слово может быть составной часть другого слова – являться вхождением.

Марковская подстановка( P,Q)- в заданном слове К находят первое вхождение слова P и заменяет на Q. Если нет вхождений P в K – подстановка не применима.

P K- формула постановки (P , Q)

P Q – формула заключающей подстановки

- схема нормального алгорифма

МЛ10. Понятие о массовой алгоритмической проблеме. Классы задач.

Пусть имеется слово Х и предикат Р(Y). Определить, удовлетворяет ли Х предикату P(Y) – единичная проблема. Для каждого слова – массовая проблема.

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

Классы задач:


  • Нерешенные задачи

  • Решенные задачи

    • Р (полиномиальные)

  • NP

    • NP-трудные

    • NP-полные

    • Недетерминированные


Оценка сложности – О(.)

Функция f(y) имеет порядок функции g(y) – O(g(y)), если
Сложности задач: O(n), O(n(n(n)))

P – O(ns)-полиномиалная

NP – экспоненциальная сложность. O(cn)



МЛ11. Стандартная форма Сколема. Теорема о ней. Эрбрановский универсум. Эрбрановский базис.

Норм преваренная форма все кванторы вперед.

Стандартная форма Сколема получается так:

  1. Произвольную формулу привести к предваренной форме) (примечание: здесь «К» пишется в обратную сторону квантор Он означает один из двух кванторов, пофигу какой: ) К1х1…КnxnM(.), причем М(.) не содержит ни одного квантора.

  2. М(.) преобразуется в КНФ

  3. а) Если квантор стоит первым, то выбираем константу, не использованную в М(.), и заменяем все вхождения переменной под квантором на эту константу. - удаляем из формулы.

б) Находим первое вхождение , т.е.



Выбираем функциональный символ f, который не используется в М(.) и заменяем все вхождения xi на - удаляем из формулы.

Повторяем а-б, пока есть кванторы .

Для выполнимой формулы сколемовская форма не эквивалентна исходной формуле.

Множество S назовем системой дизъюнктов. Если хотя бы один дизъюнкт ложен – вся формула ложна (т.к. это КНФ).

Теорема.

Для произвольной формулы F и ее S – сколемовской системы дизъюнктов: F ложна S ложна.


МЛ12.Резолютивный вывод. Подстановка. Композиция подстановок. Унификатор. Метод резолюций для логики предикатов.

и - контрарная пара

Метод резолюций:

, Q и QvR – резольвенты.

Резолютивным выводом называется последовательность формул, каждая из которых либо элемент S-системы дизъюнктов, либо резольвента.

- пустое выражение вывод завершен доказано, что система S невыполнима.

Если P содержит переменные возникает проблема. и - неконтрарная пара, однако если и получим контрарную пару.


МЛ12.Резолютивный вывод. (продолжение)

Подстановка является унификатором, если применение этой подстановки к любым дает равенство .

Если , тогда .


Применение метода резолюций для логики предикатов:


  1. Ищем такие, что после унификации образуют контрарные пары, унифицируем и применяем к ним правила I-III из начала шпоры.



  1. Если в какой-то формуле есть , такие что - унифицируем и оставляем только (то есть проводим склейку).












Введем понятие подстановки. Подстановка , - что, - куда.

Композиция подстановок :

  1. Есть и

  2. Применим к каждому

  3. Уберем из все элементы , если такие появились

  4. Уберем из все элементы, где

  5. Тогда композиция = {оставшиеся элементы , оставшиеся элементы }

Пусть есть множество формул .



Выражение называется основным, если не содержит ни одной переменной.

Эрбрановским универсумом называется объединение множеств , здесь:

  1. S – система дизъюнктов

  2. H0(S) – множество предметных констант из S. Если в S нет констант, то H0(S) = {a} – любая константа.



Пример:



Если в S есть функциональный символ, строить можно бесконечно.

Эрбрановским базисом множества дизъюнктов S называется мн-во основн примеров всех атомов в системе дизъюнктов



Если заменить в дизъюнкте переменные на термы, получим пример дизъюнкта. Если термы являются основными – получим основной пример.

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



По интерпретациям строятся семантические деревья.


Эрбрановский универсум это множество всех термов,

которые можно построить из констант и функциональных

символов заданной сигнатуры. Термы эрбрановского

универсума не содержат переменных и называются основными

термами .

Нормальный алгорифм в алфавите А называется следующее правило построения последовательности слов в алфавите A. Исходное слово На i-м шаге имеем . Отыскиваем первую формулу подстановки, левая часть которой имеет вхождение в . Осуществляем подстановку в i-ое вхождение . Если подстановка заключительная – стоп. Иначе – следующий шаг. Если ни для какой формулы подстановки нет вхождений левый части в -стоп .


Если процесс построения последовательности обрывается, то говорят , что НАМ применим к слову. Еслиговорят что НАМ переработан из V в W.

Числом шагов называют длину последовательности минус 1

Естественной сложностью называют длину схем.

Алгорифм над алфавитом А={1} называется арифметическим.