Titlebook: Mathematical Knowledge Management; Second International Andrea Asperti,Bruno Buchberger,James Harold Daven Conference proceedings 2003 Spri

只看該作者 · 發(fā)表于 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.

只看該作者 · 發(fā)表于 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.

只看該作者 · 發(fā)表于 2025-3-24 01:53:32

只看該作者 · 發(fā)表于 2025-3-24 04:45:54

只看該作者 · 發(fā)表于 2025-3-24 07:32:37

只看該作者 · 發(fā)表于 2025-3-24 13:48:40

只看該作者 · 發(fā)表于 2025-3-24 14:51:24

只看該作者 · 發(fā)表于 2025-3-24 22:10:45

只看該作者 · 發(fā)表于 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.

		自動登錄	找回密碼
密碼			To register

關(guān)于派博傳思			派博傳思旗下網(wǎng)站			友情鏈接
派博傳思介紹	公司地理位置	論文服務(wù)流程	影響因子官網(wǎng)	吾愛論文網(wǎng)	大講堂	北京大學(xué)	Oxford Uni.	Harvard Uni.
發(fā)展歷史沿革	期刊點評	投稿經(jīng)驗總結(jié)	SCIENCEGARD	IMPACTFACTOR	派博系數(shù)	清華大學(xué)	Yale Uni.	Stanford Uni.
\|Archiver\|手機版\|小黑屋\| 派博傳思國際 ( 京公網(wǎng)安備110108008328) GMT+8, 2025-10-16 01:22
Copyright © 2001-2015 派博傳思京公網(wǎng)安備110108008328 版權(quán)所有 All rights reserved