raa_tt - 命题演算句子证明器

此 crate 提供了一种算法，用于判断命题公式是否是重言式、矛盾式或偶然式，即其真值取决于其变量的真值。

这里使用的算法是 归谬法 的一种形式，即 真值树 方法，它是命题逻辑句子的决策过程。特别是对于更多逻辑变量的情况，这种方法比其他方法（例如 真值表）更有效。

为了便于使用，公式可以以文本形式提供，并由 raa_tt 二进制工具解析。命题使用的语法可以在此处检查：此处。

有关最新更改，请参阅 CHANGELOG

如何使用它？

克隆此仓库并切换到仓库文件夹。

然后运行，例如

cargo run -- -f ./test.txt
cargo run --release -- -s "((p -> q) & (r -> s) & (p | r)) -> q | s"

或者您可以通过以下方式安装 raa_tt

cargo install raa_tt

然后您可以直接从命令行调用它，例如

raa_tt -s "(a & a -> b) -> b" -q

您可以使用命令行参数 -h 获取帮助。

您能否将其嵌入到自己的应用程序中？

是的！raa_tt 也是一个库。您可以在自己的 crate 中引用它。

您想探索算法吗？

为了支持这一点，您可以使用日志功能。

基本上，设置环境变量 RUST_LOG，如下例中所示，这些示例使用 powershell

$env:RUST_LOG="raa_tt=trace,raa_tt::raa_tt_grammar_trait=error"

或者

$env:RUST_LOG="raa_tt=debug,raa_tt::raa_tt_grammar_trait=error"

您发现了 bug 吗？

请，提交问题。