Эвристические приемы поиска вывода в натуральном исчислении высказываний.

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

 

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

 

Типы исчислений:

1. Аксиоматические. Исходные дедуктивные постулаты – аксиомы и правила вывода.

2. Натуральные исчисления (естественные) Их задача – моделировать естественные способы рассуждения, делая их корректными. Процедура поиска вывода в них проще чем в аксиоматических исчислениях. Формальные отличия от аксиоматических исчислений – нет аксиом. В качестве дедуктивных постулатов только правила вывода.

 

Алгоритм создания исчисления:

1) Задается формальный язык

2) Задаются начальные постулаты

3) Задаются принципы и определения вывода

4) Задаются принципы и определения доказательства

5) Определяется отношение выводимости

6) Выявляется класс теорем (доказуемых формул)

 

Построение классического исчисления высказываний:

1) Использующийся формальный язык – язык классической логики высказываний

2) Дедуктивные постулаты – правила перехода. Правила перехода бывают двух видов:

-Прямые – правила позволяющие переходить от одной или нескольких формул определенного типа к формулам определенного типа

А₁,А₂,…,А_n ├ В₁,В₂,…,В_n

 

- Непрямые – от утверждения о выводимости перейти к утверждения другой выводимости

Г, А ├ В

Г ├ А В

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

 

А, В -введение А&ВА&В -исключение

А&В конъюнкции А В конъюнкции

 

А В -введение А В, А -исключение

А В А В дизъюнкции В дизъюнкции

 

В -введение А В, А -исключение

С В импликации В импликации

 

В, В -введение А -исключение

С отрицания А отрицания

где С – последнее из неисключенных допущений

 

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

3) Выводы

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

Вывод формулы А из Г – вывод из Г, последняя формула которого совпадает с А

4) Доказательства

Доказательство формулы А – вывод формулы А из пустого множества неисключенных допущений.

5) Выводимость

Формула А выводима из Г, если существует вывод из Г, последняя формула которого совпадает с А

6) Теоремы

Формула А называется теоремой, если ее возможно доказать в классическом исчислении высказываний

 

Эвристические приемы поиска вывода в натуральном исчислении высказываний.

 

Эвристики – подсказки, советы по выбору принципов рассуждения при поиске вывода

 

Если требуется построить вывод А₁,А₂,…,А_n ├ В, то стратегия в общем виде такова:

Допущения – А₁,А₂,…,А_n

Цель – В

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

1. импликативная формула С В. В этом случае прямой вывод:

Допущения – антецедент С

Цель – консеквент В

По правилу введения получаем С В

1. формула с отрицанием С. В этом случае док-во от противного:

Допущения – С

Цель – противоречие В и В

По правилу введения получаем С

Вспомогательные операции. Применяются только после 1 и 2 эвристик:

1. Если имеется дизъюнктивная формула А В или отрицание дизъюнкции (А В)

Допущения – А (в первом случае) или А (во втором случае)

Цель в первом случае – В

Цель во втором случае – противоречие путем введения к А

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

1. Если в выводе имеетсяимпликативная формула А В

Допущения - А

Цель – противоречие

После получения противоречия мы получаем формулу А, снимая отрицание получаем А, после чего по исключению получаем В

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

имена – знаки аргументов функций

предикаторы – знаки самих функций

предметные функторы – знаки предметных функций

логические связки – знаки истинностно-истинных функций