证明p或q仅当q或p在精益中

文章/答案/技术大牛

发布

1回答

lean

我试着做精益文档中的一章，但我很难理解所有的术语，因为我几乎不知道如何写校样。我想了解更多，但需要一些帮助。我一直在尝试和错误地尝试解决这个例子：不知道从哪里开始。有没有我在解释中遗漏的答案？

浏览 22提问于2020-05-13得票数 0

回答已采纳

1回答

如何证明精益中的分布性(命题有效性属性6)？

functional-programming、theorem-proving、lean

在经历了大多数练习，并在精益手册第3章末尾的精益中解决/证明了前五个命题有效性/性质之后，我仍然无法理解以下含义(证明性质6所需的含义之一)： theorem Distr_or_L (p q r :, sorry end 我面临的困难主要是因为当p不是真的时

浏览 13提问于2020-01-16得票数 1

回答已采纳

2回答

Lean 4‘未知标识符证明’

proof、theorem-proving、lean

我在使用精益4时遇到了一个问题。当我尝试运行这个片段时，我会得到以下错误：这意味着精</e

浏览 6提问于2021-09-14得票数 1

回答已采纳

1回答

结合精益中的两个简单假设

lean

我试着用精益来构造这个证据：这感觉就像一个简单的矛盾证明：假设P→Q.因为P，Q。Q与Q矛盾。到目前为止，我在精益课程中取得的成绩如下： exam

浏览 5提问于2022-08-23得票数 1

回答已采纳

1回答

p<q或p>=q的Coq证明

coq

我试图证明下面这个微不足道的引理： Lemma lt_or_ge: forall a b : nat,Proof.b) = false) -> (a >= b) 但似乎在Coq库中找不到它。感谢您的帮助，谢谢。

浏览 31提问于2020-02-01得票数 1

回答已采纳

1回答

