Математическая логика - наука о правильных математических рассуждениях, о математическом мышлении. Впервые правила рассуждений систематизировал Аристотель. Однако как наука математическая логика сложилась лишь в середине Х
IX века, когда Джордж Буль ввел логические связки и исчисление высказываний. Современная математическая логика изучает: а) структуру математических высказываний, б) исходные постулаты математики (аксиомы и правила вывода),
в) математические доказательства (выводы), г) истинные математические утверждения (теоремы, леммы).
Одной из основных задач математической логики является формализация понятия доказательства.
В данной работе описывается система, позволяющая автоматически находить решения для определенного класса задач. Теоретическая база, на которую опирается система, это в основном работа [4], полезны также книги [1,2,3,8,9]. При описании системы поиска доказательств было решено выделить и описать отдельно три независимые части. В первой части приводятся основные понятия математической логики: формулы исчисления высказываний, равнозначность формул, построение конъюнктивно - нормальной формы. Вводится понятие логического следствия и формулируются теоремы о логическом следствии. Вторая часть посвящена проблеме формализации процесса доказательства. Вводится понятие резольвенты. Описывается метод резолюций. Приводятся и обосновываются правила сокращения множества дизъюнктов. Третья часть содержит общее описание системы и несколько примеров ее использования. Все определения, теоремы и методы иллюстрируются различными примерами.
Изложенный материал использовался ии занятий по математической логике и методам решения задач искусственного интеллекта как со старшеклассниками специализированных классов при математико-механическом факультете СПбГУ, так и со студентами. Описываемая система использовалась на занятиях в компьютерном классе.
Данная работа выполнена при поддержке Федеральной целевой программы "Государственная поддержка интеграции высшего образования и фундаментальной науки на 1997-2000 г.г.". Регистрационный №326.53.