Выводы. 
Математическая логика

Глава посвящена логике вывода в исчислении высказываний. Анализ рассуждения и доказательство (логический вывод) являются главной задачей, решаемой логикой формально, и тем самым являются надежным доказательством истинности рассуждений и вывода.

Прежде всего любая строгая математическая теория базируется на аксиомах. Применяя к ним подстановки аксиом и правило вывода, гарантированно получаем теорему — тождественно истинный вывод. Построенная таким образом теория включает множество теорем. Прмерами таких теорий в математике являются геометрия Евклида, теория чисел и другие строгие математические теории.

Однако в приложениях вместо аксиом доступны истинные факты-гипотезы, не обязательно тождественно истинные (аксиомы), и правила, которые позволяют путем подстановок в формулы построить вывод и подтвердить истинность рассуждений и полученного результата-вывода. Такой подход принципиально меняет вывод, позволяя анализировать истинность рассуждений в самых разных приложениях. Формально определены известные, широко используемые методы прямого, обратного доказательств и доказательства от противоречий.

Правила вывода позволяют выполнить общие преобразования формул, которые могут завершаться выводами об истинности, противоречивости и выполнимости формул.

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

Рассмотренные в главе методы преобразования формул логики и вывода являются базой для дальнейшего расширения и развития классической логики и расширения приложений.