Метод резолюций и предваренная нормальная форма

[alex_dorin]

Обязательно ли приведение формул к предваренной нормальной форме для
применения метода резолюций для логики предикатов ?

[cyb12]

Основная идея метода резолюций заключается в построении системы дизъюнктов и проверки ее на противоречивость. Система дизъюнктов строится из сколемовской стандартной формы (это ПНФ, у которой все кванторы - кванторы всеобщности). А ее без ПНФ не построить... Таков метод просто.