theorem-proving 相关问题

定理证明，目前是自动推理中最发达的子领域，是计算机程序证明数学定理。

在Coq中，有没有使用Rabs，Rineq的策略？

我对Coq并不陌生，我的主要兴趣是使用它来进行简单的实际分析问题。对于第一个练习，我设法证明了x ^ 2 + 2x趋于0且x趋于0的证据。请参见代码...

coq theorem-proving coq-tactic real-number

回答 1 投票 0

R中的经验CDF与理论CDF

[我想使用R来检查“概率积分变换”定理。让我们假设X是λ= 5的指数随机变量。我想检查随机变量U = F_X = 1-exp（-5 * X） ...

r probability theorem-proving cdf ecdf

回答 1 投票 0

不同的“排序”谓词在Dafny中应等效

根据SMT解算器的自动归纳，以下内容应在Dafny上起作用：幻影方法AdjacentImpliesTransitive（s：seq ）需要∀i•1≤i s [i-1]≤s [i]； ...

theorem-proving induction dafny

回答 1 投票 3

在Coq中将非A转换为A-> False

我想通过假设A并找到False来证明不是A。将目标不是A转换为A-> False的最短，最通用的方法是什么？我尝试了exfalso，但它并未在我的假设中添加A……

coq theorem-proving

回答 1 投票 1

测试Idris中的证据是否合理

我正在尝试编写一个测试代码来检查plusComm：（a：Nat） - >（b：Nat） - > a + b = b + a确实在自然数上证明了a + b = b + a，即代码不会伪造一个使用类型的孔，...

testing idris theorem-proving

回答 1 投票 1

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

假设我有以下布尔逻辑：Z =（A或B）和（A或C）是否可以使用prolog（可能与某些库一起）来找出为什么Z为假并返回答案...

prolog theorem-proving

回答 1 投票 2

伊莎贝尔：大锤发现了一个证据，但它失败了

我常常遇到大锤找到证据的问题，但是当我插入它时，它不会终止。我想大锤是伊莎贝尔最重要的部分之一，但后来它......

isabelle theorem-proving

回答 3 投票 6

在HOL中假设一个目标

我在HOL4中陈述了以下目标：set_goal（[``A：bool``，``B：bool``]，``B：bool``）;导致证明状态val it =证明经理状态：1证明。 1.不完整的目标堆：初始......

theorem-proving hol

回答 1 投票 1

如何使用精益法消除代数表达式中的括号

我试图用精益证明一个代数定理。我的代码是import algebra.group import algebra.ring open algebra variable {A：Type}变量[s：ring A]（a b c：A）包括s定理...

theorem-proving lean

回答 3 投票 1

我想用Prolog证明一些定理，然而，它总是返回“Out of global stack”

我正在做代数中证明群论的AI作业。该定理可表示如下：A1。 i（e，X）= X（同一性）A2。 i（X，e）= X（同一性）A3。一世（...

prolog swi-prolog theorem-proving

回答 1 投票 2

什么样的函数保留了闭包属性？

我试图证明以下引理：引理tranclp_fun_preserve：“（⋀xy。x≠y⟹fx≠fy）⟹（⋀xy。fx≠fy⟹x≠y）⟹（⋀xy.fx= fy ⟹x= y）⟹（λxy.P xy）⇧+⇧+（fx）（fy）⟹（...

isabelle theorem-proving

回答 1 投票 4

关于使用解决方案来查找某些条款的驳斥的问题

我正在做人工智能课程的作业，而我目前仍然坚持要求对某些条款进行驳斥的问题。我尝试了很多方法来找到关于那些的反驳......

artificial-intelligence theorem-proving

回答 1 投票 0

甚至从模板发生的Idris类型不匹配

测试一个“简单”的身份类型示例，mod等同，但是传递性证明不会进行类型检查，即使是从模板中也是如此。不仅仅是修复，我想知道为什么？这是最小的片段......

idris typechecking theorem-proving

回答 1 投票 1

为什么布尔逻辑语句需要采用联合范式（CNF）

我在处理布尔逻辑公式时看到的大多数事情首先将其转换为CNF或DNF格式。维基百科称它“在自动化定理证明中很有用”，但不多。想知道为什么......

boolean-logic theorem-proving sat conjunctive-normal-form

回答 1 投票 1

伊德里斯不会在指数法的证明中扩展`mult`

我正在尝试在Idris中写一个2 ^ n * 2 ^ m = 2 ^（n + m）的证明。现在我有这个：expLaw :(功率2 n）*（功率2 m）=功率2（n + m）expLaw {n = Z} {m} = plusZeroRightNeutral（功率2 m）expLaw {...

idris theorem-proving

回答 1 投票 1

证明Agda的爆炸原理

由于阿格达是直觉主义者，因此必须假定排除中间的法则。但据我所知，直觉主义逻辑接受ex falso quodlibet或爆炸原理（定理......

agda theorem-proving type-theory

回答 1 投票 1

在Isabelle中，尖括号和双星号是什么意思？

我试图理解一些Isabelle代码，并且有一些我不理解的语法。我没有在教程中看到它们，包括与Isabelle2017发行版捆绑的两个，“编程......

isabelle theorem-proving formal-verification isar

回答 1 投票 1

视觉上相同类型的“重写没有改变类型”错误

我写了一个简短的函数：swapMaybe：Monad m => Maybe（m a） - > m（也许是）swapMaybe Nothing = pure Nothing swapMaybe（Just x）= map Just x然后我试图证明它的一个属性：...

functor idris theorem-proving

回答 1 投票 0

以交互方式生成的证据：elab不起作用

我试图用交互式证明助手证明以下声明：total concatAssoc：（x：List a） - >（y：List a） - >（z：List a） - >（x ++ y）++ z = x ++（y ++ z）concatAssoc =？...

idris theorem-proving elaboration

回答 1 投票 2

theorem-proving 相关问题

最新问题