检验一阶逻辑可满足性的工具/语言？

Question

一般来说，一阶逻辑是不可判定的。然而，一阶逻辑的一些片段如一元逻辑、BSR片段、分离片段是可判定的.

有一些工具可以作为Z3来解决SAT/SMT问题。是否有检验FOL公式可满足性的工具/语言？

Answer 1

SMT解决程序，如Z3，可以尝试检查FOL的可满足性(甚至是二阶逻辑！)，尽管性能可能不是很好(取决于问题的外观)，也有专门的FOL验证程序(也称为TPTP解决程序)，比如吸血鬼、E、iProver等等。