如何通过Z3或SMT-Lib添加新逻辑？

Question

我有一个理论部分，我在其中描述新的逻辑，我想实现它。但我不想从头开始做所有事情。

我看到SMT-Lib / Z3有很大的潜力，那么如何使用这些工具实现我的逻辑呢？

在实现之后，我打算根据我的逻辑运行几个例子。

Answer 1

• 按排序的一阶逻辑对您的逻辑进行Axiomati化。
• 声明逻辑排序和符号，并以SMT-LIB格式添加公理。
• 使用这些命令作为示例的前导。

根据您的逻辑，您也可以尝试使用预定义的逻辑（如数组）来表达它们，而不是简单的一阶逻辑。