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