Z3是否支持Craig插值

Question

Z3能否生成Craig插值(至少对于命题逻辑？).我没有在Z3的文档中找到它.

Answer 1

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