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

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

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

2011-08-10 15:49:58

ご返信ありがとうございます。プロジェクトのステータスについて知っていますか？数日、数週間、数ヶ月で終了しますか？ –

ケンの補間決定手続きはすでに使用されています。彼は結局それをMSRのウェブサイトで利用できるようにする。今のところ、彼はそれを個別にリリースしています。手続きを取るために彼に連絡することができます。 –

答えて