Четкое изложение основных концепций теории доказательств в математической логике читатель найдет в работе Эндрюса [Andrews, 1986]. Я также рекомендую познакомиться с книгой [Quine, 1979] — переизданием классического труда, опубликованного впервые еще в 1940 году. Достаточно обширное введение в проблематику автоматического формирования суждений содержится в книге Робинсона [Robinson, 1979].
Более популярное изложение этого материала с упором на проблематику искусственного интеллекта можно найти в работе [Genesereth andNilsson, 1987, Chapters 1-5]. Обсуждение проблем математической логики в контексте искусственного интеллекта содержится в статье Хейеса и Мичи [Hayes and Michie, 1984]. Новой работой в этой области является книга Гинзберга [Ginsberg, 1993].