Скачать 13.21 Кбайт
Обратный метод С.Ю. Маслова
Т.е. в первом случае происходит расщепление исходного благоприятного набора, или расщепление по контрарной паре литер, а во втором — расщепление по дизъюнкту 2 исходной формулы Ф.
Пример 1
1. 31 (22) 1. 22 (31)
2. 33 (1) 2. 21 51
3. 32 63 3. 51 (2, 31)
4. 63 (22 ,1, 3) 4. 42 52
5. 61 (22) 5. 42 (2, 31, 5)
6. 62 (10) 6. 21 41
7. (22 ,1, 3, 6) 7. 21 (2, 31, 5, 4)
8. (2, 31, 5, 4)
========================================
16. (--) (1, 2, 3, 4, 5, 6)
Пример 2
1. 31 (22) 1. 41 (21)
2. 33 (1) 2. 51 (21)
3. 32 63 3. 42 52
4. 63 (22 ,1, 3) 4. 42 (21, 5)
5. 61 (22) 5. (21, 5, 4)
6. 62 (10)
7. (22 ,1, 3, 6)
========================================
13. (--) (1, 2, 3, 4, 5, 6)
ЛИТЕРАТУРА:
1. Воронков А.А., Дегтярев А.Н. Автоматическое доказательство теорем //Кибернетика, 1986 No 3, 1987 No 4.
2. Логическое программирование"(сб. переводов по ред. В.Н. Агафонова). М., 1988.
3. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, Т.98, 1968.
4. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М., 1983.
5. Данцин Е.Я. Две системы тавтологичности, основанные на методе расщеплений //Записки научных семинаров ЛОМИ АН СССР, Т.105, 1981.
6. Давыдов Г.В. О корректировании недоказуемых формул //Записки научных семинаров ЛОМИ АН СССР, Т.4, 1967.
7. Давыдов Г.В. Синтез метода резолюций с обратным методом //Записки научных семинаров ЛОМИ АН СССР, Т.20, 1971.
8. Войшвилло Е.К. Символическая логика: классическая и релевантная. М., Высшая школа, 1989.
9. Математическая теория логического вывода (статьи Г. Генцена, С. Кангера, Э. Бэта). М., 1967
10. Гэри М.Г., Джонсон Д.С. ЭВМ и труднорешаемые задачи. М., 1982 г.
11. Машинный алгорифм естественного вывода в исчислении высказываний. М.-Л., 1965.
12. Вопросы кибернетики. Вып.131 (проблемы сокращения перебора). М., 1987.
13. Катречко С.Л. Модификации обратного метода С.Ю. Маслова //Материалы X Всесоюзной конференции по логике, методологии и философии науки. М., 1990.
14. Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991.
--------------------------------------------------------------------------------
[1] Данный текст «расширен» за счет фрагмента из более ранней работы [14] (Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991). == см. фрагмент ниже в разделе «ДОПОЛНЕНИЕ».
Пример 1
1. 31 (22) 1. 22 (31)
2. 33 (1) 2. 21 51
3. 32 63 3. 51 (2, 31)
4. 63 (22 ,1, 3) 4. 42 52
5. 61 (22) 5. 42 (2, 31, 5)
6. 62 (10) 6. 21 41
7. (22 ,1, 3, 6) 7. 21 (2, 31, 5, 4)
8. (2, 31, 5, 4)
========================================
16. (--) (1, 2, 3, 4, 5, 6)
Пример 2
1. 31 (22) 1. 41 (21)
2. 33 (1) 2. 51 (21)
3. 32 63 3. 42 52
4. 63 (22 ,1, 3) 4. 42 (21, 5)
5. 61 (22) 5. (21, 5, 4)
6. 62 (10)
7. (22 ,1, 3, 6)
========================================
13. (--) (1, 2, 3, 4, 5, 6)
ЛИТЕРАТУРА:
1. Воронков А.А., Дегтярев А.Н. Автоматическое доказательство теорем //Кибернетика, 1986 No 3, 1987 No 4.
2. Логическое программирование"(сб. переводов по ред. В.Н. Агафонова). М., 1988.
3. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, Т.98, 1968.
4. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М., 1983.
5. Данцин Е.Я. Две системы тавтологичности, основанные на методе расщеплений //Записки научных семинаров ЛОМИ АН СССР, Т.105, 1981.
6. Давыдов Г.В. О корректировании недоказуемых формул //Записки научных семинаров ЛОМИ АН СССР, Т.4, 1967.
7. Давыдов Г.В. Синтез метода резолюций с обратным методом //Записки научных семинаров ЛОМИ АН СССР, Т.20, 1971.
8. Войшвилло Е.К. Символическая логика: классическая и релевантная. М., Высшая школа, 1989.
9. Математическая теория логического вывода (статьи Г. Генцена, С. Кангера, Э. Бэта). М., 1967
10. Гэри М.Г., Джонсон Д.С. ЭВМ и труднорешаемые задачи. М., 1982 г.
11. Машинный алгорифм естественного вывода в исчислении высказываний. М.-Л., 1965.
12. Вопросы кибернетики. Вып.131 (проблемы сокращения перебора). М., 1987.
13. Катречко С.Л. Модификации обратного метода С.Ю. Маслова //Материалы X Всесоюзной конференции по логике, методологии и философии науки. М., 1990.
14. Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991.
--------------------------------------------------------------------------------
[1] Данный текст «расширен» за счет фрагмента из более ранней работы [14] (Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991). == см. фрагмент ниже в разделе «ДОПОЛНЕНИЕ».
|
|