MIT教员制作vdash

Mgccl · 发表于 2008-10-1 11:15:18

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？欢迎注册

×

vdash是MIT的教员Cameron Freer制作的一个网站. 现在还没有启动. 主要意义就是创造一个一切基于形式化数学的wiki. 每一个定理都被一步一步的形式化证出来. 其中只有正确的语句才能够被发布. 这样网站的存在可以将所有的证明联系起来

可以看一下他在讲解这个事情的录像. http://www.youtube.com/watch?v=ZDI7L4Ya9Ms 虽然这样的事情不是首次,但是希望这个可以成功,因为上次失败的案例是在1995年(根本都没有开始

)的QED Project. 类似的最为相像的系统就是Mizar System. 可惜是给专业数学家搞得东西,大众很难搞... 不过最为知名的应该是Metamath Proof Explorer,但是只有几个人在搞创作,其他人不能帮忙. 我将我的能力做点事吧. 只有做大了才有用. 网站出来了慢慢往上添... 不过我在想..如果用的是wiki形式做...想要做成真正的证明数据库就不容易了.

无心人 · 发表于 2008-10-1 12:19:19

很好很强大呵呵做这个很困难

账号		自动登录	找回密码
密码			欢迎注册

[分享] MIT教员制作vdash

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。