Исчисление высказываний
Исчисление высказываний представляет собой логику неанализируемых предположений, в которой пропозициональные константы могут рассматриваться как представляющие определенные простые выражения вроде "Сократ – мужчина" и "Сократ смертен". Строчные литеры р, q, r,… в дальнейшем будут использоваться для обозначения пропозициональных констант, которые иногда называют атомарными формулами, или атомами.
Ниже приведены все синтаксические правила, которые используются для конструирования правильно построенных формул (ППФ) в исчислении высказываний.
(S. U) ЕслиU является атомом, то у является ППФ.
(S) Если U является ППФ, то – U также является ППФ.
(S .v) Если U и ф являются ППФ, то (U u ф) также является ППФ.
В этих правилах строчные буквы греческого алфавита (например, U и ф) представляют пропозициональные переменные, т.е. не атомарные формулы, а любое простое или составное высказывание. Пропозициональные константы являются частью языка высказываний, который используется для приложения исчисления пропозициональных переменных к конкретной проблеме.
Выражение – U читается как "не U, а (U v ф) читается как дизъюнкция "U или ф (или оба)". Можно ввести другие логические константы – "л" (конъюнкция), "D" (импликация, или обусловленность), "=" (эквивалентность, или равнозначность), которые, по существу, являются сокращениями комбинации трех приведенных выше констант..
(U ^ ф) Эквивалентно(U v ф). Читается "U и ф".
(U 
ф) Эквивалентно (U v ф). Читается "U имплицирует ф".
(U==ф) Эквивалентно (U ф)^(ф U). Читается "U эквивалентно ф".
В конъюнктивной нормальной форме исчисления высказываний константы "импликация" и "эквивалентность" заменяются константами "отрицание" и "дизъюнкция", а затем отрицание сложного выражения раскрывается с помощью формул Де Моргана:
(U^ф) преобразуется в (Uvф), (U v ф) преобразуется в (-U^ф), U преобразуется в U.
Последний этап преобразований – внесение дизъюнкций внутрь скобок: (£ v (U ^ф))) заменяется ((£vU\(U)^(£vф)).
Принято сокращать вложенность скобочных форм, отбрасывая в нормальной конъюнктивной форме знаки операций v и л. Ниже представлен пример преобразования выражения, содержащего импликацию двух скобочных форм, в нормальную конъюнктивную форму.
(pvq) (-p^A-q) Исходное выражение.
(pvg)v(-p^ -q) Исключение~.
(pvq)v(-p^ -q) Ввод – внутрь скобок.
(pv(pvq))v(pv(pvq)) Занесение v внутрь скобок.
{{-p, р, q}, {q, р, q} } Отбрасывание А и v в конъюнктивной нормальной форме.
Выражения во внутренних скобках – это либо атомарные формулы, либо негативные атомарные формулы. Выражения такого типа называются литералами, причем с точки зрения формальной логики порядок литералов не имеет значения. Следовательно, для представления множества литералов – фразы – можно позаимствовать из теории множеств фигурные скобки. Литералы в одной и той же фразе неявно объединяются дизъюнкцией, а фразы, заключенные в фигурные скобки, неявно объединяются конъюнкцией.
Фразовая форма очень похожа на конъюнктивную нормальную форму, за исключением того, что позитивные и негативные литералы в каждой дизъюнкции группируются вместе по разные стороны от символа стрелки, а затем символ отрицания отбрасывается. Например, приведенное выше выражение преобразуется в две фразы: p,q<q.
В которых позитивные литералы сгруппированы слева от знака стрелки, а негативные справа.
Более строго, фраза представляет собой выражение, в котором p1…, рт q1,…, qn являются атомарными формулами, причем т › 0 и n › 0. Атомы в множестве р1,…, рт представляют заключения, объединенные операторами дизъюнкции, а атомы в множестве q1 …, qn – условия, объединенные операторами конъюнкции.