🗊Презентация Общие сведения о формальных и аксиоматических системах

§3. ОБЩИЕ СВЕДЕНИЯ О ФОРМАЛЬНЫХ И АКСИОМАТИЧЕСКИХ СИСТЕМАХ

Определение Формальная система представляет собой совокупность чисто абстрактных объектов, не связанных с внешним миром, в которой представлены правила оперирования множеством символов только в синтаксической трактовке без учета смыслового содержания.

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

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

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

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

Обычно это утверждения, правильность которых не вызывает сомнения, и они принимаются как очевидные истины. Такие выражения называют аксиомами, а системы, в основе построения которых лежит использование аксиом, называются аксиоматическими системами.

Определение формальной системы осуществляется в следующем порядке: Определение формальной системы осуществляется в следующем порядке: 1. Задается конечное множество символов, которые образуют алфавит формальной системы. 2. Устанавливаются процедуры построения формул формальной системы.

3. Устанавливается множество аксиом, т.е. формул, истинность которых не требует доказательства. Обычно к ним относят те утверждения, которые полагаются очевидными по самой природе рассматриваемых понятий. 3. Устанавливается множество аксиом, т.е. формул, истинность которых не требует доказательства. Обычно к ним относят те утверждения, которые полагаются очевидными по самой природе рассматриваемых понятий. 4. Устанавливается конечное множество правил вывода, которые позволяют получать новые формулы из некоторого множества известных формул.

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

Определение Формальным доказательством, или просто доказательством, называется последовательность формул такая, что каждая формула является либо аксиомой, либо выводима из предшествующих ей формул . Формула t называется теоремой, если существует доказательство, в котором она является последней.

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

Различают два типа правил вывода. 1. Правила, применяемые к формулам, рассматриваемым как единое целое, в этом случае их называют продукционными правилами. Пример. x < y и y < z, следовательно x < z  это продукция с двумя посылками.

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

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

Пример Рассмотрим формальную систему следующего вида: Алфавит = {a, b, w}. Формулы  символ или последовательность символов a, b или w. Аксиома awa. Правило вывода (продукция). с1 w с2 -> b с1 w с2 b

Символы с1 и с2 не принадлежат алфавиту формальной системы (ФС), они служат посредниками для формализации правил вывода. То есть с1 и с2 обозначают какие-либо последовательности символов a или b формальной системы и могут быть замещены любыми последовательностями символов a или b. Учитывая способ образования формул, можно сказать, что незамещаемые символы a и b называются константами, а символ w - оператором.

Из определения ФС вытекает и способ получения допустимых формул, т.е. формул, выводимых согласно правилу вывода путем его последовательного применения к аксиоме: Из определения ФС вытекает и способ получения допустимых формул, т.е. формул, выводимых согласно правилу вывода путем его последовательного применения к аксиоме: awa bawab bbawabb bbbawabbb и т.д.

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

Определение Интерпретация представляет собой распространение исходных положений какой-либо формальной системы на реальный мир. Интерпретация придает смысл каждому символу формальной системы и устанавливает взаимно однозначное соответствие между символами формальной системы и реальными объектами.

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

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

1. Математик изучает реальность, конструируя некоторое абстрактное представление о ней, т.е. некоторую формальную систему. 1. Математик изучает реальность, конструируя некоторое абстрактное представление о ней, т.е. некоторую формальную систему. 2. Строится доказательство теорем формальной системы. Вся польза и удобства формальных систем заключаются в их абстрагировании от конкретной реальности. Благодаря этому одна и та же формальная система может служить моделью многочисленных различных конкретных ситуаций.

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

Замечание Изучение аксиом и теорем как абстрактных выражений, представленных в некоторой форме, называется синтаксическим изучением аксиоматических систем (АС); изучение и рассмотрение смысла этих выражений называется семантическим изучением АС. С синтаксическим аспектом АС и связано понятие формальной системы.

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

1. Проблема противоречивости. Логическое исчисление называется непротиворечивым, если в нем недоказуемы никакие две формулы, из которых одна является отрицанием другой. 2. Проблема полноты. Система исчисления считается полной, если любая теорема теории может быть доказана или опровергнута.

