вфцвфцввц. Математическая логика
 Скачать 2.56 Mb.
|
|
Теорема эквивалентности. Если и - формулы, полученные заменой некоторых (одних и тех же) вхождений какой-либо высказывательной переменной в формуле U соответственно формулами и , то | . Следствие. Если есть некоторая подформула формулы U и эквивалентна формуле , то формула, полученная заменой в формуле U на , эквивалентна U. Иными словами, если , то . Свойства 2, 4, 10 и теорема эквивалентности позволяют формулу, составленную из высказывательных переменных лишь с помощью операции дизъюнкции, преобразовать к виду . Аналогично формула, составленная из с помощью операции конъюнкции эквивалентна формуле . Это позволяет дать определение понятиям нормальных форм исчисления высказываний, которые совпадают с соответствующими определениями алгебры высказываний. Теорема 3.1. Для каждой формулы исчисления высказываний существуют эквивалентные ей дизъюнктивная и конъюнктивная нормальные формы. 4. Исчисление секвенций ИС. Исчисление высказываний генценовского типа называется исчислением секвенций ИС. Алфавит ИС состоит из символов алфавита ИВ, дополненных символом |. Допустимые последовательности символов – формулы определяются также как и в ИВ, кроме того, в ИС вводится понятие секвенция. Пусть U1, U2, . . . ,Un, V – формулы ИС. Секвенциями называются конечные последовательности следующих двух видов: U1, U2, . . . ,Un | V (из истинности U1, U2, . . . ,Un следует истинность V); U1, U2, . . . ,Un |- (система формул U1, U2, . . . ,Un противоречива). Множество аксиом ИС определяется единственной схемой секвенций U |- U. Правила вывода ИС определяются следующими записями, где T,T1 – конечное множество формул (возможно пустое). (введение ). (удаление ). (удаление ). (введение ). (введение ). (удаление или правило разбора двух случаев). (введение ). (удаление ). (удаление или доказательство от противного). (выведение противоречия). (перестановка посылок). (уточнение или правило лишней посылки). Исчисления ИВ и ИС эквивалентны. Исчисления предикатов ИП (ИПС). Определим исчисление предикатов гильбертовского типа ИП. Это исчисление является расширением исчисления высказываний ИВ. В алфавит ИВ добавим строчные латинские буквы для обозначения предметных переменных и символы кванторов и . Язык исчисления составляют формулы, определяемые также, как в алгебре предикатов. Аксиоматика исчисления дополняется двумя схемами аксиом: , где - произвольная формула, содержащая свободные вхождения переменной x, причем ни одно из них не находится в области действия квантора по переменной y, а получена из заменой свободных вхождений xна y. К правилу заключения ИВ добавляются два правила, связанные с кванторами. Пусть и – формулы, которые содержат и не содержат свободные вхождения переменной x соответственно. Правило обобщения (введения ) . Правило введения . Правила естественного вывода дополняются 4-мя правилами. Пусть Правило введения квантора . Если T |- U(x), то T |- xU(x). Правило удаления квантора . Если T |- xU(x), то T |- U(y). Правило введения квантора . Если T |- U(y), то T |- xU(x). Правило удаления квантора . Если T, U(x) |- V, то T, xU(x) |- V. Рассмотрим пример вывода в ИП. Доказать, что в ИП |-
Исчисление предикатов генценовского типа ИПС строится расширением исчисления ИП. Прикладные исчисления предикатов. Прикладные исчисления предикатов строятся добавлением к исчислению предикатов своих собственных аксиом. Причем, в прикладных исчислениях предикатов вводится понятие терма. Термами являются: предметные переменные и константы; предметные функции. В аксиомах прикладных исчислений предикатов наряду с предметными переменными могут использоваться произвольные термы, так аксиомы 11, 12 в них имеют вид: , где t – произвольный терм. Всюду далее будут рассматриваться прикладные исчисления предикатов первого порядка, т. е. исчисления, в которых кванторами связываются только предметные переменные, а не предикаты и функции. Исчисление с равенством. В данном исчислении вводится предикат =, а к аксиомам ИП добавляются аксиомы равенства. E1. E2. Здесь Е1 является аксиомой, а Е2 – схемой аксиомы, где – произвольная формула, а – формула, полученная из заменой некоторых вхождений xна y. Теорема 6.1. В любой теории с равенством: |- для любого терма t; |- ; |- . Доказательство. 1) Данное утверждение непосредственно следует из аксиом 11’ и Е1, где . Для свойств 2), 3) построим формальные выводы формул. 2)
3)
Строгий частичный порядок. Предикатом строгого частичного порядка является предикат <, а дополнительными – следующие аксиомы. NE1. NE2. Формальная арифметика. Формальная арифметика определяется как исчисление с равенством на предметном множестве , в котором вводятся предметная константа 0 и предметные функции + , , , задаваемые аксиомами. A1. A2. A3. A4. A5. A6. A7. A8. Здесь А1-А7 – аксиомы, а А8 – схема аксиомы, определяющая доказательство по индукции. Автоматическое доказательство теорем Автоматическое доказательство теорем является основой логического программирования, одним из способов построения систем искусственного интеллекта. Алгоритм, который проверяет соотношение |- S для формулы S, множества формул и теории называется алгоритмом автоматического доказательства теорем. Для достаточно простых формальных теорий, например, прикладных исчислений первого порядка такой алгоритм существует. Автоматическое доказательство проводится методом резолюций, в основе которого лежит способ доказательства от противного. Часто логическим программированием называют автоматическое доказательство методом резолюций, однако этот метод лишь наиболее разработанный его частный случай. Теорема 7.1. Если , S|- F, где F – любое противоречие, то |- S. Доказательство. Если , S |- F, то (S)|- F, так как (S)|- и (S)|- S. Следовательно, |- (S) F. Так как (S) F , то |- и, следовательно, |- S. Метод резолюций работает со стандартной формой формул, называемой предложениями. Предложением называется бескванторная дизъюнкция литералов. Любая формула исчисления предикатов может быть преобразована в множество предложений по следующему алгоритму. Построить предварённую нормальную форму формулы. Напомним, что для этого нужно: преобразовать формулу к приведённому виду, т.е. исключить операцию и спустить операцию отрицания до атомарных формул; провести разделение связанных переменных; вынести операции связывания переменных в начало формулы. Преобразовать предварённую нормальную форму в предклазуальную, т.е. привести матрицу U нормальной формы к КНФ. Провести сколемизацию нормальной формы (построить клазуальную нормальную форму, исключив операции связывания переменных). Удалить операции (дизъюнкции клазуальной нормальной формы составят искомое множество предложений). Далее к предложениям, полученным из формул множества и из формулы S, применяется правило резолюции. Сформулируем это правило для исчисления высказываний, а, затем, обобщим его для исчисления предикатов. Определение. Пусть – предложения исчисления высказываний, такие что , . Правило вывода называется правилом резолюции исчисления высказываний, предложения – резольвируемыми, а – резольвентой. Замечание. Многие рассмотренные ранее правила вывода являются частными случаями правила резолюции. Например, основное правило исчисления ИВ – правило заключения можно представить в виде . Таким образом, множество предложений будет являться противоречивым, если в результате последовательного применения правила резолюции, получим пустую формулу, которую будем обозначать . Действительно, если резольвента пуста, то резольвируемые предложения – взаимно противоположные высказывания и система предложений противоречива. Задание 1. Доказать методом резолюций |- . Решение. В данном примере – пусто, . Преобразуем формулу в множество предложений. A A š Применив к предложениям 1, 3 правило резолюции, получим пустую формулу, то есть противоречие. Следовательно, формула S является выводимой из пустого множества посылок или теоремой рассматриваемой теории. Для того чтобы сформулировать правило резолюции для исчисления предикатов введём понятие унификатора. Определение. Подстановкой сигнатуры называется конечное множество вида , где – терм сигнатуры , отличный от переменных и все переменные различны. Например, множества и являются подстановками сигнатуры . Пусть U – формула, а – подстановка сигнатуры . Обозначим через формулу, полученную заменой всех вхождений на термы . Определение. Подстановка сигнатуры называется унификатором для множества формул сигнатуры , если . Множество формул сигнатуры , называется унифицируемым, если для него существует унификатор сигнатуры . Например, множество формул сигнатуры унифицируемо, так как подстановка является его унификатором. Определение. Пусть и – подстановки сигнатуры . Композицией подстановок и (обозначается ) называется подстановка, которая получается из множества вычеркиванием всех элементов , для которых , и всех элементов , для которых . Пример. Пусть , . Тогда = , а так как и , то . Определение. Унификатор для множества формул сигнатуры называется наиболее общим унификатором (НОУ), если для каждого унификатора сигнатуры этого множества существует подстановка сигнатуры такая, что . Так для множества наиболее общим унификатором является подстановка . Определение. Пусть – предложения исчисления предикатов, такие что , , а атомарные формулы унифицируемы наиболее общим унификатором . Правило вывода называется правилом резолюции исчисления предикатов. Задание 2. Проверить G |- , где : , , , . Решение. Выпишем множество предложений , S, пронумеровав их. Далее будем добавлять предложения в это множество, применяя правило резолюции с возможной предварительной унификацией. Рядом с новым предложением будем указывать способ его получения (правило резолюции или унификация) и номера предложений, к которым он применялся. R(1, 5) (2, 6) R (6, 7) (4, 8) š R(8, 9) Следовательно, G |- . Работа метода резолюций может иметь следующие варианты результатов: на очередном шаге получено пустое предложение и, следовательно, формула S является следствием (теорема доказана); если во множестве предложений нет новых резольвируемых предложений, то теорема опровергнута; множество предложений постоянно пополняется новыми предложениями (зацикливание), что означает, что средств данной теории недостаточно ни для того, чтобы доказать теорему, ни для того, чтобы её опровергнуть. Представим алгоритм работы метода резолюций на языке описания алгоритмов. Результат 1 – если Sвыводимо из , 0 – в противном случае. Обозначим M – множество предложений, C – множество предложений, полученное из и S. Функция choose выполняет выбор резольвируемых предложений, R – вычисляет резольвенту. while C begin choose ( ) if then return 0 R( ) end return 1 ТЕОРИЯ АЛГОРИТМОВ Неформально понятие алгоритма, как последовательности действий направленных на решение некоторой задачи, вводилось ещё в курсе информатики. Далее в курсах технологии программирования, дискретной математики, математической логики рассматривались алгоритмы решения различных типов задач. В данном разделе мы формализуем понятие алгоритма, введём понятие вычислительной сложности алгоритма, классифицируем алгоритмы. Вид формальной модели алгоритма зависит от тех понятий, которые положены в основание модели. Первый подход основан на представлении об алгоритме, как о программе для некоторого детерминированного устройства. К моделям этого типа относятся машины Тьюринга, канонические системы Поста, нормальные алгорифмы Маркова. Второй подход основан на понятии вычисления и числовой функции, основная теоретическая модель этого вида – рекурсивные функции. Перед введением формальных определений алгоритма сформулируем понятия, необходимые для дальнейшего изложения. Всюду далее будет рассматриваться некоторая массовая задача . Массовая задача определяется следующей информацией: общим списком параметров задачи; формулировкой свойств, которым должно удовлетворять её решение. Напомним, что этот набор называют ещё спецификацией задачи. Индивидуальная задача I получается подстановкой в массовую задачу данного вида конкретных значений параметров. Будем говорить, что алгоритм решает массовую задачу , если применим к произвольной индивидуальной задаче I, соответствующей задаче , и даёт решение задачи I. В качестве массовой задачи будем рассматривать задачу распознавания, т.е. задачу решением которой могут быть ответы “да” или “нет”. Например, задачей распознавания является задача определения – делится ли заданное натуральное число нацело на 4. Это не ограничивает общности, так как любая задача может быть сформулирована в терминах задачи распознавания. Обозначим через – множество всех индивидуальных задач, соответствующих задаче , – множество индивидуальных задач с ответом “да”. Таким образом, задача распознавания состоит в определении этих двух множеств. Для записи задачи распознавания используется естественный формальный эквивалент, называемый языком. Обозначим – конечное множество символов (алфавит), * – множество всех конечных цепочек, составленных из (слова), – подмножество *, называемое языком. Соответствие между задачами распознавания и языками устанавливается с помощью схем кодирования. Схема кодирования e записывает каждую индивидуальную задачу из словом в фиксированном алфавите . Множество * делится задачей и схемой кодирования e на 3 класса: слова, не являющиеся кодами индивидуальных задач из ; слова, являющиеся кодами с отрицательным ответом; слова, являющиеся кодами с положительным ответом. Третий класс слов обозначим . |