Metamath
Metamath是用來發展嚴格形式化數學定義及證明的一款語言[1],亦指用來驗證該語言的證明驗證器,以及存有邏輯、集合論、數論、群論、代數、數學分析、拓撲學、希爾伯特空間及量子邏輯[2]等領域中數萬條已證明定理且仍不斷在增加中的資料庫。
開發者 | Norman Megill |
---|---|
编程语言 | ANSI C |
操作系统 | Linux, Windows, Mac OS |
类型 | 電腦補助證明驗證 |
许可协议 | GNU通用公共授權條款 (資料庫使用創用CC) |
网站 | http://metamath.org |
參考資料
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.