Z3は再帰関数を含む数式の充足可能性をチェックできますか？

Question

私は再帰関数を含むa Z3 tutorialの例のいくつかを試しています。私は次の例を試しました。

1. Fibonacci（セクション8.3）
2. IsNat（セクション8.3）
3. Inductive（セクション10.5）

Z3タイムアウト上記実施例の全てに。しかし、このチュートリアルでは、Inductiveだけが終了していないことを暗示しているようです。

Z3は、再帰関数を含む数式の充足可能性をチェックできますか、帰納的な事実を処理できませんか？

Answer 1

Z3チュートリアルのこれらの例は、Z3の背後にある技術の限界を説明するものです。

1. Z3によって生成モデルは、各解釈機能シンボルの解釈を割り当てる：

   Z3は、2つの理由のために、これらの実施例に失敗します。モデルは、機能的なプログラムとして見ることができます。現在のバージョンは再帰的な定義を生成しません。最初の例は充足可能ですが、再帰的定義をサポートしていないため、Z3はfibの解釈を生成できません。 Z3をこの方向に拡張する予定です。

2. Z3は誘導によるプルーフをサポートしていません。実施例2および3は満足できるものではないが、誘発による証明を支持しないためZ3は失敗する。 基本的なサポートを追加する予定もあります。

これらの項目は私のTODOリストにありますが、今年は作業を開始しません。