问题标签 [implication]

我无法证明这一点：

f(n) = O(g(n))暗示f(n)^k = O(g(n)^k)

where k is element of the natural, positiv numbers

我在网上找到了类似的例子。但我不确定为这个例子实施这些解决方案是否正确。

仅供参考，我使用的逻辑程序无法进行矛盾介绍。这一点很可能无关紧要，因为我非常怀疑我是否需要使用任何形式的矛盾来证明这一点。

在我尝试解决这个问题时，我开始假设 (p ⇒ q) ⇒ p)
这是正确的吗？

如果是这样，下一步是什么？如果解决方案看起来如此明显，请原谅我。

我正在尝试为 ((p ⇒ q) ⇒ p) ⇒ p 构建一个正式的证明。在惠誉。我知道这是真的，但我如何证明呢？

我只能使用 And Intro、And Elim、Or Inro、Or Elim、Neg Intro、Neg Elim、Impl Intro、Impl Elim、Biconditional Intro 和 Biconditional Elim。

我想知道是否有任何方法可以检查列是否有值，如果值为 XXXXX，则另一列必须在（A，B，C）列表中。就像是：

我是 prolog 的新手，我已经完成了一些编码，但是我有一个我无法处理的任务。您能否告诉我如何描述一个有效的谓词，它比较 arg1、arg2 和 arg3 并返回是它 arg1>arg2>arg3？提前谢谢了！

席蒙

我正在练习逻辑对等，但遇到了一个我很难回答的问题：

证明 (R or P -> R or Q) 等价于 (not R -> (P -> Q))。

我已经检查了这两种含义的真值表，但问题指出我应该使用等价定律来证明含义是等价的。

如果有人可以帮助我，我将不胜感激。

谢谢你。

正如我似乎再也找不到的另一个 StackOverflow 答案中所述，这种模式经常出现在实际的 Prolog 代码中：

许多人试图将其浓缩为

然而众所周知，箭头结构破坏了选择点并且不合逻辑。

在 Ulrich Neumerkel 和 Stefan Kral 的Indexing dif/2中，提出了一个单调且合乎逻辑的谓词if_/3，但是在论文中他们提到了另一个引起我注意的构造：*->.

该*->构造函数的功能与上面的未加糖保护子句示例完全相同，因此它似乎非常适合我的使用，因为我不想拥有所需的具体条件，if_/3而且我不太关心额外的选择点。如果我没记错的话（编辑：我是），它提供了与条件谓词相同的语义，if_/3但不需要将“具体化”添加到条件谓词中。

然而，在它的 SWI 文档中，它声称“这种结构很少使用”，这对我来说似乎很奇怪。在我看来，这比您尝试进行纯逻辑编程时要*->好得多。->是否有任何理由避免这种结构，或者是否有更好的替代整个保护条款/否定保护条款模式？

我试图证明->Coq 命题的传递性：

我想破坏所有的命题，简单地用自反性处理所有 8 种可能性。显然事情没那么简单。这是我尝试过的：

这就是我得到的：

其次是这个错误：

非常感谢任何帮助，谢谢！

尝试在 Python + Gurobi 中实现指标约束，其中指标（LHS）是二元决策变量的总和。

嗨，我想在 Python + Gurobi 中实现以下功能：

我想以某种方式具有以下含义：

但是，这不起作用，因为指示符约束将指示符变量声明为二进制类型。有解决方法吗？稍后我必须使用 U_d 变量来定义析取约束。

先感谢您！

我看到 Isabelle/HOL 中的许多定理更喜欢元级含义：

代替

对象逻辑层，即高阶逻辑蕴涵。

Isabelle wiki说，粗略地说，应该使用元级别的含义将规则陈述中的假设与结论分开。

除此之外，关于对象和元级别含义的使用我应该知道什么？我看到后者主要被使用。我应该在什么时候使用 HOL 蕴涵？