3

スコーレム化を使用して、私の理論で存在記号を削除しようとしています。これは、存在記号を、存在記号のスコープ内の全称記号変数によってパラメーター化された関数に置き換えることを意味します。

ここで、Z3でこれを行う方法の説明を見つけましたが、まだ問題があります。次の2つの関数を想定します。

(define-fun f1 ((t Int)) Bool (= t 3))
(define-fun f2 () Bool (exists ((t Int)) (f1 t)))

真であるような整数、すなわち。f2が存在するので、それは真であるはずだと私は信じています。存在記号の式に定数を導入することにより、スコーレム化を適用します。t(f1 t)t=3

(define-const c Int)

次に、存在記号を含む式は次のように書き直されます。

(define-fun f2 () Bool (f1 c))

これは機能しません。つまり、定数cの値は3ではありません。定数に解釈を与えていないためだと思います。これcを追加すると正常に機能するためです(assert (= c 3))が、これにより存在記号の概念全体が失われます。数量詞。これが機能するように、あまり明確に解釈しない方法はありcますか？

4

1 に答える 1

7

ですから、実際にはほぼ正しいと思います。これが、自動（Z3のSNF戦術による）および手動（定数cの追加による）スコーレム化で使用したスクリプトです。これにより、スコーレム定数のモデルに値3が期待どおりに与えられました（ smt-libスクリプト： http： //rise4fun.com/Z3/YJy2）：

(define-fun f1 ((t Int)) Bool (= t 3))
(define-fun f2 () Bool (exists ((t Int)) (f1 t)))
(declare-const c Int)
(define-fun f2a () Bool (f1 c))

(push)
(assert f2)
(check-sat) ; sat
(get-model) ; model gives t!0 = 3 (automatic skolemization in Z3)
(pop)

(push)
(assert f2a)
(check-sat) ; sat
(get-model) ; model gives c = 3 after manual skolemization
(pop)

また、Z3にはスコーレム標準形（SNF）変換戦術が組み込まれていることに注意してください。これは、z3pyの例です（スクリプトへのリンク：http：//rise4fun.com/Z3Py/ZY2D ）。

s = Solver()

f1 = Function('f1', IntSort(), BoolSort())
t = Int('t')
f2 = Exists(t, f1(t))
f1p = ForAll(t, f1(t) == (t == 3)) # expanded define-fun macro (define-fun f1 ((t Int)) Bool (= t 3))

s.add(f1p)
s.add(f2)

print f1p
print f2

print s.check()
print s.model() # model has skolem constant = 3

g = Goal()
g.add(f1p)
g.add(f2)
t = Tactic('snf') # use tactic to convert to SNF
res = t(g)
print res.as_expr()
s = Solver()
s.add( res.as_expr() )
print s.check()
print s.model() # model has skolem constant = 3
于 2012-11-26T21:34:18.877 に答える