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

Категория: Математика

Нажмите для полного просмотра!
Общие сведения о формальных и аксиоматических системах, слайд №1Общие сведения о формальных и аксиоматических системах, слайд №2Общие сведения о формальных и аксиоматических системах, слайд №3Общие сведения о формальных и аксиоматических системах, слайд №4Общие сведения о формальных и аксиоматических системах, слайд №5Общие сведения о формальных и аксиоматических системах, слайд №6Общие сведения о формальных и аксиоматических системах, слайд №7Общие сведения о формальных и аксиоматических системах, слайд №8Общие сведения о формальных и аксиоматических системах, слайд №9Общие сведения о формальных и аксиоматических системах, слайд №10Общие сведения о формальных и аксиоматических системах, слайд №11Общие сведения о формальных и аксиоматических системах, слайд №12Общие сведения о формальных и аксиоматических системах, слайд №13Общие сведения о формальных и аксиоматических системах, слайд №14Общие сведения о формальных и аксиоматических системах, слайд №15Общие сведения о формальных и аксиоматических системах, слайд №16Общие сведения о формальных и аксиоматических системах, слайд №17Общие сведения о формальных и аксиоматических системах, слайд №18Общие сведения о формальных и аксиоматических системах, слайд №19Общие сведения о формальных и аксиоматических системах, слайд №20Общие сведения о формальных и аксиоматических системах, слайд №21Общие сведения о формальных и аксиоматических системах, слайд №22Общие сведения о формальных и аксиоматических системах, слайд №23Общие сведения о формальных и аксиоматических системах, слайд №24Общие сведения о формальных и аксиоматических системах, слайд №25Общие сведения о формальных и аксиоматических системах, слайд №26Общие сведения о формальных и аксиоматических системах, слайд №27Общие сведения о формальных и аксиоматических системах, слайд №28Общие сведения о формальных и аксиоматических системах, слайд №29Общие сведения о формальных и аксиоматических системах, слайд №30Общие сведения о формальных и аксиоматических системах, слайд №31Общие сведения о формальных и аксиоматических системах, слайд №32Общие сведения о формальных и аксиоматических системах, слайд №33Общие сведения о формальных и аксиоматических системах, слайд №34Общие сведения о формальных и аксиоматических системах, слайд №35Общие сведения о формальных и аксиоматических системах, слайд №36Общие сведения о формальных и аксиоматических системах, слайд №37Общие сведения о формальных и аксиоматических системах, слайд №38Общие сведения о формальных и аксиоматических системах, слайд №39Общие сведения о формальных и аксиоматических системах, слайд №40Общие сведения о формальных и аксиоматических системах, слайд №41Общие сведения о формальных и аксиоматических системах, слайд №42Общие сведения о формальных и аксиоматических системах, слайд №43Общие сведения о формальных и аксиоматических системах, слайд №44Общие сведения о формальных и аксиоматических системах, слайд №45Общие сведения о формальных и аксиоматических системах, слайд №46Общие сведения о формальных и аксиоматических системах, слайд №47Общие сведения о формальных и аксиоматических системах, слайд №48Общие сведения о формальных и аксиоматических системах, слайд №49Общие сведения о формальных и аксиоматических системах, слайд №50Общие сведения о формальных и аксиоматических системах, слайд №51Общие сведения о формальных и аксиоматических системах, слайд №52Общие сведения о формальных и аксиоматических системах, слайд №53Общие сведения о формальных и аксиоматических системах, слайд №54Общие сведения о формальных и аксиоматических системах, слайд №55Общие сведения о формальных и аксиоматических системах, слайд №56Общие сведения о формальных и аксиоматических системах, слайд №57Общие сведения о формальных и аксиоматических системах, слайд №58Общие сведения о формальных и аксиоматических системах, слайд №59Общие сведения о формальных и аксиоматических системах, слайд №60Общие сведения о формальных и аксиоматических системах, слайд №61Общие сведения о формальных и аксиоматических системах, слайд №62Общие сведения о формальных и аксиоматических системах, слайд №63Общие сведения о формальных и аксиоматических системах, слайд №64Общие сведения о формальных и аксиоматических системах, слайд №65Общие сведения о формальных и аксиоматических системах, слайд №66Общие сведения о формальных и аксиоматических системах, слайд №67Общие сведения о формальных и аксиоматических системах, слайд №68Общие сведения о формальных и аксиоматических системах, слайд №69Общие сведения о формальных и аксиоматических системах, слайд №70Общие сведения о формальных и аксиоматических системах, слайд №71Общие сведения о формальных и аксиоматических системах, слайд №72Общие сведения о формальных и аксиоматических системах, слайд №73Общие сведения о формальных и аксиоматических системах, слайд №74Общие сведения о формальных и аксиоматических системах, слайд №75Общие сведения о формальных и аксиоматических системах, слайд №76Общие сведения о формальных и аксиоматических системах, слайд №77Общие сведения о формальных и аксиоматических системах, слайд №78Общие сведения о формальных и аксиоматических системах, слайд №79Общие сведения о формальных и аксиоматических системах, слайд №80Общие сведения о формальных и аксиоматических системах, слайд №81Общие сведения о формальных и аксиоматических системах, слайд №82Общие сведения о формальных и аксиоматических системах, слайд №83Общие сведения о формальных и аксиоматических системах, слайд №84Общие сведения о формальных и аксиоматических системах, слайд №85Общие сведения о формальных и аксиоматических системах, слайд №86Общие сведения о формальных и аксиоматических системах, слайд №87Общие сведения о формальных и аксиоматических системах, слайд №88Общие сведения о формальных и аксиоматических системах, слайд №89Общие сведения о формальных и аксиоматических системах, слайд №90Общие сведения о формальных и аксиоматических системах, слайд №91

