Ответы на экзаменационные вопросы. Введение

Алгоритм отыскания СКНФ:

.

1.7. Формализованное исчисление высказываний

Исчисление высказываний – это формальная теория L, в которой определены следующие компоненты:

1. Алфавит:

,  есть логические связки;

( , ) есть служебные символы;

X₁,X₂,…,X_n есть пропозициональные переменные.

2. Формулы:

3. Аксиомы (схемы аксиом):

А1: (F(GF));

А2: ((F(GH))((FG)(FH)));

А3: ((G  F)((GF)G)),

где F, G, H –произвольные формулы.

4. Правило вывода: Modus ponens (правило отделения).

Здесь F и G – любые формулы.

Таким образом, множество аксиом теории L бесконечно, хотя задано 3-мя схемами аксиом. Множество правил вывода также бесконечно, хотя оно задано только одной схемой.

При записи формул лишние скобки опускаются, если это не вызывает недоразумений. Другие связки вводятся определениями (но не аксиомами):

Любая формула, содержащая эти связки, рассматривается как синтаксическое сокращение собственной формулы теории L.

1.8. Теорема о дедукции