Questions tagged [proof-techniques]

Questions about general methods and techniques for proving multiple theorems. When asking about the proof of a single statement, use tags relating to what the proof is about instead.

68 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
11
votes
0answers
323 views

Proof of PCP theorem

I am reading the proof of PCP theorem in Proof Verication and Hardness of Approximation Problems. The following paragraph appears in section 3 (page 4), "Outline of the Proof of the Main Theorem". ...
6
votes
0answers
216 views

What are methods for showing that concurrent objects are not linearizable?

Linearizability is a well-known correctness condition for concurrent objects. It provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point ...
6
votes
1answer
482 views

Using the Chomsky-Schutzenberger theorem to prove a language is not context-free?

The Chomsky-Schutzenberger representation theorem states that a language $L$ is context-free iff there is a homomorphism $h$, a regular language $R$, and a paired alphabet $\Sigma = T \cup \overline{T}...
5
votes
0answers
74 views

What are the properties of the unsided fold?

Foldl and folr are 2 very important functions for FP and Haskell, but I have never heard much about the unsided fold: fold f [a,b,c,d] = (f (f a b) (f c d)) That ...
4
votes
0answers
65 views

How was the four color theorem proved using brute-force search?

I recently learned some graph theory in Discrete Structures for Computer Science, we learned about the Four Color theorem, I realize there is a mathematical proof for this topic, but how was it ...
4
votes
0answers
85 views

Proof that $P$ is robust against switching between polynomially equivalent encodings

Lemma 34.1 Let $Q$ be an abstract decision problem on an instance set $I$, and let $e_1$ and $e_2$ be polynomially related encodings on $I$. Then, $e_1(Q)\in \mathrm{P}$ if and only ...
3
votes
0answers
230 views

Sequence Alignment with general gap penalties: proof of optimal substructure

I am very well-aware of how optimal substructure for pairwise global sequence alignment using the Needleman-Wunsch algorithm works. However, I have merely seen hand-waving explanations for the ...
3
votes
0answers
60 views

How to prove that the composite strategy is prefix-closed and respects the alternation condition?

I'm doing some research on game semantics using these notes. Currently I'm trying to prove that the definition of composite-strategy is indeed a strategy. I have already proved all the conditions of ...
3
votes
0answers
163 views

Proof of message complexity on the network

I try to provide a strict and mathematical rigorous proof to the following problem in Distributed Algorithms. Prove or make a contradiction: if to vertices $a$ and $b$ on the network $G$ are located ...
2
votes
2answers
68 views

Induction proofs in Big-O notation

I'm not sure how go about this question: Prove the following inequality. For a correct proof, we require a value of the constant $c>0$ and an $n \in \mathbb N$, such that $\forall n>N : f(x)<...
2
votes
0answers
192 views

Given undirected and connected graph G=(V,E). Prove for any DFS run: for any u,v∈V if u.d>v.d then u.d−v.d≥δ(u,v)

Given undirected and connected graph $G = (V,E)$. Prove for any DFS run: for any $u,v \in V$ if $u.d>v.d$ then $u.d − v.d ≥ δ(u,v)$ $δ(u,v)$-distance of a shortest path (not necessarily unique) in ...
2
votes
0answers
86 views

Red-black tree trinode restructuring after insertion and deletion

When performing an insertion/deletion on a red-black tree, how can be argued or proved that it requires at most one/two trinode restructuring(s) respectively? My thoughts so far were: after inserting ...
2
votes
0answers
49 views

Can Pareto Optimality be compared to Nash Equilibrium?

Given a state $s$, and a value function $v^i$ that determines the expected payoff for the i-th agent in that state, can the two definitions below, one of Nash equilibrium and another of Pareto ...
2
votes
0answers
171 views

What you want to “prove” in algorithms

So it seems that you can get pretty far with just type definitions as a formal model of a system. The typed properties verify that the properties will have that type, typed function arguments verify ...
2
votes
1answer
112 views

Language of CFG: $S \to aS | aSbS | \varepsilon$

I'm trying to prove that the language L generated by the CFG $S \to aS | aSbS | \varepsilon$ is the language $L=\{ w \in \{a,b\}^*: \text{every prefix of $w$ has at least as many $a$'s as $b$'s} \}$.I ...
2
votes
0answers
109 views

Formalizing an intuitive linear programming proof

