1

する

(=> (f g))

常に同じことを意味する

(or (not f) g))

?

私のモデルでは、2 つの式の動作が異なります。=>を使用するとUNSATが得られますが、他のバリアントを使用しても結果は得られません ( timeout )。演算子とその意味のリストがあれば満足です。SMTLIB 標準については知っていますが、ドキュメントでは演算子の意味について明示的に説明されていません。具体的には、' => ' は、三項式で使用される場合、' ite ' (if_then_else) 演算子のエイリアスとしても機能するようで、私はそれについてかなり混乱しています。

関連する場合は、 AUFLIAロジックを設定します。

最初に単純な「はい」または「いいえ」の答えを探しています。そして、SMT2 に関する適切なドキュメント (本かもしれません) が 2 番目です。

ダニエル・ジャクソンのマークスイープ・モデルから生成されたこのかなり大きなモデルを持っています。自分で見てみたい人のために、alloy4 用です。

4

1 に答える 1

2

あなたの表現は正しくない/不適切です。

=>確かに「含意」を意味します。つまり、(=> f g)と同等(or (not f) g)です。

疑わしい場合は、Z3 を使用して証明できます。以下のクエリはunsat次のとおりです。

(declare-const p Bool)
(declare-const q Bool)

(define-fun conjecture () Bool
    (= (=> p q) 
       (or (not p) q)))

(assert (not conjecture))
(check-sat)
于 2012-07-25T11:08:53.543 に答える