Метод резолюцій

1. Пустий диз’юнкт

2. Основні кроки зведення

2.1. Усунення імплікацій та тотожностей

2.2. Втягнення заперечень всередину (зведення до вигляду, коли всі заперечення знаходяться тільки над літералами) – на основі законів де Моргана

2.3. Перейменування змінних (щоб не було випадкового співпадіння імен змінних в області дії кванторів)

2.4. Зведення до нормальної форми: K1 … Kn M(x1, …, xn), де M - формула, яка містить тільки кон’юнкції та диз’юнкції атомарних формул і не містить кванторів, Ki - квантори

2.5. Усунення кванторів існування

2.6. Усунення кванторів узагальнення

2.7. Зведення до кон’юнктивної нормальної форми

2.8. Розділення кон’юнкцій

3. Атомарна формула

4. Літерал

5. Диз’юнкт