theorem-proving

theorem-proving

文章 0 浏览 3

Z3:提取存在模型值

我正在使用 Z3 的 QBVF 求解器,想知道是否可以从存在断言中提取值。也就是说,假设我有以下内容: (assert (exists ((x (_ BitVec 16))) (forall ((y…

你与清晨阳光 2024-12-01 08:55:11 1 0

GNU Prolog 的同义反复检查器

Closed. This question is seeking recommendations for software libraries, tutorials, tools, books, or other off-site resources. It does not …

牵你手 2024-11-29 16:11:40 2 0

有人尝试过用Z3本身来证明Z3吗?

有没有人尝试用 Z3 本身证明 Z3 ? 是否有可能使用 Z3 来证明 Z3 是正确的? 更理论化的是,是否有可能使用 X 本身来证明工具 X 是正确的?…

日暮斜阳 2024-11-27 10:22:27 1 0

如何进行 Coq 证明?

我的 Coq 证明有问题,希望得到一些帮助和指导。我的部分定义如下: Inductive Architecture : Set := | Create_Architecture (Arch_Name: string)(My…

放低过去 2024-11-27 06:42:36 2 0

用于位向量算术的 SMT 求解器

我正在计划使用现成的 SMT 求解器对 C 代码的符号执行进行一些实验,并想知道使用哪个求解器;例如,查看 SMT 竞赛参赛者,并仅采用开源系统,将范围…

撩心不撩汉 2024-11-14 06:21:10 3 0

模式匹配不专门化类型

我正在 Coq 中玩耍,尝试创建一个排序列表。 我只是想要一个接受列表 [1,2,3,2,4] 并返回类似 Sorted [1,2,3,4] 的函数 -即去掉坏的部分,但实际上并…

醉梦枕江山 2024-11-09 08:14:22 5 0

使用定理证明者寻找攻击

我听说过一些关于使用自动定理证明器来尝试证明软件系统中不存在安全漏洞的消息。一般来说,这是极其困难的。 我的问题是,是否有人使用类似的工具来…

迟到的我 2024-09-18 14:59:35 11 0

显示 (head . init ) = Agda 中的 head

我试图证明 Agda 中的一个简单引理,我认为这是正确的。 如果向量具有两个以上元素,则在获取 init 后获取其 head 与立即获取其 head 相同。 我将其表…

冷︶言冷语的世界 2024-09-13 08:28:17 6 0

希尔伯特系统 - 自动证明

我试图证明以下陈述 ~(a->~b) => a 希尔伯特风格系统。不幸的是,似乎不可能提出一个通用算法来找到证明,但我正在寻找一种强力类型的策略。欢迎任何…

一袭水袖舞倾城 2024-08-07 20:32:52 13 0

交互式数学证明系统

我正在寻找一种工具(首选 GUI,但 CLI 也可以),它允许我输入数学表达式,然后对其进行操作,但限制我只能进行数学上有效的运算。 此外,该工具必须…

三寸金莲 2024-07-16 12:25:33 12 0

成对优先队列

我有一组 A 和一组 B,每个都有一个关联的数字优先级,其中每个 A 可能匹配一些或所有 B,反之亦然,我的主循环基本上包括: 按优先级顺序选取最好的 …

潦草背影 2024-07-13 21:47:01 10 0

Kowalski 图定理证明

我正在尝试使用 Kowalski 图算法来求解定理 证明。 算法的描述位于 http://www.doc.ic.ac.uk/~rak/ 对于如何处理大事件保持沉默 它生成的重复子句的数…

对岸观火 2024-07-10 10:23:08 7 0
更多

推荐作者

胡图图

文章 0 评论 0

zt006

文章 0 评论 0

z祗昰~

文章 0 评论 0

冰葑

文章 0 评论 0

野の

文章 0 评论 0

天空

文章 0 评论 0

    我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
    原文