Книга посвящена рассмотрению проблемы автоматического поиска теорем для классической и интуиционистской логик.
В ней предлагаются построенные авторами алгоритмы поиска доказательства для натуральных исчислений классической и интуиционистской логик высказываний, а также для натурального первопорядкового исчисления предикатов.
Относительно этих алгоритмов доказываются метатеоремы об их непротиворечивости и полноте. Это и многое другое вы найдете в книге Логика и компьютер. Выпуск 5. Пусть докажет компьютер