Z3はCraig補間をサポートします

Question

Z3はCraig補間を生成できますか（少なくとも命題論理の場合は？）。 私はZ3のドキュメントでそれを見つけられませんでした。

Answer 1

いいえ、Z3はCraig補間をサポートしていませんが、校正を生成します。補間は、プルーフから抽出することができる。 Ken Mcmillanは、このアプローチを使用してZ3の上に補間ジェネレータを開発しています。