问题标签 [theorem-proving]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
logic - 自动定理证明程序 - 从哪里开始?
我是一名二年级学生,我的离散数学 2 任务是制作一个自动定理证明器。我必须在 4 周内制作一个适用于命题逻辑的简单证明程序(假设证明始终存在)。到目前为止,我已经用谷歌搜索了,但那里的材料在 4 周内真的很难理解。谁能推荐我一些适合初学者的书籍/网站/开源代码或一些有用的提示?先感谢您。
logic - Z3 定理证明器:勾股定理(非线性算术)
因此?
我的问题发生的用例上下文
我定义了一个三角形的 3 个随机项。Microsoft Z3 应输出:
- 约束是否满足或是否有无效的输入值?
- 所有其他三角形项目的模型,其中所有变量都分配给具体值。
为了约束我需要assert
三角形等式的项目 - 我想从勾股定理((h_c² + p² = b²) ^ (h_c² + q² = a²)
)开始。
问题
我知道 Microsoft Z3 解决非线性算术问题的能力有限。但即使是一些手动计算器也能够解决这样一个非常简化的版本:
问题
- 如果给出两个值,有没有办法让 Microsoft Z3 解决勾股定理?
- 或者:是否有另一个定理证明器能够处理这些非线性算术的情况?
感谢您对此的帮助 - 如果有任何不清楚的地方,请发表评论。
theorem-proving - 在 Isabelle 中一起调用 Nitpick 和 Sledgehammer
当我在Isabelle中陈述引理时,我经常输入nitpick
,如果这没有给我一个反例。然后我键入sledgehammer
以尝试自动查找证明。
我想知道:是否可以调用Nitpick和Sledgehammer以便它们同时运行?既然Sledgehammer已经将我的引理发送给了一堆自动证明者,那么这些证明者中的一个难道不能成为像Nitpick这样的反例发现者吗?
math - Z3Py:从方程组生成抽象公式
我的例子:方程组
伪代码约束库 解决方案我想要的信息
在方程组中,我想获得以下知识:
我可以用来从给定值(在约束基础中)计算变量值(解决方案)的抽象公式。
(就像在高中,老师不仅想要看到结果,还想要这样一个转换的抽象公式。)
像...这样的公式我的问题
如何使用Z3Py从 Z3 约束方程系统中检索此信息?
谢谢。- 如果有任何不清楚的地方,请评论什么是错的。
logic - 使用 Coq 的案例证明
我有一个简单的定理,我想用案例证明来证明。下面给出一个例子。
我将如何解决这个问题。而且,我将如何使用相等的两个可能值(真或假)来定义证明?
任何帮助,将不胜感激。谢谢,
theorem-proving - 有限有界量词的消除规则
我有以下目标:
我想将此目标分解为六个子目标P 0
,P 1
,P 2
,P 3
和。这很容易做到。但是用于执行此操作的相关规则是什么?我问是因为我的实际目标看起来更像这样:P 4
P 5
apply auto
auto
并且apply auto
不会以同样的方式打破这个目标(它给了我
反而)。
z3 - Z3 不会对手工制作的数据类型进行大小写拆分
我已经定义了自己的布尔值,称为boolean
SMT2,以及boolean_and
它们的 AND 函数。我的猜想是 AND 是可交换的:
然而,z3 在一段时间后报告了这个问题的未知数,尽管我认为它应该能够对 skolemised 变量sk_x
和sk_y
.
奇怪的是,如果我删除我的布尔公理化并将其替换为
declare-datatypes
,z3 将报告unsat
:
我究竟做错了什么?如何使用我的公理化让 z3 进行案例拆分?
matrix - Z3:执行矩阵运算
我的情况
我正在做一个需要:
- 证明涉及矩阵运算的3D 矩阵变换公式的正确性
- 找到具有未知矩阵条目值的模型。
我的问题
- 使用矩阵运算来表达公式以便它们可以解决的最佳方法是
z3
什么?(Z3Py 的 Sudoku 示例中使用的方式不是很优雅,似乎不适合更复杂的矩阵运算。)
谢谢。- 如果有任何不清楚的地方,请留下问题评论。
coq - How do you make notations visible outside of a module signature in Coq?
I've defined a module signature in Coq that defines several notations. When I try to use these notations outside of the signature however, Coq fails. A simplified version of my code is given below. Any help would be appreciated.
c - 如何用coq证明ac程序的正确性
我想证明我的一些程序的正确性,但我不知道从哪里开始。假设我有以下程序,我该如何证明它的正确性或缺乏。我怎样才能从下面的源代码中将它们插入定理证明器。Coq 或 ACL2 或几乎任何东西。
下面的代码只计算它从标准输入中读取的字节数。它有 2 个版本,一个逐字节计数,另一个尽可能以无符号整数大小的块读取它们。我知道它既不便携也不漂亮,这只是一个可以让我入门的例子。在一些帮助下。
代码有效,我知道它是正确的,我知道如何为它编写单元测试,但我不知道如何证明它。