После того, как все наборы второго поколения построены, переходим к наборам третьего поколения. Так продолжается до тех пор, пока мы не построим пустой набор (тогда ДНФ общезначима). Если на каком-то этапе мы не можем построить ни один новый набор, то можно сделать вывод о необщезначимости ДНФ.

В нашем случае наборы 1 — 8 будут наборами 0-го поколения, наборы 9, 10, 13, 14 — наборами первого поколения. Набор 11 будет набором второго поколения и будет построен только после 14-го. Можно заметить, что применение этой тактики в нашем случае неэффективно: тактика при небольших формулах (глубина вывода которых не превышает 3 шага) несколько тормозит работу программы, но дает существенный выигрыш при больших формулах.

============

— данный текст (в соавторстве с Царьков Д.В.) подготовлен в качестве итогового научного отчета по гранту РГНФ № 096-03-04143 (исследовательский проект "От логических исчислений к интеллектуальным системам").

Литература:
1. Гэри М.Г., Джонсон Д.С. ЭВМ и труднорешаемые задачи. — М.: Мир, 1982.

2. Пойа Д. Как решать задачу. — М.: Учпедгиз, 1959.

3. Ван Хао На пути к механической математике //Кибернетический сборник, 1962 № 5. С. 114 - 165.

4. Кангер С. Упрощенный метод доказательства для элементарной логики //Математическая теория логического вывода. — М.: Наука, 1967. С. 200 - 208.

5. Маслов С.Ю. Теория дедуктивных систем и ее применения. — М.: Радио и связь, 1986.

6. Серебрянников О.Ф. Эвристические принципы и логические исчисления. — М.: Наука, 1970.

7. Смирнов В.А. Формальный вывод и логические исчисления. — М.: Наука, 1972.

8. Катречко С.Л. Бесконечность и теория поиска вывода //Бесконечность в математике: философские и исторические аспекты. — М., «Янус-К», 1997.

9. Weyhrauch R.W. Prolegomena to a theory of mechanized formal reasoning //Artificial Intelligence, 1980, Vol. 13. P. 133 - 170.

10. Катречко С.Л. Исчисление поиска вывода с «условной дизъюнкцией» //XI Международная конференция "Логика, методология, философия науки», Т.2. Москва — Обнинск, 1995.

11. Черч А. Введение в математическую логику. — М.: ИЛ., 1960

12. Сидоренко Е.А. Пропозициональное исчисление с условной дизъюнкцией //Методы логического анализа. — М.: Наука,1977. С. 150 - 159.

13. Катречко С.Л. От логики к теории поиска вывода //Международная конференция «Развитие логики в России: итоги и перспективы», М., 1997.

14. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний //Н.А. Шанин, Г.В. Давыдов, С.Ю. Маслов и др. — М. — Л., Наука, 1965.

15. Давыдов Г.В. Некоторые замечания о поиске вывода в исчислении предикатов //Записки научных семинаров ЛОМИ АН СССР, 1968. Т.8. С.8 - 20.

16. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, 1968, Т.98. С.26 - 87.

17. Робинсон Дж. Машинно — ориентированная логика, основанная на принципе резолюции //Кибернетический сборник (новая серия). 1970. Вып.7. С.194 - 218.

18. Данцин Е.Я. Две системы тавтологичности, основанные на методе расщеплений //Записки научных семинаров ЛОМИ АН СССР, Т.105. Л., 1981.

19. Катречко С.Л. Модификация обратного метода С.Ю.Маслова //Материалы Х Всесоюзной конференции по логике, методологии и философии науки. — Минск, 1990. С.110 - 112.

20. Катречко С.Л. Моделирование правила расщеплений в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках. — М., ИФРАН, 1992, С. 125 -141.

21. Катречко С.Л. Обратный метод С. Ю. Маслова //Логика и компьютер (вып.2): логические языки, содержательные рассуждения и методы поиска доказательства. — М., Наука, 1995. С.62 - 75.

22. Царьков Д.В., Катречко С.Л. Об одном алгоритме приведения пропозициональных формул к д. н. ф //Тезисы международной конференции (1-ые) «Смирновские чтения», Москва, 1997.

23. Царьков Д.В. Новый алгоритм преобразования формул в Д. Н. Ф //Тезисы международной конференции «Развитие логики в России: итоги и перспективы», Москва, 1997.

24. Интеллектуальный бектрекинг //Логические исследования, Вып.3. — М., Наука, 1995.

25. Katrechcko S.L. Frege's system and proof-search theory //Abstacts of Russian conference "Frege's and Hilbert's heritage in the XX-th centure: logic, philosophy and mathematics", Kaliningrad, 1992. P.7 - 8.

26. Логика и компьютер. Вып.3. — М., Наука, 1996.