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

Question

我有一个理论部分，在那里我描述了新的逻辑，我想实现它。但我不想一切从头做起。

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

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

Answer 1

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

根据您的逻辑，您还可以尝试使用预定义逻辑来表达它们，例如数组，而不是普通的一阶逻辑。