companion
发表于 2025-3-23 10:53:11
http://reply.papertrans.cn/63/6262/626190/626190_11.png
仔细检查
发表于 2025-3-23 16:25:13
MKM from Book to Computer: A Case Study, we describe the sorts of knowledge in one chapter (elementary transcendental functions) and the difficulties in making this sort of knowledge formal. This makes us ask questions about the nature of a Mathematical Knowledge Repository, and whether a database is enough, or whether more “intelligence” is required.
Ambiguous
发表于 2025-3-23 19:08:44
From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfallsems and make important design decisions. This paper is based on our experiences on the exportation to XML of the theories developed in Coq and NuPRL: we try to collect a set of (hopefully useful) suggestions to pave the way to other teams willing to attempt the same operation.
freight
发表于 2025-3-24 01:53:32
http://reply.papertrans.cn/63/6262/626190/626190_14.png
产生
发表于 2025-3-24 04:45:54
http://reply.papertrans.cn/63/6262/626190/626190_15.png
Cocker
发表于 2025-3-24 07:32:37
http://reply.papertrans.cn/63/6262/626190/626190_16.png
占线
发表于 2025-3-24 13:48:40
http://reply.papertrans.cn/63/6262/626190/626190_17.png
GRAZE
发表于 2025-3-24 14:51:24
http://reply.papertrans.cn/63/6262/626190/626190_18.png
空洞
发表于 2025-3-24 22:10:45
http://reply.papertrans.cn/63/6262/626190/626190_19.png
职业拳击手
发表于 2025-3-25 00:18:10
Comparing Mathematical ProversWe compare fifteen systems for the formalizations of mathematics with the computer. We present several tables that list various properties of these programs. The three main dimensions on which we compare these systems are: the size of their library, the strength of their logic and their level of automation.