U. Kohlenbach, P. Oliva, “Proof Mining: A Systematic Way of Analyzing Proofs in Mathematics”, Математическая логика и алгебра, Сборник статей. К 100-летию со дня рождения академика Петра Сергеевича Новикова, Труды МИАН, 242, Наука, МАИК «Наука/Интерпериодика», М., 2003, 147–175; Proc. Steklov Inst. Math., 242 (2003), 136

Труды Математического института имени В. А. Стеклова

RUS ENG

ЖУРНАЛЫ ПЕРСОНАЛИИ ОРГАНИЗАЦИИ КОНФЕРЕНЦИИ СЕМИНАРЫ ВИДЕОТЕКА ПАКЕТ AMSBIB

JavaScript is disabled in your browser. Please switch it on to enable full functionality of the website

	Общая информация
	Последний выпуск
	Скоро в журнале
	Архив
	Импакт-фактор
	Правила для авторов
	Лицензионный договор

	Поиск публикаций
	Поиск ссылок

	RSS
	Последний выпуск
	Текущие выпуски
	Архивные выпуски
	Что такое RSS

Труды МИАН:
Год:
Том:
Выпуск:
Страница:
	Найти

Персональный вход:
Логин:
Пароль:
	Запомнить пароль
	Войти
	Забыли пароль?
	Регистрация

Труды Математического института имени В. А. Стеклова, 2003, том 242, страницы 147–175 (Mi tm413)

Эта публикация цитируется в 39 научных статьях (всего в 39 статьях)

Proof Mining: A Systematic Way of Analyzing Proofs in Mathematics

U. Kohlenbach, P. Oliva

University of Aarhus

PDF полного текста (367 kB) Список цитирования (39)

Список литературы:

PDF

HTML

Аннотация: Proof mining is the process of logically analyzing proofs in mathematics with the aim of obtaining new information. In this survey paper, we discuss, by means of examples from mathematics, some of the main techniques used in proof mining. We show that these techniques apply not only to proofs based on classical logic but also to proofs that involve noneffective principles such as the attainment of the infimum of

$f\in C[0,1]$ and the convergence for bounded monotone sequences of reals. We also report on recent case studies in approximation theory and fixed point theory where new results were obtained.

Поступило в июне 2002 г.

Реферативные базы данных:

УДК: 510.6

Язык публикации: английский

Образец цитирования: U. Kohlenbach, P. Oliva, “Proof Mining: A Systematic Way of Analyzing Proofs in Mathematics”, Математическая логика и алгебра, Сборник статей. К 100-летию со дня рождения академика Петра Сергеевича Новикова, Труды МИАН, 242, Наука, МАИК «Наука/Интерпериодика», М., 2003, 147–175; Proc. Steklov Inst. Math., 242 (2003), 136–164

Цитирование в формате AMSBIB

\RBibitem{KohOli03}

\by U.~Kohlenbach, P.~Oliva

\paper Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics

\inbook Математическая логика и алгебра

\bookinfo Сборник статей. К~100-летию со дня рождения академика Петра Сергеевича Новикова

\serial Труды МИАН

\yr 2003

\vol 242

\pages 147--175

\publ Наука, МАИК «Наука/Интерпериодика»

\publaddr М.

\mathnet{http://mi.mathnet.ru/tm413}

\mathscinet{http://mathscinet.ams.org/mathscinet-getitem?mr=2054493}

\zmath{https://zbmath.org/?q=an:1079.03045}

\transl

\jour Proc. Steklov Inst. Math.

\yr 2003

\vol 242

\pages 136--164

Образцы ссылок на эту страницу:

https://www.mathnet.ru/rus/tm413

https://www.mathnet.ru/rus/tm/v242/p147

Эта публикация цитируется в следующих 39 статьяx:

Powell T., Wiesnet F., “Rates of Convergence For Asymptotically Weakly Contractive Mappings in Normed Spaces”, Numer. Funct. Anal. Optim., 42:15 (2021), 1802–1838
Sipos A., “Revisiting Jointly Firmly Nonexpansive Families of Mappings”, Optimization, 2021
Dinis B., Pinto P., “Metastability of the Proximal Point Algorithm With Multi-Parameters”, Port Math., 77:3-4 (2020), 345–381
Miller D., “Mechanized Metatheory Revisited”, J. Autom. Reasoning, 63:3 (2019), 625–665
Rinaldi D., Schuster P., Wessel D., “Eliminating Disjunctions By Disjunction Elimination”, Indag. Math.-New Ser., 29:1, SI (2018), 226–259
Leustean L., Nicolae A., Sipos A., “An Abstract Proximal Point Algorithm”, J. Glob. Optim., 72:3 (2018), 553–577
Hadzihasanovic A., van den Berg B., “Nonstandard Functional Interpretations and Categorical Models”, Notre Dame J. Form. Log., 58:3 (2017), 343–380
Oliva P., “Hybrid Functional Interpretations of Linear and Intuitionistic Logic”, J. Logic Comput., 22:2, SI (2012), 305–328
Singh Sh.L., Mishra S.N., Pant R., “Fixed Points of Generalized Asymptotic Contractions”, Fixed Point Theory, 12:2 (2011), 475–484
Schuster P., “Problems, solutions, and completions”, J. Log. Algebr. Program., 79:1 (2010), 84–91
Avigad J., Towsner H., “Metastability in the Furstenberg-Zimmer tower”, Fund Math, 210:3 (2010), 243–268
Safarik P., Kohlenbach U., “On the computational content of the Bolzano-WeierstraB Principle”, MLQ Math Log Q, 56:5 (2010), 508–532
Briseid E.M., “Logical aspects of rates of convergence in metric spaces”, J. Symbolic Logic, 74:4 (2009), 1401–1428
Hernest M.-D., “Light monotone Dialectica methods for proof mining”, MLQ Math. Log. Q., 55:5 (2009), 551–561
Briseid E.M., “Fixed points of generalized contractive mappings”, J. Nonlinear Convex Anal., 9:2 (2008), 181–204
Seisenberger M., “Programs from proofs using classical dependent choice”, Ann. Pure Appl. Logic, 153:1-3 (2008), 97–110
Gerhardy Ph., Kohlenbach U., “General logical metatheorems for functional analysis”, Trans. Amer. Math. Soc., 360:5 (2008), 2615–2660
Cantini A., “On formal proofs”, Deduction, Computation, Experiment: Exploring the Effectiveness of Proof, 2008, 29–48
Ferreira F., “A most artistic package of a jumble of ideas (Kurt Gödel)”, Dialectica, 62:2 (2008), 205–222
Kohlenbach U., “Gödel's functional interpretation and its use in current mathematics (Reprinted from 'Horizons of Truth - Logics, Foundations of Mathematics, and the Quest for Understanding the Nature of Knowledge', 2008)”, Dialectica, 62:2 (2008), 223–267

Citing articles in Google Scholar: Russian citations, English citations
Related articles in Google Scholar: Russian articles, English articles

Труды Математического института имени В. А. Стеклова

Proceedings of the Steklov Institute of Mathematics

Статистика просмотров:
Страница аннотации:	950
PDF полного текста:	319
Список литературы:	93

Что такое QR-код?

Обратная связь:

Пользовательское соглашение

Регистрация посетителей портала

Логотипы