文件名称：qedeq:形式正确的数学知识
文件大小：41.44MB
文件格式：ZIP
更新时间：2024-05-28 16:07:51
Java
希尔伯特二世 概述 按照希尔伯特程序的传统，我们创建了一个形式正确的（可由证明验证者检查）但可读的（如普通的LaTeX教科书）数学知识库，该知识库可在Internet上免费访问。 逻辑和集合论开始了。 介绍 希尔伯特二世（ Hilbert II ）的目标是分散访问经过验证和可读的数学知识。 顾名思义，该项目是希尔伯特计划的传统。 希尔伯特二世（Hilbert II）希望成为一个免费的全球数学知识库，其中包含形式正确的数学定理和证明。 所有相关文档均根据GNU*文档许可发布。 我们旨在使普通的数学论证适应形式语法。 这意味着，每当在数学中经常使用某种论证时，我们都希望将其整合到希尔伯特二世的形式语言中。 这种正式语言称为QEDEQ格式。 希尔伯特二世（Hilbert II）提供了一个程序套件，使数学家能够将定理和证明放入该知识库中。 这些证明由证明检查器自动验证。 还可以集成“通用数学