z3 - Z3是否支持克雷格插值

Question

Z3 可以生成 Craig 插值（至少对于命题逻辑？）。我在 Z3 的文档中没有找到它。

Answer 1

不，Z3 不支持 Craig 插值，但它会生成证明。可以从证明中提取插值。Ken Mcmillan 正在使用这种方法在 Z3 之上开发一个插值生成器。