如何证明或伪造“`forall (P，q:支柱)，(P -> Q) -> (Q -> P) -> P=q.”？

equality、coq、proof、dependent-type、curry-howard

我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，coq使得证明1=2 ->假是不可能的。但是，如果是这样的话，为什么还要消除证据的内容呢？没有

浏览 0提问于2014-10-26得票数 8

回答已采纳

1回答

例子：(p∨q)∧(p∨r)→p∨(q∧r)

lean

定理证明在精益说明如下：由于这涉及到iff，让我们先演示一个方向，从左到右： (assume h : p ∨ (q</e

浏览 11提问于2019-10-16得票数 1

回答已采纳

1回答

将nat的证明转换为非负整型的证明

lean

我证明了一些相当微不足道的引理显然，这同样适用于非负整数、有理数、实数等：一般来说，如果我们有一些精益的p n，我们应该能够得出0 ≤ z → p' z，其中p‘与p“相同”。然而，我甚至不知道如何在精益

浏览 4提问于2020-12-14得票数 3

1回答

TPIL 3.6:示例：(p→q)→p∧

lean

定理证明在精益说明如下：让我们用¬来重写→表达式example : ((p → q)

浏览 2提问于2019-10-27得票数 1

1回答

如何使用LEAN证明命题逻辑中的两个陈述？

theorem-proving、lean

在精益教程的第三章末尾，我仍然在努力(因此阻止我进一步阅读手册)的两个校对如下： theorem T11 : ¬(p ↔ ¬p) := sorry 为此，我试图证明正确的含义在这一点上停止了： theorem另一个是： theorem T2R : ((p ∨ q) → r) → (p → r) ∧ (q → r) := intros porqr, sorry end 我假设使用

浏览 16提问于2020-01-18得票数 0

回答已采纳

1回答

经典公理暗示每一个命题都是可判定的？

coq

在精益手册“精益证明定理”中，我读到：“用经典公理，我们可以证明每一个命题都是可判定的”。我想要求澄清这一声明，我在问一个Coq论坛，因为这个问题同样适用于Coq，也适用于精益(但我觉得我更有可能在这里得到答案)。在阅读“用经典公理”时，我知道我们有一些等价于排除中间定律的东西： Axiom LEM : forall (p:Prop), p \&

浏览 0提问于2020-04-20得票数 3

回答已采纳

1回答

如何从精益中的基本原理证明(∀x，p x)→(∃x，p x？

theorem-proving、lean

在“精益中的定理证明”4.4中，从第一原则证明这个基本含义的证明击败了我到目前为止的所有尝试： open classicaltheorem T08R : (¬ ∀ x, p x) → (∃x

浏览 21提问于2020-02-02得票数 2

回答已采纳

1回答

为什么倾斜的“赞成”得到特殊待遇？

types、theorem-proving、curry-howard、lean

自从我开始阅读交互式精益教程以来，有一个问题一直困扰着我：Type中独立的Type层次结构的目的是什么？| \ | | | | 这些边缘实际上是用?为什么精益能区分他们？Prop让人感到奇怪的是，它一方面是一种归纳类型(例如，它是封闭的，意味着p ∧ nat没有任何意义)，另一方面，它被用作一种类型(例如，通过为p构造一个<e

浏览 2提问于2017-04-18得票数 3

回答已采纳

2回答

精益中的几个基本命题逻辑证明

logic、proof、lean

我刚看了一下精益的文档，试着做，-∧和∨的交换性例:p∨q↔q∨p p对不起例：(p∨<em

浏览 3提问于2019-12-24得票数 1

回答已采纳

3回答

GNU Prolog的同义检验器

open-source、prolog、gnu-prolog、theorem-proving

或 3^2 * (X + 2) == (9 * X) + 18.作为结果，我期望的是布尔答案，如“是/否”、“等于/不同”、“证明已找到/未能找到证明”或类似的。P.P.S .如@larsman所指出，根据的说法，没有办法证明“所有”公式。这就是为什么我在寻找一些可以从给定的公理和规则中得到证明的东西，就像我在寻找Gnu Prolog程序一样，我正在寻找这样一组公理和规

浏览 8提问于2011-08-14得票数 2

回答已采纳

1回答

如何执行多个存在消除，所有这些都共享一个单一的多变量通用量化假设？

theorem-proving、lean

精益文档显示了以下两个仅包含单个变量的示例：variables (α : Type) (p q : α → Prop)exists.elim h assume hw : p w ∧ q w, -- this is ∀ w, p w ∧ <em

浏览 11提问于2020-02-29得票数 1

回答已采纳

1回答

例子：((p∨q)→r)→(p→r)∧(q→r)

lean

定理证明在精益说明如下：让我们关注左右方向： (assume hpq : p ∨ q,

浏览 3提问于2019-10-19得票数 0

回答已采纳

1回答

在z3中使用公理进行演绎

c#、z3

我是Z3的新用户，我希望它使用一些公理，并且只有这些公理才能将一个公式简化为一阶逻辑中的另一个等价公式。示例:仅使用2.not(p或q) <=> not(p) <=> not(q) 3.p和p <=

浏览 0提问于2012-05-17得票数 1

回答已采纳

2回答

初学者，不能进口精益。

theorem-proving、lean

我不能用精益进口任何东西。/tmp/lean-3.4.1-linux/bin/./lean /tmp/test.leanopen classical没有错误。

浏览 0提问于2018-06-11得票数 3

回答已采纳

2回答

在Coq中，是否有一种方法可以方便地证明假设的前提？

coq

我在我的证明上下文中有H : P -> Q，我需要Q来完成我的证明，但是我没有任何P的证据：在证明了目标P后，是否有一种策略或其他任何方法可以使前提P -> Q成为一个新的目标，然后用Q代替P。然后，我可以直接使用Q来证明最初的目标。然而，我也可以使用assert (HP : <

浏览 16提问于2022-04-26得票数 0

点击加载更多