Процедура резолюції

Доведення чи спростування формули називають логічним виведенням (висновком). Вважається, що в процесі виведення використовуються лише раніше набуті формалізовані знання, а не нові експерименти та спостереження. У сучасних системах автоматизації логічного виведення використовується метод резолюцій. У процедурі резолюції замість заданої формули F, яка вважається тотожньо істинною, розглядають її заперечення та намагаються довести його несперечливість. Це – доведенням від протилежного. В його основі – операція виключення з різних пропозицій висловлювань-резольвент, якщо ці висловлювання водних реченнях заперечуються, а в інших – ні. Потрібна суперечливість встановлюється як одночасна справедливість двох взаємовиключних висловлювань. Якщо процес виведення резольвент обірветься, не призвівши до суперечності, то вихідна теорема є невірною. Перевагою методу резолюцій є можливість виявлення суперечності значно раніше, ніж буде виконано повний перебір можливостей. Нині розроблена велика кількість евристичних покращень спрямованості, тим самим і швидкодія методу.