theorem-proving 相关问题

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

Coq定理证明：Peano算术中的简单分数定律

我正在学习coq，并试图证明Peano算术中的相等性。我陷入了简单的分数定律。我们从小学知道（n + m）/ 2 = n / 2 + m / 2。在Peano算术中，此...

coq theorem-proving peano-numbers

回答 1 投票 0

如何有效简化具有上一个引理的coq目标？

为什么我的证明的最后一行没有丢下一个后继者，而不是增加一个。注意：我在课堂环境之外做这些练习，不要纵容人们用它来作弊，我只是...

coq theorem-proving coq-tactic

回答 1 投票 0

如何在Prover9中建模爱因斯坦的船只难题（一阶逻辑）

我需要在Prover9中模拟以下难题：港口有5艘船：希腊船六点出发，并携带咖啡。中间的船有一个黑色的烟囱。英国船...

theorem-proving first-order-logic zebra-puzzle

回答 2 投票 0

ATS证明：为什么需要大于或等于此静态？

我正在写a * 0 = 0的证明，但我偶然发现了一些奇怪之处。为什么第7行上的sif a> = 0需要是> =，并且当sif> 0时不编译？ prfn mul_ax0_0 {a：int}（）：...

if-statement theorem-proving ats

回答 1 投票 1

在Agda中，我如何证明在共性列表（也就是Stream）上的不合格之后的缺点是身份？

我正在通过https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html研究共形和共通图案。我以为我理解了本文的代码，所以我决定从事以下工作...

agda theorem-proving coinduction

回答 1 投票 2

您如何阅读coq量词`forall P：Set-> Prop`？

我是Coq的新手，正在这里查看Mike Nahas的教程：nahas_tutorial.v。具体来说，我在理解下面给出的语句时遇到了麻烦：定理forall_exists：（forall P：...

types coq proof theorem-proving

回答 1 投票 1

空集的这种形式化在Agda中正确吗？

我正在遵循Agda的Haskell逻辑，数学和编程之路。本书指出：空集是一个小关系，是阿格达中两个集A和B之间的最小关系：data∅...

logic agda theorem-proving set-theory

回答 1 投票 0

Idris：是否可以在相等性证明中引用抽象变量？

这个问题的最简单的例子（但不是我能展示的唯一例子）是：假设我得到了一个高阶函数f：（a-> b）-> c。我想证明f =（\ g => f（\ x => g x）...

idris theorem-proving

回答 1 投票 0

如何使用引用来指导Haskell中的类型检查器？

在以下程序中填充孔是否一定需要非建设性的手段？如果是，则x：〜：y是否可确定？更笼统地说，我该如何使用反驳来指导...

haskell types dependent-type theorem-proving

回答 1 投票 4

在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

theorem-proving 相关问题

最新问题