数学知识管理：理论、应用和发展

理论计算机科学电子笔记93（2004）1-4www.elsevier.com/locate/entcs前言数学知识管理研讨会2003数学是最古老和最迷人的科学之一。计算机科学是一门非常年轻的科学。然而，计算机已经改变了我们交换和开发信息的方式，并为其他领域带来了新的发展计算机技术在医学、地理学、化学、生物学等方面的巨大影响无论怎样估计都不为对于数学，我们已经看到许多复杂的计算机系统（如计算机代数，定理证明器等）。帮助检查、验证、存储或计算数学。然而，我们正处于一个富有成效的和非常需要的研究调查数学知识管理（MKM）的开始有多少次，有一个理论这一点已经被发现了。作者们有多少次通过证明成千上万的引理来达到最终结果，然后发现其中许多引理已经被证明，如果作者知道它们，他们将节省许多宝贵的时间。要解释这种情况，最好的办法莫过于引用哈兹温克尔的话：我们但数学知识管理不仅仅是节省宝贵的时间，找到已经存在的东西，并建立在他人的工作上。MKM将在改善数学的教学、演示和发展以及加强和提高数学在所有其他领域的应用这些，以及许多其他原因导致一些领先的团体在欧洲硬币MKM研究领域，然后由美国倡议在美国和加拿大。日本的研究人员也在这方面变得活跃起来，已经有令人印象深刻的迹象表明，MKM正在成为数学中最有用的领域之一，1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.01.0012前言/理论计算机科学电子笔记93（2004）1-4它的应用。MKM的进展将延续到各种数学应用中。MKM会议和研讨会也在欧洲和北美举行，取得了相当大的成功：• 第一届数学知识管理国际研讨会。RISC，A-4232 SchlossHagenberg，奥地利2001年9月24日至26日。http://www.risc.uni-linz.ac.at/institute/conferences/MKM2001/• 第二届数学知识管理国际研讨会。意大利贝尔蒂诺罗。2003年2月16日至18日。http://www.cs.unibo.it/MKM03/• 第三届数学知识管理国际研讨会即将召开波兰比亚沃维耶扎。2004年9月19日至21日。http://mizar.uwb.edu.pl/MKM2004/• 第一届北美数学知识管理研讨会加拿大安大略省汉密尔顿。2002年6月12日至13日。http://imps.mcmaster.ca/na-mkm-2002/• 第二届北美数学知识管理研讨会美国亚利桑那州凤凰城。2004年1月6日http://imps.mcmaster.ca/na-mkm-2004/欧洲联盟http://monet.nag.co.uk/mkm//index.html。这种支持为MKM网络开辟了新的层面，并允许开始新的倡议和合作MKM网络感谢这种支持。MKM网络的成员在上述MKM会议和讲习班以及其他相关会议上举行了会议此外，2003年11月25日至29日在爱丁堡的赫瑞瓦特大学为MKM网络组织了一次官方活动，以审查迄今为止取得的进展并讨论未来的方向。来自欧洲、美国和日本的活跃团体进行了会谈，越来越明显的是，这一迷人的领域正在快速发展，并在各个方面发挥着越来越重要的战略作用。数学、计算机及相关领域。有关此活动的详细信息，请参阅http://www.macs.hw.ac.uk/~fairouz/mkm-symposium03/本次活动的演讲包括五个主题演讲，十三个邀请会谈，以及一些接受的会谈。主题演讲的题目如下：• Henk Barendregt（Nijmegen，NL）：建议建立一个机器人参考的数学。前言/理论计算机科学电子笔记93（2004）1• N.G. de Bruijn（荷兰埃因霍温）：回忆Automath项目。• Bob Constable（康奈尔大学，美国）：迈向形式数学的全球数字。• James Davenport（英国巴斯）：计算数学。• Abel Hazewinkel（CWI，阿姆斯特丹，荷兰）：为什么数学知识，它可能是。受邀的演讲描述了MKM社区中一些领导小组的研究。在MKM网络中看到如此多的活跃团体令人印象深刻。时间不允许邀请这些活跃的团体中的每一个进行谈话。相反，所提出的邀请会谈（标题如下）给了令人兴奋的工作发生在MKM的宣传。还有更多的事情正在进行，MKM似乎是目前最迷人的研究领域以下是受邀演讲的标题• OMEGA：从证明计划到数学知识管理。• Mizar项目• 数学知识管理与定理。• 把数学放到语义网上。• 计算数学• ActiveMath：个性化，主动学习，OMDoc等。• OMDoc：数学知识的表示格式。• 平等的科学：关于Coq Li的一些统计考虑。• 数学教育的内容。• 数学公式识别。• FOC和外部世界。• 建立一个数学逻辑教学工具• Logosphere：一个形式证明内容+意义的数字图书馆。由于邀请的会谈描述的是已经进行了一段时间的工作，并在此基础上建立了许多新的工作，因此我们认为，我们还需要从描述新工作的提交文件清单中选择一些会谈。发出了征文通知。在不到一个月的时间里，收到了19份意见书，其中只有9份被选入本卷。挑选被接受论文的方案委员会由以下人员组成： 如下：4.《理论计算机科学电子笔记》前言93（2004）1-4• Andrea Litti（意大利博洛尼亚大学）• Olga Caprotti（奥地利Risc-Linz）• James Davenport（英国巴斯大学）• William Farmer（加拿大麦克马斯特大学）• Fairouz Kamareddine（主席）（英国赫瑞瓦特大学）• Manfred Kerber（英国伯明翰大学）• Michael Kohlhase（德国不来梅工业大学• Daniel Leivant（美国印第安纳大学）• Rob Nederpelt（荷兰埃因霍温科技大学）• Renaud Rioboo（法国巴黎第七大学）• Andrzej Trybulec（波兰比亚韦斯托克）• Freek Wiedijk（荷兰奈梅亨大学）这些讲座具有挑战性，并越来越多地说明了在数学的各个方面对数学知识管理的需求数学知识管理是一场新的革命，它将对我们学习、教学、发展、研究、存储和使用数学的方式产生深远的影响。这反过来又会影响到任何使用数学的FairouzKamareddineHeriot-Watt University苏格兰爱丁堡