2

私はシンボリック変数のセットを持っています:

int a, b, c, d, e;

いくつかの公理によって制約される一連の未知の関数:

f1(a, b) = f2(c, b)
f1(d, e) = f1(e, d)
f3(b, c, e) = f1(b, e)
c = f1(a, b)
b = d

ここで関数f1、f2、f3は不明ですが、修正されています。したがって、それは の理論ではありませんuninterpreted functions。

次の主張の妥当性を証明したい:

c = f2(f1(a, b), b)
f3(d, f2(c, b), e) = f1(e, b)

上記の公理的等式に基づく置換を使用します。

関数の解釈を考え出すのではなく、提供された等式のみを使用して答えを結合しようとするような定理の理論はありますか?

もしそうなら、その理論の名前は何ですか? また、どの SMT ソルバーがそれをサポートしていますか?

線形算術のような他の理論と混合できますか?

4

1 に答える 1

3

公理を満たす関数が存在する場合、これは未解釈関数の理論に含まれるため、これはまだ解釈されていない関数です。同様に、そのような関数が存在しない場合、これは未解釈の関数では未飽和です。したがって、解釈されていない関数の問題が充足可能である場合にのみ、あなたが描写しているものは充足可能であり、したがって2つの理論は同型、つまり同じです。

特定の定理が公理に基づいて有効であることを証明しようとしている場合、sat の結果は無効なモデルに対応するため、ソルバーがどのように満足できる結果を表すかは重要ではありません。SMT ソルバーを使用して定理を証明するには、公理を主張し、定理の否定を主張してから、満足できない結果を探す必要があります。充足可能性と有効性との関係のより詳細な説明については、この質問を参照してください。

Z3 を使用して最初の定理を証明するには、SMT-LIB 2 で次のようにすれば十分です。

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(declare-fun f1 (Int Int) Int)
(declare-fun f2 (Int Int) Int)

(assert (= (f1 a b) (f2 c b)))
(assert (= c (f1 a b)))
(assert (not (= c (f2 (f1 a b) b))))

(check-sat)
于 2016-08-29T13:13:49.700 に答える