Z3中的Skolemization

Question

我试图用Skolemization去除我的理论中的存在量词.这意味着我用存在量词范围内的通用量化变量参数化的函数替换存在量词.

在这里我找到了如何在Z3中做到这一点的解释,但我仍然遇到麻烦.假设有以下两个函数:

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

我认为f2应该是真的,因为存在一个t这样的整数(f1 t),即t=3.我通过引入存在量化公式的常数来应用Skolemization:

(define-const c Int)

然后将具有存在量词的公式重写为:

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

这不起作用,也就是说,常量c没有值3.我怀疑这是因为我们没有对常量给出解释c,因为如果我们添加(assert (= c 3))它就可以正常工作,但这会夺走存在的整个想法量词.有没有一种方法我可以给出一个不那么明确的解释,c以便这样做？

Answer 1

所以,我认为你实际上是正确的,这里是我使用自动(通过Z3的SNF战术)和手动(通过添加常数c)skolemization的脚本,它在模型中为skolem提供了值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内置了Skolem普通形式(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