1回答
我是Z3的新手，但有一些使用Prolog的经验。我已经设法解决了以下“难题”，即使用Prolog证明这个女孩是个巫师，但我不知道如何用Z3 (用C++或Python)实现它：https://www.netfunny.com/rhf/jokes/90q4
浏览 41提问于2020-07-04得票数 1
回答已采纳
0回答
我正在使用Z3定理证明器(使用Z3Py: Python中的Z3 )来创建QBF (量化布尔公式)。
有没有办法在Z3中直接将你的qbf公式转换成？
浏览 13提问于2017-11-27得票数 3
回答已采纳
1回答
我想知道是否有人能告诉我Z3和coq之间的区别？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略？或者可能coq中的证明搜索能力没有Z3那么强大？
浏览 1提问于2012-07-18得票数 44
回答已采纳
1回答
我试图用Z3定理求解器来解决SMT语法中的SAT问题，需要用CNF编写命题公式，并求出满意的值。我知道这些概念，但我不理解实现。你能给出用Z3定理证明器解决3-SAT问题的例子吗？谢谢
浏览 9提问于2021-12-05得票数 0
1回答
有没有一种方法可以使用Z3定理证明器从一组令人满意的任务中均匀抽样？如果没有，哪种系统最接近Z3具有此功能？
浏览 0提问于2012-10-05得票数 1
回答已采纳
1回答
定理证明工具z3花了很多时间来解决一个公式，我相信它应该能够很容易地处理。为了更好地理解这一点，并可能优化我对z3的输入，我想看看z3在求解过程中生成的内部约束。从命令行使用z3时，如何打印z3为其后端求解器生成的公式？
浏览 1提问于2012-10-28得票数 7
回答已采纳
1回答
我正在尝试让Z3验证一些在符号中使用迭代最大值的形式证明。例如，对于f a函数(↑i: 0≤i< N: f(I))指定当它应用于0到N之间的值时f的最高值。它可以很好地公理化为：如果p是i类型的谓词，有没有办法在Z3中定义这样的量词？它对我的证明的形成是非常方便的，所以我想让它尽可能地接近这个定义。
谢谢!
浏览 1提问于2012-07-06得票数 2
1回答
当Z3中的一个公式未满足并指定了(get-proof)时，会有一个输出，我找不到任何关于它是什么的信息。我在哪里可以找到关于这方面的任何文档？
在我看来很难读，有没有什么工具可以把这个作为输入呢？
浏览 5提问于2012-02-02得票数 6
回答已采纳
2回答
我需要证明地图数据结构的一些属性(如空、域、更新等)。Z3中是否支持地图？我最好的选择是我需要在Z3中添加一个新的理论，它假设对Z3的实现有很好的了解-这一假设在我的情况下是不成立的。
浏览 1提问于2018-09-13得票数 3
2回答
我想用Z3来用通用量词证明公理中的定理，但是Z3似乎不适合我的问题。它能够解决一些这样的问题，但它似乎不时地被卡住。如果不是Z3，我还能用什么工具呢？为了给您一个问题类型的概念，我想从公理/假设∀….Pₙ {∀….P₁, …, ∀….Pₘ}来证明{∀….P₁, …, ∀….Pₘ}。所有符号都没有解释，所有公式都只有通用量词。虽然FOL是不可判定的，但是对于我感兴趣的片段是否有可能有一个决策过程，或者是在其他工具中，或者甚至在
浏览 10提问于2022-01-27得票数 0
1回答
但Coq不是定理证明者，Coq是证明助手，这意味着用户需要在每一步中提供一些提示，Coq应该选择什么规则/策略。存在更多的ore - lest组合启发式策略，但Coq仍然不是证明者。我听说过在证明助手中使用机器学习或其他启发式方法来自动化证明过程的努力(它们被命名为*hammer?)，其中一些趋势发表在http://ai4reason.org/activities.html上。我的问题是- Co
浏览 21提问于2019-05-15得票数 3
回答已采纳
1回答
我正在尝试用z3做一件有点奇怪的事情。我正在尝试看看是否可以使用z3从交互式定理证明者那里获得类似"apply“的策略。我有一个类似于ForAll([x], Implies(a(x),b(x))的定理，以及一个在语法上等于b(x)的目标x，用于适当地选择x。有没有一种方法可以用z3得到适当的x？我不能只使用一个模型，因为c可能包含自由变量。我一直在尝试看看是否可以在Implies(ForA
浏览 11提问于2019-12-19得票数 0
我使用Z3定理证明器作为编译器的后端，以验证函数调用是否遵守它们的约定。然而，在解决看似简单的存在查询时，Z3似乎被卡住了。 (exists ((C Term))这是众所周知的缺陷还是Z3有没有
浏览 0提问于2019-09-15得票数 1
2回答
Z3或Z3Py中的假设
、、、
有没有一种方法可以在Z3 (我使用的是Z3Py库)中表达假设，这样引擎就不会检查它们的有效性，而是像定理证明一样将它们作为基本理论？用Z3Py编码，如下所示：assumption1 = ForAll(t，f1(t) = f2(t))。当前代码的问题是我的断言集非常大，并且我使用量词(我试图证明实时系统的可满足性)。如果
浏览 27提问于2016-03-23得票数 2
我最近开始使用Microsoft Z3进行定理证明，我想知道是否有一种方法可以将Z3实数转换为Z3浮点数，以便将它们传递给其他复杂函数。这就是我想做的， if x > 10: # This is where Z3 gives me an error as 'x' is a z3 object
浏览 6提问于2022-07-30得票数 0
回答已采纳
1回答
我有一份合金声明sig ATM {card : disj set Card}1- (declare-sort ATM) 8- (assert(forall ((atm ATM) (c Card)) (=> (card atm c)(= c(disjSetCard atm)))))问题是，在第
浏览 0提问于2015-07-04得票数 0
我试图理解如何定义断言，使其能够证明已经定义的函数的某些数学性质。正如在中所讨论的，SMT求解器并不适合于归纳，这通常需要证明一种数学性质。在我的例子中，我有一个标识函数 f(x) = x的递归函数定义(就像一个简单的例子)： (ite然而，我想知道如何在z3中证明一般的数学性质。我尝试使用所有量词来证明函数的对合，但是z3
浏览 2提问于2021-01-29得票数 0
回答已采纳
我们这里的问题是要证明使用带测试的Kleene代数。在b的值被p保持的情况下，我们有交换性条件bp = pb；并且两个程序之间的等价性被简化为方程在b的值不被p保留的情况下，我们有交换性条件pc = cp；并且两个程序之间的等价性被简化为方程
我正在尝试使用以下SMT-LIB代码来证明第一个等式(declare-fun sum (S S) S)(declar
浏览 4提问于2014-08-04得票数 3
2回答
我试图使用公理化命令在语法上实现LTL逻辑，目的是自动找到定理的证明(证明程序属性的动机)。我的问题是，是否存在一个命题，就像前面提到的那样，但它是为命题逻辑而做的，即只能访问MP和命题逻辑公理。编辑:我正在寻找一个希尔伯特风格的演绎证明器，而不是SAT，
浏览 2提问于2020-01-15得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
云直播
对象存储
腾讯会议活动推荐
腾讯云开发者
