一般来说，一阶逻辑是Undecidable。但是，一阶逻辑的一些片段，如 Monadic 逻辑、BSR 片段、分离片段是可判定的。
存在解决 SAT/SMT 求解器的工具，如 Z3。是否有任何工具/语言可以检查 FOL 公式的可满足性？
问问题
111 次
1 回答
2
SMT 求解器，如 Z3，可以尝试检查 FOL 的可满足性（甚至是二阶逻辑！），尽管性能可能不是很好（取决于问题的外观）还有专门的 FOL 证明器（又名 TPTP 求解器），如 Vampire 、E、iProver 等。在此处查看更多信息：https ://en.wikipedia.org/wiki/Automated_theorem_proving
于 2019-12-05T11:10:30.217 回答