SMM 3 - Metamath数据库处理器

是什么？

Metamath是一种用于表达形式化证明的语言，对底层逻辑的假设很少，足够简单以支持各种工具。参见 http://us.metamath.org/#faq。

构建

安装Rust (version 1.9.0或更高版本，然后检出此存储库并运行

cargo build --release

或者使用 cargo install

cargo install --git https://github.com/sorear/smetamath-rs
# $HOME/.cargo/bin/smetamath has been installed, use it as the binary in the following instructions

运行

# The largest known Metamath database, and best test case
git clone https://github.com/metamath/set.mm

# One-shot verification using 4 threads
target/release/smetamath --timing --jobs 4 --split --verify set.mm/set.mm

# Incremental verification
(while sleep 5; do echo; done) | target/release/smetamath --timing --jobs 4 --split --repeat --trace-recalc --verify set.mm/set.mm
# then make small changes to the beginning, end, or middle of the DB and observe how behavior changes

待办事项

• 对于增量验证器，我们可以进行更细粒度的依赖跟踪
• 目前还没有语法解析器或概要推理
• 可能需要研究一些证明模型的内容？