My professor has asked me to prove the following: Prove that we can use an algorithm for linear programming to solve linear inequality feasibility problems. The number of variables and ...
2
votes
0answers
289 views

Analysis of the long division algorithm in the Knuth book (Seminumerical algorithms) 1

I've been reading through the long division algorithm exposed in the Knuth book for a week and I still miss some details. There's an implementation of such algorithm in "Hacker's Delight" by Warren, ...
2
votes
0answers
145 views

Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
2
votes
0answers
164 views

How to prove a Language is neither a Computably enumerable nor Co-Computably enumerable?

What would be the general approach for that? And what are the things that generally overlooked while proving such things? For example, I have a Language, L ={e:$L(M_e)$ such that it accepts only 'a ...
2
votes
0answers
210 views

Proving NP-Completeness by reduction

I'm given a more restricted version of 3-SAT called 3-SAT-M: Problem: 3-SAT-M INPUT: A set of clauses C {c1,...,ck} over n boolean variables {x1,...,xn}, where every clause contains exactly ...
2
votes
0answers
49 views

What are the fundamental principles/algorithms on the process of equation solving?

I have seen a lot of solvers that are capable of, for example, getting an equation such as x ^ 2 + x = 12 and finding x = [3, -4]. I know some of them are implemented by hardcoding special cases. For ...
2
votes
0answers
29 views

How does supercompilers relate to macro tree transducers?

Supercompilers can be used as a generalisation of deforestation of a functional program. Macro Tree Transducers composition can be used to the same effect, using a completely different approach. What ...
2
votes
0answers
1k views

k-Trees Graph Coloring

There is an exercise in Distributed Algorithm I have some difficulties to solve. There are few ideas, however nothing useful at the time. I will appreciate any help with it. Graph $G$ is a $k$-tree ...
1
vote
0answers
66 views

Proving a first order logic theorem in equational logic with a term rewriting system

I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean ...
1
vote
0answers
50 views

How to prove a recursive's function Big-Theta without using repeated substitution, master theorem, or having the closed form?

I have a function defined: $V(j, k)$ where $j, k \in \mathbb{N}$ and $t > 0 \in \mathbb{N}$ and $1 \leq q \leq j - 1$. Note $\mathbb{N}$ includes $0$. $V(j, k) = \begin{cases} tj & k \leq 2 \\...
1
vote
0answers
35 views

Weaker conjectures to prove in order to arrive at P =/= NP

We know we have a long way to go before we come to a proof of P $\neq$ NP. We also know that this road is studded with minor conjectures that will have to be proved/disproved in order to arrive at the ...
1
vote
0answers
47 views

Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode: ...
1
vote
0answers
55 views

How do we know that Icosoku always has solutions?

This is a continuation of a question I asked here. The puzzle Icosoku is now described by Wikipedia as: "The puzzle frame is a blue plastic icosahedron, and the pieces are 20 white equilateral-...
1
vote
0answers
78 views

How to prove that the predecessor of each node in Dijkstra form a tree?

Prove that the array prev[.] computed by Dijkstra’s algorithm, the edges (v, prev[v]) for all v ∈ V , form a tree In order to prove this I used induction. Lemma :...
1
vote
0answers
18 views

Strategy / Technique for Proving Equivalence between Multiple Program Forms

Wondering how to prove different compiled forms of a program to be "effectively the same" or "equivalent". For example, you can have a program represented as your normal nested function calls, or ...
1
vote
0answers
61 views

how real example projects apply formal proof techniques

Given that there are examples of formal proofs used to formally verify real-world software applications, I would like to know what these people and teams actually do to create these formal proofs. ...
1
vote
0answers
338 views

Accounting method vs Potential method for analysing an augmented stack and differences with standard complexity analysis

With reference to chapter 17 of CLRS, (Amortized analysis). I'm trying to understand the differences between the accounting method and the potential method. Let's start with standard analysis of the ...
1
vote
0answers
46 views

How can I prove impossibility of generalizing a given higher order function from pure to monadic or applicative?

There is a great divide in Haskell between pure and monadic algorithms. While the latter are indistinguishable from their usual imperative counterparts, the former can get much more magical. What this ...
1
vote
0answers
107 views

Doubt on dovetailing

Let < M > be an encoding of a Turing machine. L = { < M > | M is a Turing machine that accepts a string of length 2014 } Above language is R.E(even though we have infinite TM's) as we have ...
1
vote
0answers
34 views

What's the polynomial involved in the PCP theorem?

Statements of the PCP theorem always speak of a proof of length $poly(n)$. But what polynomial is that exactly? Could you actually construct the PCP for some mathematical fact in real life?
1
vote
0answers
64 views

Why does the proof that #SAT is in IP stop after m rounds?

I've been struggling to understand why the interactive proof for #SAT stops after only $m$ rounds, where $m$ is the number of variables in the formula $\phi$. I understand that two polynomials of ...
1
vote
0answers
415 views

Minimal number of states

In a recent IT class we got the task of creating a finite state automaton that accepts only the words "auto" "automarke" "tomaten" and "automaten" and no others. Basically the whole class had no ...
1
vote
0answers
279 views

Given a context free grammar, prove if the grammar is ambiguous

Here is a context free grammar that I have been given for practice: Grammar $G = (V,\Sigma,R,S)$ where $V$ is $\{S,A,B,a,b,c\}$ and $\Sigma$ is $\{a,b,c\}$. $R$ has the following rules: $$\begin{...
1
vote
0answers
97 views

Proving an invariant in a recursion using mathematical induction

Given the following pseudocode for function AP(x, y: integer) which returns an integer, ...
1
vote
0answers
125 views

Program equivalence with Structural induction

I recently attended my first lecture on structural induction and the professor stated that structural induction can be used to to prove that two programming languages are equivalent. I am new to ...
1
vote
0answers
185 views

Maximum flow problem with non-zero lower bound

Given $G = (V,E )$ a directed graph, if $ X \subseteq V $ we write $$\begin{align*} \delta ^{+}(X) &= \{ xy\in E \mid x \in X, y\in V - X \} \\ \delta ^{-}(X) &= \delta ^{+}(V -...
0
votes
0answers
61 views

Making Candies - HackerRank question - proof of optimality of a greedy approach

I stumbled across this question in HackerRank: Karl loves playing games on social networking sites. His current favorite is CandyMaker, where the goal is to make candies. Karl just started a ...
0
votes
0answers
21 views

Proof by padding: $\textsf{TIME}(t_1(n)) = \textsf{TIME}(t_2(n)) \implies \textsf{TIME}(t_1(f(n))) = \textsf{TIME}(t_2(f(n)))$

I've been given the task of proving the statement in the title, which I found out it should be called the translational lemma by means of a padding argument; $f$, $t_1$ and $t_2$ are three ...
0
votes
0answers
23 views

How to generate tests using Model-Based Testing paradigm (for a newcomer)

So I just learned of Model-Based Testing. It sounds like this is a practical approach to some level of formal verification of production software applications. As I understand it, you have a ...
0
votes
0answers
47 views

On the complexity of existential and universal quantifiers

I'm trying to analyze the time complexities of the two former kind of quantifiers, I need help figuring out if I'm following the right path or if I'm making mistakes, here's what I've produced so far: ...
0
votes
0answers
40 views

Proof that this sorting algorithm sorts the input

I'm given this "sorting" algorithm and now I'm supposed to prove, that if given an array of integers of length $n$, sort(A,0,n-1) will sort it. ...
0
votes
0answers
64 views

proving DFA stuck

This DFA fulfills: Define a function $diff: \{0,1\}^*\to\Bbb Z$, for $w \in\{0,1\}^*$, $diff(w)=($# of 1's in $w)- ($# of 0's in $w$). Thus, $diff(\epsilon)=0$; $diff(0)=−1$; $diff(1)=1$. Let $L = ...
0
votes
0answers
35 views

Is there any proof that Scheduling with a resource constraint works with two resources?

I've been reading this paper: https://ac.els-cdn.com/S0304397511002623/1-s2.0-S0304397511002623-main.pdf?_tid=bc074517-2b81-4d37-bc92-a5c20dba6b23&acdnat=...
0
votes
0answers
32 views

How to prove that for a decidable problem the problem and the compliment of the problem are semi-decidable?

Given a decidable problem, how would I go about proofing that the problem and the complement of the problem have to be semi-decidable?
0
votes
0answers
2k views

proof why worst case for bubble sort is array sorted in reverse order

Question 1: Let's say we have bubble sort algorithm which sorts numbers in ascending order. Intuitively one might agree that the worst case input for this algorithm is array already sorted in ...