Метод резолюции исчислений предикатов

Метод резолюций опирается на исчисление резольвент. Существует теорема, утверждающая, что вопрос о доказуемости произвольной формулы в исчислении предикатов сводится к вопросу о доказуемости пустого списка в исчислении резольвент. Идея метода резолюций заключается в том, что доказательство истинности или ложности выдвинутого предположения ведется методом от противного. Для этого в исходное множество предложений включают аксиомы формальной системы и отрицание доказываемой гипотезы. Если в процессе доказательства возникает противоречие между отрицанием гипотезы и аксиомами, выражающееся в нахождении пустого списка (дизъюнкта), то выдвинутая гипотеза правильна.

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

В методе резолюций множество предложений обычно рассматривается как составной предикат, содержащий несколько предикатов, соединенных логическими функциями и кванторами существования и общности. Так как одинаковые по смыслу предикаты могут иметь разный вид, то предложения преобразуются в клаузальную форму – разновидность конъюнктивной нормальной формы (КНФ), в которой удалены кванторы существования, всеобщности, символы импликации, равнозначности и др.

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

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

Итак, если требуется методом резолюций доказать истинность какого-либо логического утверждения, то отрицание этого утверждения преобразуется в клаузальную форму, по его предложениям выполняется поиск пустого предложения с использованием унификации и вывода резольвент. Невыполнимость отрицания подтверждает истинность рассматриваемого утверждения.