|
|
|
|
Литература
|
|
| |
| 1. |
А. Г. Драгалин, Математический интуиционизм. Введение в теорию доказательств, Наука, М., 1979  |
| 2. |
С. К. Клини, “Перестановочность применений правил в генценовских исчислениях LK и LJ”, Математическая теория логического вывода, Наука, М., 1967 |
| 3. |
С. К. Клини, Математическая логика, Мир, М., 1973 |
| 4. |
Б. Ю. Конев, “Уточнение оценок высоты термов в наиболее общем унификаторе”, Зап. научн. семинаров ПОМИ, 241, 1997, 117–134   |
| 5. |
Б. Ю. Конев, “Верхняя оценка высоты термов в выводах с сечениями по формулам ограниченной глубины связанных вхождений”, Зап. научн. семинаров ПОМИ, 277, 2001, 80–103 |
| 6. |
Г. Е. Минц, В. П. Оревков, “О погружающих операциях”, Зап. научн. семинаров ПОМИ, 4, 1967, 163–175 |
| 7. |
В. П. Оревков, “О гливенковских классах секвенций”, Тр. Матем. ин-та АН СССР, 98, 1968, 131–154 |
| 8. |
В. П. Оревков, “Нижние оценки увеличения сложности выводов после устранения сечений”, Зап. научн. семинаров ПОМИ, 88, 1979, 137–162 |
| 9. |
V. P. Orevkov, Complexity of proofs and their transformations in axiomatic theories, Amer. Math. Soc., 1993 |
| 10. |
R. Harrop, “Concering formulas of types $A\rightarrow B\vee C, A\rightarrow\exists xB(x)$”, J. Symbolic Logic, 25:1 (1960), 27–32  |
| 11. |
R. Statman, The predicate calculus is not a Kalmar elementary speed-up of the equation calculus, Cambbridge, 1975 |
| 12. |
R. Statman, “Bounds for proof-search and speed-up in the predicate calculus”, Ann. Math. Logic, 15 (1978), 225–287 |
