我正在尝试使用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这样才能奏效？
所以，我认为你实际上是正确的，这是我使用自动（通过 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