标签: proof

在我的算法分析课程中，我从算法中导出了函数 f(n) = n^2 - n + 2。现在我需要证明或反驳f(n) \xe2\x88\x88 O(n)。显然不是，所以我几个小时以来一直试图反驳这一点，但不知道该怎么做。

为了反驳它，我需要证明否定：

\xe2\x88\x80M > 0, \xe2\x88\x80N > 0, \xe2\x88\x83n > N s.t. n^2 - n + 1 < M\xc2\xb7n\n

我尝试过前后工作，但似乎无济于事。我还试图证明，与我的判断相反， f(n) \xe2\x88\x88 O(n)：

\xe2\x88\x83M > 0, \xe2\x88\x83N > 0 s.t. \xe2\x88\x80n > N, n^2 - n + 1 \xe2\x89\xa5 M\xc2\xb7n\n

...没有成功。我到底做错了什么？

以下文本是算法书的摘录.

我们可以使用常用于链表的矩形框来绘制二叉树,但树通常被绘制为由线连接的圆,因为它们实际上是图形.我们在引用树时也没有显式地绘制NULL链接,因为每个具有N个节点的二叉树都需要N + 1个NULL链接.

我的问题是作者的意思是每个具有N个节点的二叉树都需要N + 1个空链接？作者如何使用N + 1号码？

有人可以告诉我解决以下问题的数学部分.

显示没有比较排序,其运行时间至少是n的一半是线性的!长度为n的输入.那么长度为n的输入的1/n的一小部分呢？分数(1 /(2)^ n)怎么样？

解:

如果排序在m个输入排列的线性时间内运行,那么由m个相应叶子和它们的祖先组成的决策树部分的高度h是线性的.使用与定理8.1的证明中相同的参数来表明m = n!/ 2,n!/ n或n!/ 2n是不可能的.我们有2 ^h≥m,这给我们h≥lgm.对于此处给出的所有可能的ms,lgm =Ω(n lg n),因此h =Ω(n lg n).特别是,

    lgn!/2= lg n! ? 1 ? n lg n ? n lg e ? 1
    lgn!/n= lg n! ? lg n ? n lg n ? n lg e ? lg n
    lgn!/2^n= lg n! ? n ? n lg n ? n lg e ? n

我试图证明Isabelle/HOL的交换性是一种自定义的add功能.我设法证明了相关性,但我坚持这个.

定义add:

fun add :: "nat ? nat ? nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"

相关性证明:

lemma add_Associative: "add(add k m) z = add k (add m z)"
apply(induction k)
apply(auto)
done

交换的证明:

theorem add_commutativity: "add k m = add m k"
apply(induction k)
apply(induction m)
apply(auto)

我有以下目标:

goal (3 subgoals):
1. add 0 0 = add 0 0
2. ?m. add 0 m = add …

我想在 Isabelle 中使用 nat 类型，但我想重载一些现有的定义，例如加法。我写了以下代码：

theory Prueba
imports Main HOL
begin

primrec suma::"nat ? nat ? nat" where
"suma 0 n = 0" |
"suma (Suc x) n = 0"
no_notation suma (infix "+" 65)

value "2 + (1 :: nat)"

我试图用一个总是输出 0 的新定义来重载加法。但是，当我评估2 + (1 :: nat)I get 时"Suc (Suc (Suc 0))" :: "nat"，这意味着 Isabelle 仍在使用来自 Nat 的加号定义。我怎样才能让它使用我对 + 的新定义？

谢谢

在命题和谓词演算中证明了数十个引理之后（有些比其他的更具挑战性，但通常仍然可以在intro-apply-destruct自动驾驶仪上证明），我从一开始就打了一个~forall，并立即被抓住了。显然，我对 Coq 的理解和知识缺乏。所以，我要求使用低级 Coq 技术来证明一般形式的语句

~forall A [B].., C -> D.  
exists A [B].., ~(C -> D).

换句话说，我希望有一个通用的 Coq 方法来设置和触发反例。（量化上述函数的主要原因是它是 Coq 中的（或）原始连接词。）如果你想要例子，我建议例如

~forall P Q: Prop, P -> Q.
~forall P: Prop, P -> ~P.

有一个相关的问题既没有提出也没有回答我的问题，所以我认为它不是重复的。

我有以下定义

Inductive subseq : list nat -> list nat -> Prop :=
| empty_subseq : subseq [] []
| add_right : forall y xs ys, subseq xs ys -> subseq xs (y::ys)
| add_both : forall x y xs ys, subseq xs ys -> subseq (x::xs) (y::ys)
.

使用这个,我希望证明以下引理

Lemma del_l_preserves_subseq : forall x xs ys, subseq (x :: xs) ys -> subseq xs ys.

所以,我试着看看subseq (x :: xs) ys做的证明destruct H.

Proof.
  intros. induction H.

3 …

我正在学习 prolog，我对 prolog 使用矛盾证明的说法感到困惑：

解析证明过程利用了一种被称为“归谬法”的技术：假设要证明的公式是假的，并证明这会导致矛盾，从而证明要证明的公式实际上是正确的。

他们展示了以下证明图（基于前面一节建立的规则和事实）：

但如果我倒着读这些步骤，那就是一个简单直接的证明：

/* axiom: tottenham_court_road is connected to leicester_square by northern road */
connected(tottenham_court_road, leicester_square, northern)

/* therefore it's connected to something on some road */
connected(tottenham_court_road, W, L)

/* being connected to something also means it's nearby */
nearby(X,Y):-connected(X,Y,L)

/* Therefore tottenham_court_road is near something */
nearby(tottenham_court_road, W)

这是如何用反证法证明的呢？为什么这是一个比公理链式推理更有用的框架？

我试图证明基于以下定义的引理。

Section lemma.

Variable A : Type.
Variable P : A -> Prop.

Variable P_dec : forall x, {P x}+{~P x}.

Inductive vector : nat -> Type :=
  | Vnil : vector O
  | Vcons : forall {n}, A -> vector n -> vector (S n).

  Arguments Vcons {_} _ _.

Fixpoint countPV {n: nat} (v : vector n): nat :=
match v with
| Vnil => O
| Vcons x v' => if P_dec x then S (countPV v') …

我是一所大学的讲师，参加一门名为“ 类型系统的语言 ” 的课程，在最后一次讲解中，该教授将以下示例用于类型理论的归纳证明：

假设存在归纳定义的自然数（出于某种原因，他坚持称其为术语），而我们在它们上递归定义了一个大于函数。我们可以证明，对于每一个n，它都拥有（suc n> n）。

我准备了以下Coq代码以在类中实现此代码：

Inductive term : Set :=
  | zero
  | suc (t : term)
.

Fixpoint greaterThan (t t' : term) {struct t} : bool :=
  match t, t' with
   | zero, _ => false
   | suc t, zero => true
   | suc t, suc t' => t > t'
  end
where "t > t'" := (greaterThan t t').

Lemma successorIsGreater : forall t : term, suc t > t = …