کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4673071 | 1346607 | 2013 | 16 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
N.G. de Bruijn's contribution to the formalization of mathematics
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
ریاضیات (عمومی)
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: N.G. de Bruijn's contribution to the formalization of mathematics N.G. de Bruijn's contribution to the formalization of mathematics](/preview/png/4673071.png)
چکیده انگلیسی
N.G. (Dick) de Bruijn was the first to develop a formal language suitable for the complete expression of a mathematical subject matter. His formalization does not only regard the usual mathematical expressions, but also all sorts of meta-notions such as definitions, substitutions, theorems and even complete proofs. He envisaged (and demonstrated) that a full formalization enables one to check proofs automatically by means of a computer program. He started developing his ideas about a suitable formal language for mathematics in the end of the 1960s, when computers were still in their infancy. De Bruijn was ahead of his time and much of his work only became known to a wider audience much later. In the present paper we highlight de Bruijn's contributions to the formalization of mathematics, directed towards verification by a computer, by placing these in their time and by relating them to parallel and later developments. We aim to explain some of the more technical aspects of de Bruijn's work to a wider audience of interested mathematicians and computer scientists.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Indagationes Mathematicae - Volume 24, Issue 4, 15 November 2013, Pages 1034-1049
Journal: Indagationes Mathematicae - Volume 24, Issue 4, 15 November 2013, Pages 1034-1049
نویسندگان
Herman Geuvers, Rob Nederpelt,