Новиков Ф.А. Дискретная математика для программистов (860615), страница 29
Текст из файла (страница 29)
Это высказывание может быть истинным или ложным (или пе иметь истинностного значения). Если соответствующее высказывание является истинным, то говорят, что формула выполняетсяв дайной интерпретации.ОТСТУПЛЕНИЕВ конечном счёте, нас интересуют такие формальные теории, которые описывают какие-тореальные объекты и связи между ними. Речь идёт прежде всего о математических объектахи математических теориях, которые выбираются в качестве области интерпретации.Интерпретация I называется моделью множества формул Г, если все формулыэтого множества выполняются в интерпретации I. Интерпретация I называется моделью формальной теории Т, если все теоремы этой теории выполняютсяв интерпретации I (то есть все выводимые формулы оказываются истиннымив данной интерпретации).4.2.4. Общезначимость и непротиворечивостьФормула называется общезначимой (или тавтологией), если она истинна в любой интерпретации.
Формула называется противоречивой, если она ложна в любой интерпретации.Формула G называется логическим следствием множества формул Г, если Gвыполняется в любой модели Г.Формальная теория 7 называется семантически непротиворечивой, если пи однаеё теорема не является противоречием.
Таким образом, формальная теория пригодна для описания тех множеств (алгебраических систем), которые являются еёмоделями. Модель для формальной теории 7 существует тогда и только тогда,когда Т семантически непротиворечива.Формальная теория Т называется формально непротиворечивой, если в ней неявляются выводимыми одновременно формулы F иТеория Т формальнонепротиворечива тогда и только тогда, когда она семантически непротиворечива.150Глава 4. Логические исчисленияЗАМЕЧАНИЕПоследние утверждения являются доказуемыми метатеоремами, доказательства которыхопускаются из-за технических сложностей.4.2.5.
Полнота, независимость и разрешимостьПусть интерпретация / : Т - » М является моделью формальной теории 7. Тогдаформальная теория Т называется полной (или адекватной), если каждому истинному высказыванию области интерпретации М соответствует теорема теории Т.Если для множества (алгебраической системы) М существует формальная полпая непротиворечивая теория Т, то система М называется аксиоматизируемой(или формализуемой).Система аксиом (или аксиоматизация) формально непротиворечивой теории 7называется независимой, если никакая из аксиом не выводима из остальных поправилам вывода теории Т.Формальная теория 7 называется разрешимой, если существует алгоритм, который для любой формулы теории определяет, является ли эта формула теоремойтеории.
Формальная теория Т называется полуразрешимой, если существует алгоритм, который для любой формулы F теории выдает ответ «ДА», если F являетсятеоремой теории, и, может быть, пе выдает никакого ответа, если F не являетсятеоремой (то есть алгоритм применим не ко всем формулам).4.3. Исчисление высказыванийВ этом разделе дано описание формальной теории исчисления высказываний.Поскольку исчисление высказываний уже знакомо читателю по материалам разделов 3.1 и 4.1, здесь сделай сильный акцепт именно на формальной технике. 'Знакомство с чисто механическим характером формальных выводов подготавливаетрассмотрение методов автоматического доказательства теорем в разделе 4.5.4.3.1. Классическое определение исчислениявысказыванийИсчисление высказываний — это формальная теория1. Алфавит:2. Формулы:3.
Аксиомы:4. Правило:в которой:-1 и —> — связки;( , ) — служебные символы;а, Ъ,..., а\, Ь\,... — пропозициональные переменные.1) переменные суть формулы;2) если А, В — формулы, то (->А) и (А —> В) — формулы.AiА2Аз{А_{Вл));((А —•(£?—> С)) - ((А - В)-* {А - С)));^4)—• Л) —> В)).^ — — (Modus ponens).В1514.3. Исчисление высказыванийЗдесь А, В и С — любые формулы.
Таким образом, множество аксиом теории £бесконечно, хотя задано тремя схемами аксиом. Множество правил вывода такжебесконечно, хотя оно задано только одной схемой.ЗАМЕЧАНИЕЛатинское словосочетание Modusponens обычно переводят на русский как правило отделения и обозначают MP.При записи формул лишние скобки опускаются, если это не вызывает недоразумений. Другие связки вводятся определениями:Ак-> - В ) ,ВА V ВD=-,A->В.Любая формула, содержащая эти связки, рассматривается как синтаксическоесокращение собственной формулы теорииОТСТУПЛЕНИЕКлассическое задание теории £ с помощью схем аксиом над любыми формулами вполнесоответствует математической традиции (мы пишем (а + Ь)2 = а 2 + 2ab+b2, подразумеваяпод а и & не только любые числа, но и любые выражения!).
В то же время это не оченьудобно для представления формальных теорий в программах. В следующих трёх подразделах вводится определение исчисления высказываний, более удобное для программнойреализации.4.3.2. Частный случай формулыЕсли в формулу (исчисления высказываний) А вместо переменных x i , . . . , x nподставить, соответственно, формулы B i , .
. . , В п , то получится формула В, которая называется частным случаем формулы А:BT£A(...,xi1...){Bi//xi}?=1.Каждая формула В{ подставляется вместо всех вхождений переменной ж*. Наборподстановок {Bi//xi}^гназывается унификатором.Формула С называется совместным частным случаем формул А и В, если Сявляется частным случаем формулы А и одновременно частным случаем формулы В при одном и том же наборе подстановок, то естьC = A(...,xi,...){XJ/xi}^1иC =B(...,xi,...){Xi//xi}^1.Формулы, которые имеют совместный частный случай, называются унифицируемыми, а набор подстановок [ X J с помощью которого получается совместный частный случай унифицируемых формул, называется общим унификатором.Наименьший возможный унификатор называется наиболее общим унификатором.152Глава 4.
Логические исчисленияНабор формул В\,..., Вп называется частным случаем набора формул А\,...,Ап,если каждая формула Bi является частным случаем формулы Ai при одном итом же наборе подстановок. Набор формул С\,..., Сп называется совместнымчастным случаем наборов формул А\,..., Ап и Вi,..., Вп, если каждая формула Ci является частным случаем формул Ai и Bi при одном и том же набореподстановок.4.3.3. Алгоритм унификацииЕсли язык формул удовлетворяет определённым условиям, то можно проверить,являются ли две заданные формулы унифицируемыми, и если это так, то найтинаиболее общий унификатор.
В частности, это возможно для типичного языкаформул, описанного в подразделе 4.3.1. В следующем алгоритме предполагается,что функция / осуществляет синтаксический разбор формулы и возвращает знакглавной операции (то есть —>, -i или признак того, что формула является переменной), а функции I и г возвращают левый и правый операнды главной операции,то есть подформулы (считаем, что отрицание имеет только правый операнд).
Набор подстановок (унификатор) представлен в виде глобального массива S, значениями индекса которого являются имена переменных, а значениями элементов —формулы, которые подставляются вместо соответствующих переменных.Алгоритм 4.1 Рекурсивная функция UnifyВход: формулы А и В.Выход: false, если формулы не унифицируемы; true и наиболее общийунификатор S в противном случае,if f(A) — переменная thenv: = f(A) { переменная }if S[v] = 0 thenS[v]: = В; return true { то есть добавляем подстановку {B//v} }elsereturn (S[v] = В) { либо эта подстановка уже есть, либо унификацияневозможна }end ifend ifif f(A) ф f(B) thenreturn false { главные операции различны — унификация невозможна }end ifif f(A) = ' - / thenreturn Umfу(r(A), r(B)) { пытаемся унифицировать операнды отрицаний }end ifif f(A) ='->' thenr e t u r n Unify(1(A), 1(B)) & Unify(r(A),r(B)){ пытаемся унифицировать операнды импликаций }end if1534.3.
Исчисление высказыванийПри любых подстановках формул вместо переменных главная операция (связка) формулы остаётся неизменной. Поэтому если главные операцииформул различны, то формулы заведомо не унифицируемы. В противиом случае,то есть если главные операции совпадают, формулы унифицируемы тогда и только тогда, когда унифицируемы подформулы, являющиеся операндами главнойоперации.
Эта рекурсия заканчивается, когда сопоставление доходит до переменных. Переменная унифицируется с любой формулой (в частности, с другой переменной) простой подстановкой этой формулы вместо переменной. Ноподстановки для всех вхождений одной переменной должны совпадать.•ОБОСНОВАНИЕ4.3.4. Конструктивное определение исчислениявысказыванийАлфавит и множество формул — те же (см. 4.3.1).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