Вы можете ознакомиться и скачать презентацию на тему Общие сведения о формальных и аксиоматических системах. Доклад-сообщение содержит 91 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.


Слайды и текст этой презентации

Слайд 1






§3. ОБЩИЕ СВЕДЕНИЯ О ФОРМАЛЬНЫХ И АКСИОМАТИЧЕСКИХ СИСТЕМАХ
Описание слайда:
§3. ОБЩИЕ СВЕДЕНИЯ О ФОРМАЛЬНЫХ И АКСИОМАТИЧЕСКИХ СИСТЕМАХ

Слайд 2



Определение

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

Слайд 3




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

Слайд 4




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

Слайд 5




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

Слайд 6




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

Слайд 7




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

Слайд 8



	Определение формальной системы осуществляется в следующем порядке:
	Определение формальной системы осуществляется в следующем порядке:

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

Слайд 9



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

Слайд 10



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

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

Слайд 11



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

Слайд 12




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

Слайд 13




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

Слайд 14



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

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

Слайд 15



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

Слайд 16



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

Слайд 17




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

Слайд 18



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

Слайд 19



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

Слайд 20



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

Слайд 21




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

Слайд 22




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

Слайд 23



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

Слайд 24



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

Слайд 25



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

Слайд 26




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

Слайд 27




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

Слайд 28




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

Слайд 29






§4.  ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ
Описание слайда:
§4. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Слайд 30



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

Слайд 31




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

Слайд 32



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

Слайд 33



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

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

Слайд 34



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

Слайд 35



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

Слайд 36



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

Слайд 37




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

Слайд 38



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

Слайд 39




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

Слайд 40
Общие сведения о формальных и аксиоматических системах, слайд №40
Описание слайда:

Слайд 41




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

Слайд 42



Пример
Описание слайда:
Пример

Слайд 43




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

Слайд 44



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

Слайд 45



             
             
2) правило подстановки. 



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

Слайд 46



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

Слайд 47




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

Слайд 48





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

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

Слайд 49



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


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

Слайд 50





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

Слайд 51



  

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

Слайд 52





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

Слайд 53




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

Слайд 54




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

Слайд 55



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

Слайд 56




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

Слайд 57



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

Слайд 58





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

Слайд 59




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

Слайд 60



	
	

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

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

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

Слайд 61






МЕТОДЫ, ИСПОЛЬЗУЕМЫЕ ДЛЯ ОПРЕДЕЛЕНИЯ ОБЩЕЗНАЧИМОСТИ  ФОРМУЛ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ
Описание слайда:
МЕТОДЫ, ИСПОЛЬЗУЕМЫЕ ДЛЯ ОПРЕДЕЛЕНИЯ ОБЩЕЗНАЧИМОСТИ ФОРМУЛ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

Слайд 62



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

Слайд 63



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

Слайд 64



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

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

Слайд 65



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

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

Слайд 66





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

Слайд 67



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

Слайд 68



	Из 			имеем 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 должна принимать взаимно исключающие значения, что невозможно. Следовательно, предположение о существовании  интерпретации, при которой формула 

принимает значение «ложь» неверно и это означает ее общезначимость.
Описание слайда:
Из имеем 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 должна принимать взаимно исключающие значения, что невозможно. Следовательно, предположение о существовании интерпретации, при которой формула принимает значение «ложь» неверно и это означает ее общезначимость.

Слайд 69



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

Слайд 70



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

Слайд 71



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

Слайд 72



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

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

Слайд 73



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

Слайд 74



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

Слайд 75



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

Слайд 76



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

Слайд 77



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

Слайд 78



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

Слайд 79



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

Слайд 80



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

Слайд 81



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

Слайд 82



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

Слайд 83



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




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

Слайд 84



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

Слайд 85



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

Слайд 86



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

Слайд 87



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

Слайд 88



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

Слайд 89



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

Слайд 90



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



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

Слайд 91
Общие сведения о формальных и аксиоматических системах, слайд №91
Описание слайда:



Похожие презентации
Mypresentation.ru
Загрузить презентацию