Выводимость формулы B из множества посылок F1; F2; … Fn равносильна доказательству теоремы ├─ (F1 & F2 & … & Fn B). Используя правила эквивалентных преобразований алгебры высказываний, формулу теоремы можно преобразовать так: ├─ (F1 & F2 & … & Fn B) = ((F1 & F2 & … & Fn) B) = (F1 & F2 & … & Fn & B). Т. е. заключение B является логическим следствием посылок F1; F2; … Fn т. и только т., когда формула теоремы (F1 & F2 & … & Fn & B) противоречива, т. е. имеет значение false. Сведения доказательства теоремы к противоречию на формуле, представленной в КНФ, составляет основу принципа резолюции.Для вывода по принципу резолюции необходимо:1) допустить отрицание заключения, т. е. B (известный способ доказательства от противного);2) привести все формулы (посылки и заключение) к КНФ;3) выписать множество дизъюнктов S = {D1; D2; … Dk};4) выполнить анализ всех пар множества S по правилу: “если существуют контрарные пары, один элемент которой Di содержит литеру A, а другой элемент Dj – A, то соединить эту пару логической связкой дизъюнкции (Di Dj), исключив контрарные литеры A и A: в результате этой операции получен новый дизъюнкт – резольвента, которую нужно включить в множество исходных дизъюнктов (п. 3); продолжая процедуру соединения дизъюнкт, устранить все контрарные пары; если в результате соединения всех дизъюнктов и резольвент будет получена пустая резольвента - , то вывод окончен и доказательство подтвердило противоречие.