我想用Z3来用泛量词证明公理中的定理，但Z3似乎不适合我的问题。它能够解决一些这样的问题，但似乎时不时会陷入困境如果不是Z3，我还可以寻找其他哪些工具
为了让你了解问题的类型，我想证明∀….Pₙ从公理/假设CCD_ 2。所有符号都是不可解释的，所有公式都只有通用量词。
我知道证据助理，但我需要一个完全自动的决定程序。虽然FOL是不可决定的，但我感兴趣的片段是否有可能有一个决定程序，无论是在其他工具中，还是在Z3中？
这类问题经常出现，唉，SMT求解器与量词重的问题不太匹配。最好的方法是指定模式(有关详细信息，请参阅基于电子匹配的量词实例化(。但它相当脆弱，绝对不是那么容易使用。
与你想要的相比，你最好的选择是使用校对助手；并希望他们的自动化策略(如Isabelle的大锤(可以在不需要太多用户干预的情况下进行证明。
当然，这是一般性的建议，但实际上对你的具体问题一无所知。如果你发布了它的一个具体实例，你可能会得到一个更好的答案，即是否有其他方法可以使用z3对它进行建模。
给定片段的当前公式，您仍然处于FOL的不可判定片段中。如果你可以限制你的P被允许谈论的内容，那么你可能会陷入一个可判定的片段中(例如，单子的、保护的、有效的命题的，有一些(。
除了SMT求解器和证明助手之外，还有一整类自动定理证明器对这类问题是完全的(即，如果有不一致的证明，他们最终会找到(，而SMT求解器不是。CASC是一个了解此类解决者的好地方，因为它是一个专注于此类问题的竞赛。吸血鬼是一个很好的例子(注意，我是吸血鬼的开发者(。