Если в результате приведения к виду ПНФ матрица формулы M не будет содержать свободных переменных и сколемовских функций, то для вывода заключения полностью применим принцип резолюции исчисления высказываний (см. вопрос 9). Необходимо сформировать из матрицы множество дизъюнктов и сравнивая контрарные литеры получить пустую резольвенту .В результате приведения формулы к виду ССФ матрица формулы будет содержать сколемовские функции, где для получения контрарных литер необходимо выполнить операцию подстановки и замены термов предикатов.Т. о. главной проблемой принципа резолюции в исчислении предикатов является замена и подстановка термов. В случае решения этой задачи принцип резолюции применим также, как в исчислении высказываний.Принцип резолюции является более эффективной процедурой вывода, нежели дедуктивный вывод (процедура Эрбрана). Но он страдает существенным недостатком в формировании множества излишних и ненужных резольвент.