【发布时间】：2019-03-12 20:34:01
【问题描述】：
我有一个理论部分，我描述了新的逻辑并且我想实现它。但我不想从头开始做所有事情。
我看到了 SMT-Lib/Z3 的巨大潜力，那么如何使用这些工具实现我的逻辑？
在实现之后，我打算根据我的逻辑运行几个示例。
【问题讨论】：
-
使用比 SMT-LIB 支持的更丰富的逻辑的证明/验证通常被编码到 SMT-LIB 中。例如，Viper (viper.ethz.ch) 将基于分离逻辑的证明编码到 SMT-LIB 中，这是一个非常复杂的过程。这启用了一个工具堆栈，其中甚至“更高”的工具使用更丰富的逻辑将证明编码到 Viper 中，并最终编码到 SMT-LIB 中，例如这里：描述link.springer.com/chapter/10.1007/978-3-319-89960-2_11。