Предваренная нормальная форма. Скулемизация. Метод резолюций для исчисления предикатов. Теорема о полноте исчисления предикатов. Множество тавтологий является неразрешимым перечислимым множеством.