Etableau
Etableau是基于Eprover的一阶逻辑的一阶定理证明器，将其用作库。 Etableau以一种新颖的方式将叠加演算与子句式演算相结合，使用该演算来生成引理和新的假设，这些假设和新假设可用于在某些情况下查找矛盾。
这意味着可以使用Eprover的饱和度来关闭难以使用子句形演算关闭的画面分支。 饱和过程得益于画面分支上存在的额外假设。 似乎饱和过程通常会很快找到或根本找不到证明，因此通过使用不同的假设进行许多简短的证明搜索，就有可能找到原本可能不是的证明。
Etableau的许可和安装方式与Eprover相同。
要安装Etableau，请克隆此存储库，执行以下命令，或按照Eprover的说明进行操作。
./configure
make rebuild
可执行文件“ eprover”在PROVER目录中生成。 要检查它是否有效，请尝试运行./epr
评论0