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