Заключение. 
Аналитическое и формальное доказательство теоремы в ИВ

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

Для метода пропозициональной резолюции приводится программа и результат выполнения программы для курсового задания.

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