3. Проблема независимости аксиом. Для начала введем понятие независимой аксиомы. Аксиома называется независимой, если она не может быть выведена из других аксиом. Система аксиом исчисления называется независимой, если каждая аксиома в ней независима. 4. Проблема разрешимости. Система исчисления называется разрешимой, если существует алгоритм, позволяющий по каждому утверждению выяснить, является ли оно истинным или ложным.

§4. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Определение Исчисление высказываний (ИВ), т.е. логика высказываний – это формальная система, интерпретацией которой является алгебра высказываний. Под высказыванием понимается повествовательное предложение, о котором можно сказать, что оно истинно или ложно.

Как и любая формальная система, исчисление высказываний строится на основе четырех основных процедур: 1. Задания алфавита. 2. Установления правил построения формул. 3. Определение аксиом. 4. Определение правил вывода.

Алфавит, который состоит из символов трех категорий: Алфавит, который состоит из символов трех категорий: а) бесконечное счетное множество высказываний (или переменных высказываний), которые обычно обозначаются буквами: x, y, z, a, b, c, x10, y1, , и т.д.; б) логические операторы (или логические связки), которые обозначают символы логических операций (v, &, и т.д.); в) открывающиеся и закрывающиеся скобки: ( , ) . Других символов в ИВ нет!!!

Формулы в исчислении высказываний однозначно получаются с помощью правил, которые описываются базисом и индуктивным шагом: Формулы в исчислении высказываний однозначно получаются с помощью правил, которые описываются базисом и индуктивным шагом: базис: всякое высказывание есть формула; индуктивный шаг: если X и Y  формулы, то , , , также формулы. Никакая другая последовательность символов не является формулой!!!

Пример. Если x, y, z  формулы в соответствии с правилом базиса, то (x->y), (x&z) и т.д.  формулы в соответствии с правилом индуктивного шага. Очевидно, что не будут формулами: &x, (x&z, т.к. они не удовлетворяют вышеуказанным правилам. В первом случае в бинарной операции используется один операнд, а во втором  отсутствует закрывающая скобка!!!

С введением понятия формулы вводится и понятие подформулы или части формулы, делается это следующим образом. С введением понятия формулы вводится и понятие подформулы или части формулы, делается это следующим образом. Подформулой элементарной формулы является только она сама. Если X - формула, то ее подформулами будут: она сама, X и все подформулы X. Обозначим w  любую из логических операций (v, &, -> и т.д.), кроме отрицания. Тогда, если (XwY)  формула, то ее подформулы: она сама, формулы X и Y и все подформулы X и Y.

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

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

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

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

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

Пример

Правила вывода устанавливают отношения на множестве формул исчисления высказываний. Правила вывода обычно представляются как отношения на множестве формул исчисления высказываний. Над чертой записываются формулы, которые играют роль посылки (уже известные истинные выражения), а под чертой – выводимая формула, истинность которой утверждается данным правилом. Она называется следствием или заключением.

В исчислении высказываний используется два правила вывода: В исчислении высказываний используется два правила вывода: правило заключения (modus ponens). Если A и  это выводимые формулы, то B также является выводимой формулой. Записывается это правило так:

2) правило подстановки. где - это формулы,  попарно различные переменные высказывания; через запись обозначен результат одновременной замены всех вхождений переменных в A на формулы

Справедливость правил вывода исчисления высказываний подтверждается применением методов булевой алгебры. Справедливость правил вывода исчисления высказываний подтверждается применением методов булевой алгебры. В частности, тождественную истинность выводимой формулы В можно установить следующим образом: если А и А → В  тождественно истинные формулы, то есть А = 1 и А → В = 1, следовательно Так как в последнем выражении = 0, а значение логической суммы равно 1, то В должно быть равно 1 (то есть быть истинным).

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

Правило сложного заключения. Если  формулы и  теорема, то формула B  также теорема. Правило двойного отрицания Если и  теоремы, то будет теоремой и формула иначе и

Правило силлогизма (замыкания). Правило силлогизма (замыкания). Если и  теоремы, то также теорема, иначе Правило композиции. Если теорема, то так же теорема, иначе

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

