Студопедия

Главная страница Случайная лекция

Порталы:

БиологияВойнаГеографияИнформатикаИскусствоИсторияКультураЛингвистикаМатематикаМедицинаОхрана трудаПолитикаПравоПсихологияРелигияТехникаФизикаФилософияЭкономика






Исчисление секвенций

Читайте также:
  1. Аксиоматическое исчисление высказываний
  2. Вопрос Порядок исчисление и уплаты налога на имущество в НКО, порядок применения льгот.
  3. Дифференциальное исчисление функций многих переменных
  4. Интегральное исчисление функций многих переменных и элементы векторного анализа.
  5. Исчисление амортизационных отчислений
  6. Исчисление предикатов
  7. Исчисление секвенций в PL
  8. Исчисление средней сезонной волны из процентных отношений уровней
  9. Исчисление сроков.

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

Ключевым фактом здесь является теорема о дедукции: если Г, А├ В, то Г├А®В. Этот факт записывается в виде вспомогательного правила вывода:

Доказательство общезначимости секвенций в исчислении предикатов, как и в исчислении высказываний, строится с использованием схемы аксиом и правил вывода. Изучение системы исчисления секвенций, названной естественной дедуктивной системой (Logische Kalkul), было начато Г. Генценом в 1934 году. В этой системе логические аксиомы формализованы, а преобразования формул не выполняются. Вместо этого используется большое число правил вывода, которые представляют собой стройную систему, подходящую для проведения обратного вывода.

Название «естественная дедуктивная система» введено для того, чтобы отличить ее от системы выводов на основе резолюций. Это основная система выводов в логике предикатов, в которой функционируют как единое целое группы правил вывода и логические аксиомы. В системе с малым числом правил вывода обычно имеется большое число логических аксиом, и наоборот. Рассмотрим систему исчисления секвенций.

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

Как и в исчислении высказываний, мы будем рассматривать кроме формул выражения вида, Г |- A, называемые секвенциями где |- - символ секвенции, Г - последовательность формул, которая может быть пустой, A - формула.


<== предыдущая страница | следующая страница ==>
Общезначимые эквивалентности логики предикатов | Правила вывода в исчислении предикатов

Дата добавления: 2014-11-08; просмотров: 606; Нарушение авторских прав


lektsiopedia.org - Лекциопедия - 2013 год. | Страница сгенерирована за: 0.007 сек.