连接证明器

本项目旨在使用Rust重写leanCoP家族的几个自动化定理证明器，例如leanCoP和nanoCoP。

项目的目标是

• 性能：证明器应尽可能在每次时间内执行尽可能多的推理。
• 与原始证明器的兼容性：如果需要，证明器应能够重现原始证明器的相同步骤。这是为了帮助调试并保证正确性和完整性。

参考证明器meanCoP可以进行子句和非子句的证明搜索。它的子句证明搜索执行与leanCoP相同的证明步骤，而它的非子句证明搜索执行证明搜索与nanoCoP相似，但有一个技术可以在从子句连接到其副本时允许更小的扩展子句。

要运行证明器，需要安装最新的Rust工具链。这可以通过使用rustup方便地完成。

安装Rust后，您可以运行meanCoP，例如

cargo run --release problems/ijcar16ex.p

安装meanCoP

cargo install --path meancop

项目在eval目录中包含一个广泛的评估套件。