连接证明器

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

项目目标：

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

参考证明器 meanCoP 可以执行子句和非子句证明搜索。它的子句证明搜索执行与 leanCoP 相同的证明步骤，而它的非子句证明搜索则类似于 nanoCoP，除了有一种技术可以在从子句连接到其自身的副本时生成更小的扩展子句。

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

一旦安装了 Rust，您就可以运行 meanCoP，例如：

cargo run --release problems/ijcar16ex.p

安装 meanCoP

cargo install --path meancop

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