Правило заключения ИСХОДНЫЕ ПОСЫЛКИ. Если данный многоугольник правильный (А=1), то в него можно вписать окружность (А → В). Возьмем правильный многоугольник (А=1). ВЫВОД. В данный многоугольник можно вписать окружность (В = 1).

Правило силлогизма ИСХОДНЫЕ ПОСЫЛКИ. Если треугольник равнобедренный (А = 1), то две его стороны равны (В = 1), т.е. А → В. Если две стороны треугольника равны (В = 1), то два его угла равны (С = 1), т.е. В → С. ВЫВОД. Если треугольник равнобедренный, то два его угла равны (А→С).

Как отмечалось выше, формулы исчисления высказываний можно интерпретировать как формулы алгебры высказываний (АВ). Для этого следует переменные ИВ трактовать как переменные АВ, т.е. переменные, которые могут принимать только значение 0 и 1 (ложь и истина). Все логические операции (, ,  и т.д.), которые используются в ИВ, интерпретируются так же, как и в АВ, т.е. на основе тех же самых таблиц истинности. Очевидно, что между формулами ИВ и АВ существует взаимнооднозначное соответствие.

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

Определение. Формула выполнима, если она может принимать значение «истина» (например, Определение. Формула выполнима, если она может принимать значение «истина» (например, ) Определение. Формула невыполнима, если ни при каких значениях составляющих ее высказываний она не может быть истинной (например, ). Определение. Формула общезначима, если она принимает значение «истина» независимо от истинности ее составляющих (например, ). Определение. Формула нейтральна, если она не общезначима и не является невыполнимой.

Определение. Тавтологиями называются общезначимые формулы. Если формула А≡1, т.е. А – тавтология, то это можно записать так

Определение (Логический вывод на основе множества гипотез). Пусть E – это множество формул, тогда запись означает, что если все формулы из Е истинны, то будет истинной формула А. В этом случае А – называется логическим следствием из Е. Если и E|=A , то можно записать Формулы называются гипотезами, а формула А – заключением.

Определение. Принцип дедукции состоит в следующем. Формула A является логическим следствием конечного множества Е тогда и только тогда, когда содержит невыполнимые формулы.

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

Действительно, если А есть логическое следствие гипотез ,то, учитывая сформулированный выше принцип дедукции, можно считать справедливой следующую запись: Это правило называется правилом прямой дедукции. Возьмем отрицание от этого выражения, тогда по правилу де Моргана получим Это правило называется правилом обратной дедукции.

МЕТОДЫ, ИСПОЛЬЗУЕМЫЕ ДЛЯ ОПРЕДЕЛЕНИЯ ОБЩЕЗНАЧИМОСТИ ФОРМУЛ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

Алгоритм редукции. Этот алгоритм позволяет доказывать общезначимость формул исчисления высказываний путем приведения к абсурду. Рассмотрим на примере. Пусть требуется доказать общезначимость следующей формулы: Алгоритм редукции. Этот алгоритм позволяет доказывать общезначимость формул исчисления высказываний путем приведения к абсурду. Рассмотрим на примере. Пусть требуется доказать общезначимость следующей формулы:

Предположим, что при некоторой интерпретации эта формула принимает значение «ложь». Из определения функции импликации известно, что значение «ложь» она принимает только в том случае, когда посылка истинна, а заключение ложно. Учитывая указанное свойство, представляем исходную формулу в виде двух интерпретаций следующего вида: Предположим, что при некоторой интерпретации эта формула принимает значение «ложь». Из определения функции импликации известно, что значение «ложь» она принимает только в том случае, когда посылка истинна, а заключение ложно. Учитывая указанное свойство, представляем исходную формулу в виде двух интерпретаций следующего вида:

Применив ранее использованные рассуждения к первой строке, получим следующие значения переменных: Применив ранее использованные рассуждения к первой строке, получим следующие значения переменных: Если подставить полученные значения во вторую строку, то получится противоречие. Значит, предположение о том, что существует некоторая интерпретация, при которой исходная формула принимает значение «ложь», неверно, и это означает общезначимость исходной формулы.

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

Тогда из первой формулы следует, что возможна одна из следующих комбинаций значений переменных a и b:

Из второй формулы следует Из второй формулы следует это означает, что возможны следующие значения c и a:

Из имеем c=1, b=0. Это единственно допустимые для c и b значения, при которых формула принимает значение «ложь». Сопоставляем полученные результаты с ранее рассмотренными возможными значениями переменных. Оказывается, что при с=1 единственное допустимое значение для a  это a=1, а при b=0 единственное допустимое значение a=0. Из имеем c=1, b=0. Это единственно допустимые для c и b значения, при которых формула принимает значение «ложь». Сопоставляем полученные результаты с ранее рассмотренными возможными значениями переменных. Оказывается, что при с=1 единственное допустимое значение для a  это a=1, а при b=0 единственное допустимое значение a=0. То есть переменная a должна принимать взаимно исключающие значения, что невозможно. Следовательно, предположение о существовании интерпретации, при которой формула принимает значение «ложь» неверно и это означает ее общезначимость.

Метод резолюций. Для порождения логических следствий будет использована очень простая схема рассуждений. Пусть A, B и X – формулы. Предположим, что две формулы истинны. Тогда, если X истина, то отсюда следует, что B тоже истина. Наоборот, если X – ложь, то следует, что A – истина. Получаем правило Метод резолюций. Для порождения логических следствий будет использована очень простая схема рассуждений. Пусть A, B и X – формулы. Предположим, что две формулы истинны. Тогда, если X истина, то отсюда следует, что B тоже истина. Наоборот, если X – ложь, то следует, что A – истина. Получаем правило , которое можно записать в виде .

В том частном случае, когда X – высказывание, а A и B – дизъюнкты, это правило называется правилом резолюций. В том частном случае, когда X – высказывание, а A и B – дизъюнкты, это правило называется правилом резолюций. Рассмотрим, каким образом это правило может быть использовано для построения доказательства. В методе резолюций применяется также приведенное выше правило прямой дедукции: для того чтобы доказать, что формула С является логическим следствием из гипотез H1,H2,…,Hn, следует доказать, что H1&H2&…&Hn& =0.

Так как левая часть последнего равенства представляет собой конъюнкцию, для его выполнения достаточно доказать равенство нулю любой входящей в уравнение формулы. Так как левая часть последнего равенства представляет собой конъюнкцию, для его выполнения достаточно доказать равенство нулю любой входящей в уравнение формулы. Таким образом, для доказательства выводимости исходной формулы С необходимо доказать, что в множестве {H1,H2,…,Hn, } имеется хотя бы одна невыполнимая формула. Для этого каждый элемент указанного множества рассматривается как элементарная дизъюнкция (дизъюнкт).

Применение метода резолюций предусматривает порождение новых дизъюнктов на основе следующей леммы, в основе которой лежит правило резолюций. Применение метода резолюций предусматривает порождение новых дизъюнктов на основе следующей леммы, в основе которой лежит правило резолюций. Лемма. Пусть S1 и S2 – дизъюнкты нормальной формы S, а l – литера. Если и , то дизъюнкт является логическим следствием нормальной формы S. Следствие. Нормальные формы S и эквивалентны. Замечание. Дизъюнкт r называется резольвентой дизъюнктов S1 и S2 .

Для доказательства приведенных выше утверждений о выполнимости формулы С необходимо, как отмечалось выше, доказать, что хотя бы один дизъюнкт из рассматриваемого множества исходных и порожденных дизъюнктов тождественно равен нулю. В этом случае говорят, что получен пустой дизъюнкт.

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

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

Определение. Литера  это элементарное высказывание или его отрицание. Например, Определение. Литера  это элементарное высказывание или его отрицание. Например, . Определение. Дизъюнкт или элементарная дизъюнкция  это совокупность различных литер, связанных дизъюнктивной связью. Например, . Определение. Конъюнктивной нормальной формой (КНФ) некоторой формулы называется равносильная ей формула, представляющая конъюнкций элементарных дизъюнкций. Например, .

Так как для того, чтобы выражение в форме КНФ было тождественно истинным, необходимо и достаточно, чтобы был истиной каждый дизъюнкт в него входящий, то при построении логического вывода можно перейти от КНФ к множеству дизъюнктов, в котором каждый элемент множества имеет значение «истинно». Так как для того, чтобы выражение в форме КНФ было тождественно истинным, необходимо и достаточно, чтобы был истиной каждый дизъюнкт в него входящий, то при построении логического вывода можно перейти от КНФ к множеству дизъюнктов, в котором каждый элемент множества имеет значение «истинно». Определение. Пустой дизъюнкт  это такой дизъюнкт, значение которого тождественно ложно.

Итак, невыполнимость формул, из которых формируется конечное множество дизъюнктов S, доказывается с помощью следующего алгоритма. Итак, невыполнимость формул, из которых формируется конечное множество дизъюнктов S, доказывается с помощью следующего алгоритма. Шаг 1. Проверка множества S на невыполнимость. Если пустой дизъюнкт принадлежит множеству S (он может либо присутствовать изначально или получается из-за того, что в множестве одновременно присутствует некоторая литера и ее отрицание), это означает, что множество S невыполнимо и алгоритм свою работу закончил. Иначе переходим на шаг 2.

Шаг 2. Построение резольвенты. Выбираем l, S1, S2, такие, что и и вычисляем резольвенту r. Если невозможно выбрать l, S1, S2, соответствующие указанным условиям, то алгоритм свою работу закончил и можно сказать, что исходное множество выполнимо. Иначе переходим на шаг 3. Шаг 2. Построение резольвенты. Выбираем l, S1, S2, такие, что и и вычисляем резольвенту r. Если невозможно выбрать l, S1, S2, соответствующие указанным условиям, то алгоритм свою работу закончил и можно сказать, что исходное множество выполнимо. Иначе переходим на шаг 3.

Шаг 3. Обновление множества дизъюнктов. Заменяем множество дизъюнктов , т.е. добавляем к существующим дизъюнктам новый дизъюнкт  резольвенту, полученную на предыдущем шаге. После чего переходим на шаг 1.

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

Порождаем логические следствия, при порождении следствия будем указывать, номера участвовавших в построении дизъюнктов: Порождаем логические следствия, при порождении следствия будем указывать, номера участвовавших в построении дизъюнктов:

Замечание. Алгоритм проверки невыполнимости недетерминирован. Вообще говоря, возможен не один вариант выбора значений для l, S1 и S2. В приведенном примере дизъюнкты выбирались в лексико-графическом порядке номеров. Такая стратегия не оптимальна, так как некоторые резольвенты оказались не нужны, а также вычислялись более одного раза. Этот же пример с минимумом резолюций будет выглядеть так: Замечание. Алгоритм проверки невыполнимости недетерминирован. Вообще говоря, возможен не один вариант выбора значений для l, S1 и S2. В приведенном примере дизъюнкты выбирались в лексико-графическом порядке номеров. Такая стратегия не оптимальна, так как некоторые резольвенты оказались не нужны, а также вычислялись более одного раза. Этот же пример с минимумом резолюций будет выглядеть так: Ясно, что принятая стратегия может существенно влиять на процесс выполнения алгоритма. Тем не менее существуют два свойства, не зависящие от используемой стратегии.

Свойство 1. Если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо (за исключением случая, когда оно содержит пустой дизъюнкт). Свойство 2. Если выполнение этого алгоритма закончилось нормально после порождения пустого дизъюнкта, то установлена невыполнимость исходного множества S. В заключение рассмотрим несколько примеров применения метода резолюций в логике высказываний.

Пример. Доказать, используя метод резолюций, что S является логическим следствием множества гипотез H, где Пример. Доказать, используя метод резолюций, что S является логическим следствием множества гипотез H, где , а . Сначала преобразуем множество гипотез в множество дизъюнктов:

Для доказательства того, что H |= S необходимо и достаточно доказать невыполнимость следующего множества дизъюнктов Для доказательства того, что H |= S необходимо и достаточно доказать невыполнимость следующего множества дизъюнктов

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

Введем следующие обозначения для высказываний: Введем следующие обозначения для высказываний: g – встать рано; d – играть в преферанс; с – идти на первую пару; s – лечь поздно спать; e – мало спать. Используя введенные обозначения, перейдем от утверждений к следующему набору гипотез: , , .

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

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