Составители:
Рубрика:
3
Введение
Принцип резолюции – универсальный способ доказательства
утверждений. Наиболее широкое применение он находит при
доказательстве высказываний, сформулированных на языке
исчисления высказываний (ИВ) и исчисления предикатов (ИП).
В данной разработке ИВ и ИП вводятся как конкретизация
общего понятия формальной системы. Излагается ряд основных
результатов этих теорий, вводится понятие логического следствия;
устанавливается, что проблема
выводимости утверждения из набора
предпосылок сводится к доказательству невыполнимости
(противоречивости) некоторой конъюнктивной нормальной формы
(КНФ). Для доказательства противоречивости КНФ вводится и
изучается процедура резолюции, включая некоторые ее
модификации (линейную и семантическую резолюции).
Известно, что проблема противоречивости КНФ NР - полна.
Согласно естественнонаучной гипотезе Р
≠
МР, полиномиальных
решающих алгоритмов для нее не существует. Вместе с тем
выделяются частные классы КНФ, для которых удается построить
алгоритмы решения с полиномиальной верхней оценкой временной
вычислительной сложности.
При написании данной разработки использованы литературные
источники [1-4].
Понятие формальной системы
Формальная система (ФС) считается заданной, если определены
следующие ее компоненты: 1) алфавит
; 2) совокупность правильно
построенных формул; 3) множество аксиом; 4) множество правил
вывода.
Алфавит ФС включает конечное или бесконечное число
символов. Эти символы делятся на три группы – буквы, символы
операций и связок, вспомогательные символы (скобки различных
видов, запятые и т.д.). Количество символов связок, символов
операций и вспомогательных символов конечно, число букв может
быть
бесконечно за счет индексов, принимающих натуральные
значения.
Любую конечную последовательность символов алфавита
именуем формулой ФС. В совокупности формул ФС выделено
множество правильно построенных формул (ППФ). Для ППФ
задаются правила их конструирования и эффективная процедура,
позволяющая по каждой формуле ФС определить, является ли она
ППФ.
Введение
Принцип резолюции – универсальный способ доказательства
утверждений. Наиболее широкое применение он находит при
доказательстве высказываний, сформулированных на языке
исчисления высказываний (ИВ) и исчисления предикатов (ИП).
В данной разработке ИВ и ИП вводятся как конкретизация
общего понятия формальной системы. Излагается ряд основных
результатов этих теорий, вводится понятие логического следствия;
устанавливается, что проблема выводимости утверждения из набора
предпосылок сводится к доказательству невыполнимости
(противоречивости) некоторой конъюнктивной нормальной формы
(КНФ). Для доказательства противоречивости КНФ вводится и
изучается процедура резолюции, включая некоторые ее
модификации (линейную и семантическую резолюции).
Известно, что проблема противоречивости КНФ NР - полна.
Согласно естественнонаучной гипотезе Р ≠ МР, полиномиальных
решающих алгоритмов для нее не существует. Вместе с тем
выделяются частные классы КНФ, для которых удается построить
алгоритмы решения с полиномиальной верхней оценкой временной
вычислительной сложности.
При написании данной разработки использованы литературные
источники [1-4].
Понятие формальной системы
Формальная система (ФС) считается заданной, если определены
следующие ее компоненты: 1) алфавит; 2) совокупность правильно
построенных формул; 3) множество аксиом; 4) множество правил
вывода.
Алфавит ФС включает конечное или бесконечное число
символов. Эти символы делятся на три группы – буквы, символы
операций и связок, вспомогательные символы (скобки различных
видов, запятые и т.д.). Количество символов связок, символов
операций и вспомогательных символов конечно, число букв может
быть бесконечно за счет индексов, принимающих натуральные
значения.
Любую конечную последовательность символов алфавита
именуем формулой ФС. В совокупности формул ФС выделено
множество правильно построенных формул (ППФ). Для ППФ
задаются правила их конструирования и эффективная процедура,
позволяющая по каждой формуле ФС определить, является ли она
ППФ.
3
