theorem-proving相关内容

Z3-Python中的SAT查询变慢了：增量式SAT怎么办？

在Z3(Python)中，循环内的SAT查询速度变慢，我可以使用增量SAT来解决此问题吗？ 问题如下：我在循环中执行具体的SAT搜索。在每次迭代中，我都会得到一个模型(当然，我存储了该模型的否定，以便不会再次探索相同的模型)。此外，如果该模型满足某个属性，我还会添加它的子查询，并将其他限制添加到公式中。然后再次迭代，直到获得UNSAT(即不再有模型)。 我提供代码的定向快照： ..
发布时间：2022-08-22 00:00:00 其他开发

如何使Z3'；(Python)的SAT解算偏向某个标准，例如更倾向于有更多否定的文字

在Z3(Python)中，有没有办法将SAT搜索“偏向”“条件”？ 一个案例：我希望Z3获得一个模型，但不是任何模型：如果可能，请给我一个有大量否定文字的模型。 例如，如果我们必须搜索A or B，可能的模型是[A = True, B = True]，但我宁愿收到模型[A = True, B = False]或模型[A = False, B = True]，因为它们有更多的False分 ..
发布时间：2022-08-21 21:35:15 其他开发

使用 pytorch 验证卷积定理

基本上这个定理的公式如下: F(f*g) = F(f)xF(g) 我知道这个定理，但我只是无法使用 pytorch 重现结果. 以下是可重现的代码: 导入火炬导入 torch.nn.functional 作为 F# 计算 f*gf = 火炬.ones((1,1,5,5))g = torch.tensor(list(range(9))).view(1,1,3,3).float() ..
发布时间：2022-01-06 19:51:55 其他开发

Z3 Java API - 获得 unsat 核心

我想弄清楚如何使用 Z3 的 Java API 获取 unsat 核心.我们的场景如下(代码在下面，在rise4fun中有效): 我们以编程方式创建 SMT2 输入 输入包含函数定义、数据类型声明和断言 我们使用 parseSMTLIB2String API 解析它 我们确保上下文和求解器具有 unsat_core -> true Z3 为提供的输入返回 UNSAT，这是正确的 不 ..
发布时间：2021-10-04 20:41:44 其他开发

QF_NRA 中是否包含除以零?

QF_NRA 中是否包含除以零? SMT-LIB 标准在这方面令人困惑.定义标准的论文根本没有讨论这一点，事实上 NRA和 QF_NRA 没有出现在该文档的任何地方.标准网站上提供了一些信息.实数定义为包括: - 形式为 (/m n) 或 (/(- m) n) 的所有术语，其中- m 是 0 以外的数字，- n 是 0 和 1 以外的数字，- 作为整数，m 和 n 除了 1 没有公因数. ..
发布时间：2021-10-04 20:40:27 其他开发

避免在 Z3 中使用量词

我正在试验 Z3，我结合了算术、量词和等式的理论.这似乎不是很有效，事实上，在可能的情况下，用所有实例化的地面实例替换量词似乎更有效.考虑以下示例，其中我对函数 f 的唯一名称公理进行了编码，该函数接受两个排序 Obj 参数并返回一个已解释的排序 S.这个公理指出 f 的每个唯一参数列表都返回一个唯一对象: (declare-datatypes () ((Obj o1 o2 o3 o4 o5 o ..
发布时间：2021-10-04 20:34:08 其他开发

有没有人试过用 Z3 本身证明 Z3?

有人试过用 Z3 本身证明 Z3 吗? 是否有可能使用 Z3 证明 Z3 是正确的? 更多的理论，是否有可能证明工具 X 是正确的，使用 X 本身? 解决方案 简短的回答是:“不，没有人试图使用 Z3 本身来证明 Z3":-) “我们证明程序 X 是正确的"这句话非常具有误导性.主要问题是:正确是什么意思.在 Z3 的情况下，可以说 Z3 是正确的，至少，对于不可满足的问 ..
发布时间：2021-10-04 20:33:37 其他开发

Z3:提取存在模型值

我正在使用 Z3 的 QBVF 求解器，想知道是否可以从存在性断言中提取值.也就是说，假设我有以下内容: (assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x)))) 这基本上是说有一个“最少"的 16 位无符号值.然后，我可以说: (check-sat)(获取模型) Z3-3.0 高兴地回应: ..
发布时间：2021-10-04 20:29:26 其他开发

