В чём заключается метод резолюции в логике первого порядка?

Метод резолюции в логике первого порядка заключается в попытке вывести из множества дизъюнктов пустой дизъюнкт, для которого нет интерпретаций и который тем самым гарантирует невыполнимость множества дизъюнктов. studfile.net

Алгоритм метода предполагает последовательное порождение резольвент от различных пар родительских дизъюнктов до тех пор, пока не будет получен пустой дизъюнкт. vec.etu.ru Это означает, что множество невыполнимо и тем самым логическое следствие доказано. vec.etu.ru Если пустой дизъюнкт получить не удастся, то множество является выполнимым и значит, что логическое следствие не имеет места. vec.etu.ru

Основная идея метода заключается в том, что если пара исходных дизъюнктов множества содержит контрарную литералу, то новый дизъюнкт формируется из оставшихся частей дизъюнктов, не содержащих эти контрарные литералы. studfile.net Этот вновь сформированный дизъюнкт называется резольвентой исходных дизъюнктов. studfile.net