我正在尝试使用微软研究院开发的SMT求解器Z3检索所有可能的一阶理论模型.这是一个最小的工作示例:
(declare-const f Bool)
(assert (or (= f true) (= f false)))
在这个命题案例中,有两个令人满意的任务:f->true和f->false.因为Z3(以及一般的SMT求解器)只会尝试找到一个令人满意的模型,所以找不到所有解决方案是不可能的.在这里,我发现了一个有用的命令(next-sat),但似乎最新版本的Z3不再支持这一点.这对我来说有点不幸,总的来说我觉得这个命令非常有用.还有另一种方法吗？
假设我想对列表中的每个元素应用一个函数，然后将结果值放在另一个列表中，以便我可以立即使用它们。在 python 中，我会做这样的事情：
list = [1,2,3]
str = ', '.join(multiply(x, 2) for x in list)
在 Go 中，我做这样的事情：
list := []int{1,2,3}
list2 := []int
for _,x := range list {
list2 := append(list2, multiply(x, 2))
}
str := strings.Join(list2, ", ")
是否有可能以更短的方式做到这一点？
我正在试验Z3,在那里我结合了算术,量词和平等的理论.这似乎不是非常有效,事实上,在可能的情况下用所有实例化的地面实例替换量词似乎更有效.考虑下面的示例,其中我为一个函数编码了唯一名称公理,该函数f接受两个排序参数Obj并返回一个解释排序S.这个公理说明每个唯一的参数列表f返回一个唯一的对象:
(declare-datatypes () ((Obj o1 o2 o3 o4 o5 o6 o7 o8)))
(declare-sort S 0)
(declare-fun f (Obj Obj) S)
(assert (forall ((o11 Obj) (o12 Obj) (o21 Obj) (o22 Obj))
(=>
(not (and (= o11 o21) (= o12 o22)))
(not (= (f o11 o12) (f o21 o22))))))
虽然这是在逻辑中定义这样一个公理的标准方法,但是像这样实现它在计算上非常昂贵.它包含4个量化变量,每个变量可以有8个值.这意味着这导致了8^4 = 4096平等.需要Z3 0.69s和2016量词实例来证明这一点.当我编写一个生成此公式实例的简单脚本时:
(assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8)))
生成这些公理需要0.002s,而在Z3中需要0.01s(或更少).当我们增加域中的对象或函数的参数数量时,f这种差异会迅速增加,并且量化的情况很快变得不可行.
这让我想知道:当我们有一个有界域时,为什么我们首先在Z3中使用量词？我知道SMT使用启发式方法来寻找解决方案,但我感觉它仍然无法与一个简单的特定于域的地面实施竞争,后者将基础实例提供给SMT,这仅仅是SAT解决方案.我的直觉是否正确？
我正在尝试找到一种将以下一阶逻辑表达式放入Prolog中的方法：
(p(0) or p(1)) and not (p(0) and p(1))
这意味着它应该以以下方式响应查询：
?- p(0)
Yes.
?- p(1)
Yes.
?- p(0),p(1).
No.
我试图翻译逻辑表达式：
(p(0) or p(1)) and not (p(0) and p(1)) <=>
(not p(0) -> p(1)) and (p(0) -> not p(1)) <=>
p(0) <-> not p(1)
使用Clarks补全（表示每个定义理论都可以通过给出if-halves放入逻辑程序中），我可以获得：
p(0) :- not p(1).
不幸的是，这种结果理论仅是合理的（它不会得出虚假信息），而并不完整（例如：无法得出p（1））。这是克拉克斯定理的结果。
有人知道是否有更好的解决方案？谢谢！
我试图证明 Z3（Microsoft 的 SMT 求解器）中的一个归纳事实。我知道 Z3 通常不提供此功能，如Z3 指南（第 8 节：数据类型）中所述，但是当我们限制要证明事实的域时，这似乎是可能的。考虑以下示例：
(declare-fun p (Int) Bool)
(assert (p 0))
(assert (forall ((x Int))
(=>
(and (> x 0) (<= x 20))
(= (p (- x 1)) (p x) ))))
(assert (not (p 20)))
(check-sat)
求解器正确响应unsat，这意味着这(p 20)是有效的。问题是，当我们进一步放松这个约束时（我们20在前面的例子中用大于 20 的任何整数替换），求解器响应unknown。
我觉得这很奇怪，因为 Z3 解决原来的问题并没有花很长时间，但是当我们将上限增加 1 时，它突然变得不可能。我试图向量词添加一个模式，如下所示：
(declare-fun p (Int) Bool)
(assert (p 0))
(assert (forall ((x Int))
(! (=>
(and (> x 0) (<= x …我试图用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以便这样做？