一般来说,一阶逻辑是Undecidable。但是,一阶逻辑的一些片段,如 Monadic 逻辑、BSR 片段、分离片段是可判定的。
存在解决 SAT/SMT 求解器的工具,如 Z3。是否有任何工具/语言可以检查 FOL 公式的可满足性?
一般来说,一阶逻辑是Undecidable。但是,一阶逻辑的一些片段,如 Monadic 逻辑、BSR 片段、分离片段是可判定的。
存在解决 SAT/SMT 求解器的工具,如 Z3。是否有任何工具/语言可以检查 FOL 公式的可满足性?
SMT 求解器,如 Z3,可以尝试检查 FOL 的可满足性(甚至是二阶逻辑!),尽管性能可能不是很好(取决于问题的外观)还有专门的 FOL 证明器(又名 TPTP 求解器),如 Vampire 、E、iProver 等。在此处查看更多信息:https ://en.wikipedia.org/wiki/Automated_theorem_proving