Automath A Language for Mathematics
Automath A Language for Mathematics
复制标题
DOI：
10.1007/978-3-642-81955-1_11
复制
发表时间：
1973
期刊：
影响因子：
--
通讯作者：
中科院分区：
文献类型：
--
作者：
AUTOMATH是一种用于表达详细数学思想的语言。它不是一种编程语言，尽管它与现有的编程语言有一些共同的特性。它是由语法定义的，每一个根据它的规则写的文本都声称对应于正确的数学。它可以用来表达数学的很大一部分（见1.6），并承认许多奠定基础的方式。规则是这样的，计算机可以被指示检查用该语言编写的文本是否正确。这些教科书并不局限于单个定理的证明;它们可以包含整个数学理论，包括这些理论中使用的推理规则。
AUTOMATH is a language intended for expressing detailed mathematical thoughts. It isnota programming language, although it has several features in common with existing programming languages. It is defined by a grammar, and every text written according to its rules is claimed to correspond to correct mathematics. It can be used to express a large part (see 1.6) of mathematics, and admits many ways for laying the foundations. The rules are such that a computer can be instructed to check whether texts written in the language are correct. These texts are not restricted to proofs of single theorems; they can contain entire mathematical theories, including the rules of inference used in such theories.