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