Z3:找到所有满意的模型

我正在尝试使用 Z3(一种由 Microsoft Research 开发的 SMT 求解器)检索某些一阶理论的所有可能模型.这是一个最小的工作示例: (declare-const f Bool)(断言(或(= f真)(= f假))) 在这个命题情况下，有两个令人满意的赋值:f->true 和 f->false.由于 Z3(以及一般的 SMT 求解器)只会尝试找到一个令人满意的模型，因此无法直接 ..
发布时间：2021-10-04 20:28:18 其他开发

使用 prolog 显示布尔逻辑失败的原因

假设我有以下布尔逻辑: Z = (A or B) and (A or C) 是否可以使用 prolog(可能与某些库一起使用)来找出 Z 为假的原因并以以下格式返回答案: Z 是假的，因为 A 或 (b 和 c) 是假的 如果我替换一些已知值(或全部)，比如 (c = true)，它会说:Z 是假的，因为 A 是假的 它可以告诉我是哪个规则或规则的哪一部分导致了这个问题:Z 是错误的 ..
发布时间：2021-06-22 18:54:34 其他开发

证明定理时循环

在用Debruijn指数形式化Lambda演算并在Coq中进行替换之后，我试图证明以下定理. 定理atom_equality:forall e:expression，forall x:nat，(beta_reduction(Var x)e)->(e = Var x). 这些是表达和减少beta的定义 归纳表达式:类型:=|Var(n:nat)|抽象(e:表达式)|应用程序(e1:表达式)( ..
发布时间：2021-04-24 20:07:58 其他开发

有没有一种方法可以使用Djinn在Emacs中自动生成Haskell代码？

标题几乎说明了一切。我正在寻找这样的东西： f :: Int->布尔-> Int f = _body Djinn可以使用定理证明通过证明该函数生成代码 我想知道，是否有现有的方法可以从Emacs中获得此功能？因此，不是在代码中编写TemplateHaskell，而是在代码上运行命令，然后插入生成的代码？ 我已经安装了ghc-mod，但是我对此不太 ..
发布时间：2020-10-28 23:54:28 其他开发

Coq：承认断言

是否有一种方法可以接受Coq中的断言？ 假设我有一个这样的定理： 定理检验：forall mn：nat， m * n = n * m。 证明。 前奏n m。 断言（H1：m + m * n = m * S n）。 {承认。 } 中止。 上述断言似乎对我不起作用。 我收到的错误是： 错误：没有集中的证据（没有正在进行的证明编辑）。 ..
发布时间：2020-10-09 06:42:31 其他开发

如何阅读Coq对proj1_sig的定义？

在Coq中， sig 定义为 归纳信号（ A：Type）（P：A-> Prop）：Type：= $​​ b $ b存在：forall x：A，P x-> sig P. 我读为 “ A sig P是一种类型，其中P是一个接受A并返回Prop的函数。定义该类型，使得如果P x成立，则类型A的元素x就是sig P类型。” proj1_sig 定义为 ..
发布时间：2020-10-09 06:25:55 其他开发

程序定点的Coq简化

是否有针对 Program Fixpoint s的战术 simpl ？ 特别是，如何证明以下琐碎的陈述？ 程序定点bla（n：nat）{measure n}：= 将n与 匹配| 0 => 0 | S n’=> S（bla n’） 结尾。 引理显而易见：forall n，bla n = n。 归纳n。自反性。 （*我被困在这里。对于一个普通的固定点，例如，我可以使用 s ..
发布时间：2020-10-09 06:14:50 其他开发

Isabelle2016和Proof General

我一直在尝试学习使用Isabelle2016.虽然原则上我喜欢异步证明检查的想法，但出于多种原因，我不喜欢Isabelle/jEdit，其中最严重的是它使用了(对我来说)太多的内存. 如果我可以在Isabelle 2016中使用良好的老式Proof General，那就太好了.我将变量isa-isabelle-command设置为指向文件Isabelle分发目录下的文件bin/isabell ..
发布时间：2020-07-31 04:20:24 其他开发