Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

0
votes
0answers
21 views

How to prove that this TSP variation is NP-Hard?

The problem is as follows: given a list of cities, a list of distances between them, and upper bounds for date/times that the cities must have been visited by, compute the shortest (optimal) going ...
1
vote
1answer
25 views

Proof for Turing Machines being able to simulate any algorithm in the same time complexity

I have always read that Turing machines can simulate any algorithm, without changing the time complexity of the algorithm, and hence it is easier to study the Turing machine equivalent of the ...
1
vote
1answer
36 views

Proof By Contradiction - Hamiltonian Paths and Cycles

Was hoping if anyone had any way to prove the following claim using proof by contradiction Let $G = (V, E)$ be a simple graph with at least one vertex, and let $G'$ be the graph formed by adding a ...
0
votes
1answer
19 views

Showing $2^x$ is a lower bound

How do I show that $2^x - x^2 \in \Omega(2^x)$? Basically, I know that this means that $\exists a, x_0 \in \mathbb{R^+}, \forall x \in \mathbb{N}, a.2^x \leq 2^x - x^2$. I worked around a bit with ...
1
vote
1answer
34 views

How to prove the correctness of an algorithm for sub-sequence counting using induction?

This code is found from https://www.geeksforgeeks.org/find-number-times-string-occurs-given-string/ How to prove it? (The precondition implies the postcondition) Precondition: 0 ≤ m ≤ len(a) and 0 ≤ ...
1
vote
0answers
23 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
4answers
76 views

Is there a *simple* proof that the intersection of a CFL and a regular language is a CFL?

I am following a course on complexity theory where languages are a part of the course. There is a proof that no matter how hard I try to understand, it is till so complex that I cannot make it to half ...
0
votes
1answer
14 views

There could not be an edge from u to v in a DAG, if w is before v in a topological order

I am trying to prove that given a DAG. There exists a valid topological ordering that has v in front of u iff there is no path from u to v. The proof is related to the fact that reverse DFS post ...
2
votes
0answers
22 views

Challenging exercises for proof correctness [closed]

I would like to know where I can find challenging exercises that ask to prove the correctness of an algorithm. The invariant of most of the exercises I’ve found on the internet are quite easy (...
0
votes
1answer
47 views

lower bound proof with adversary argument

We have to run a song on a Walkman, for that we need 2 full batteries. Let's say we have a mixed set of 30 batteries (15 are empty and and 15 are full) and then only way to test if the battery is full ...
2
votes
1answer
42 views

How to reduce a problem?

I am a bit confused on how to reduce a problem. I'll give an example: Let's say there is a problem called HALTEMPTY and we know it is undecidable. $HALTEMPTY_{TM} = \{\langle M\rangle \mid M \text{ ...
3
votes
1answer
47 views

Undecidable problem intersection of two DCFL languages is DCFL?

We have two deterministic pushdown automatas A and B, which languages are deterministic context-free. The problem is to decide if there exists a deterministic pushdown automata, which language is an ...
1
vote
0answers
41 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 :...
2
votes
1answer
42 views

How to Apply Elementary Axioms from Kleene Star to an Inequality

Axioms For * \begin{align} 1 + aa^* &\leq a^* \\ 1 + a^*a &\leq a^* \\ b + ax &\leq x \to a^*b \leq x \\ b + xa &\leq x \to ba^* \leq x \\ \end{align} Elementary Results \begin{...
6
votes
3answers
2k views

Prove that A** = A*, where A is a language over Σ*

Let $\mathcal A$ be an arbitrary language over $\Sigma^*$ Proof. To prove, $\mathcal A^{**} = \mathcal A^* $ $\mathcal A^{**} = \left( \mathcal A^0 \cup \mathcal A^1 \cup {...} \cup \mathcal A^n \...
3
votes
1answer
34 views

Any finite Graph G with all V have at least degree of 2, is it true that every vertex is necessarily contained IN a cycle?

As title, (note: this questions is asking weather or not all vertices are contained IN a cycle not asking if the G contains a cycle. My attempt is that: So this graph would be an counter example ...
3
votes
1answer
89 views

Relating a proof to a Haskell program

I am trying to relate the following integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ and its proof to its role as a specification of ...
5
votes
1answer
99 views

Is it possible to simulate a fair coin with a finite number of tossing of a biased one?

It is a classic problem to simulate a fair coin with a biased one. According to Fair Coin (wiki), John von Neumann gave the following procedure: Toss the coin twice. If the results ...
0
votes
1answer
44 views

Does indirect diagonalization a relativize technique?

My main question is can with R.kanon , Fortnow ,... technique that shows lower bounds for SAT seperate P and NP ? Baker-Gill-Solovay showed that $P?=NP$ could not be solved with relativization. Does ...
3
votes
1answer
64 views

Removing arithmetic within recurrences

A similar question was asked here: Solving recurrences using substitution method, but I am still somewhat hazy as to how this process works. Say, for $T(n) = T(\lceil n/5 \rceil + 36) + n \log n$ ...
3
votes
1answer
48 views

How to prove that a string is made up of subsequences occurring some arbitrary number of times using concatenation?

How to prove that a string, s is made up of n > 1 subsequences occurring some arbitrary number of times using concatenation ...
1
vote
1answer
39 views

Prove that $f^{-1}:\mathbb{N} \rightarrow \mathbb{N}$ is partial recursive

I'm stuck on this problem: Given $f:\mathbb{N} \rightarrow \mathbb{N}$ a partial recursive function that is also injective and total. Prove that the function $f^{-1}:\mathbb{N} \rightarrow \mathbb{N}$...
1
vote
1answer
69 views

Prove that $D =\{x \in \mathbb{N} | \Phi_x(x)\uparrow\}$ is **not** recursively enumerable

So I tried to prove that $D =\{x \in \mathbb{N} | \Phi_x(x)\uparrow\}$ is not recursively enumerable in the following way: let's suppose that $g$ is the computable function that represents $D$ $$g(x) ...
1
vote
1answer
33 views

Prove that $L^r$ is context free without alphabet

I'm stuck with this problem: Given $L$ a CFL on the alphabet $\Sigma$. Prove that $L^r=\{x^r|x\in L\}$, where for each $a\in\Sigma$ and $y\in\Sigma^*$, $$\epsilon^r=\epsilon,$$ $$(ay)^r=y^ra,$$ is ...
3
votes
1answer
48 views

Why is the graph inside Graham Scan always planar

One of the ways to prove that Graham Scan constructs convex hull in linear time is using planarity of the graph obtained by running the algorithm. This graph is always planar, so according to Euler's ...
0
votes
1answer
34 views

Is Loop Invariant Proof a form of Induction?

As far as I see, what computer scientists refer to as loop invariant proofs are exact replicas of induction proof. Is it true? Can I state that loop invariant proof implies an induction? Is there a ...
1
vote
0answers
16 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 ...
0
votes
1answer
51 views

How CompCert “proves” different things in its codebase

In order to understand examples of formal proofs, I am interested in how CompCert applies "proof" techniques. Specifically, I am wondering what a particular example is of something CompCert "proves" ...
1
vote
0answers
31 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. ...
0
votes
2answers
102 views

An example of something you can formally verify with proofs in Software Development

I have been working on understanding formal verification of software. Formal methods include things like modeling your software with Petri Nets, Automata, or State-Transition Graphs. Other techniques ...
1
vote
1answer
42 views

How to Specify the Behavior of Automata for Verification

I am wondering what it takes to "verify" or "prove" that an automaton is correct. What the components are that are required. It seems that an automaton would be an easier thing to formally verify as ...
2
votes
0answers
42 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 ...
-1
votes
1answer
59 views

NP-completeness of vertex cover

Show that the following language is NP-complete $$ L = \{ \langle G,k \rangle \mid \text{$G$ is a graph with a set $S$ of $k$ vertices hitting every edge of $G$}\}. $$ I know I should reduce the ...
0
votes
0answers
28 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=...
1
vote
2answers
41 views

How to prove a side effect in a function

I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and ...
3
votes
1answer
56 views

High-level requirements for a Proof of “Saving to the Database”

This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the ...
2
votes
1answer
33 views

Understanding Hoare Logic Axioms

Given these 5 axioms of Hoare Logic: \begin{array}{cl} \frac{}{\{\phi([x \leftarrow E])\}\ x := E\ \{\phi(x)\}} & \mathtt{Assignment}\\\\ \frac{\{\phi\}\ P_1\ \{\eta\} \quad \{\eta\}\ P_2\ \{\psi\...
0
votes
1answer
49 views
1
vote
1answer
50 views

If a Triple Graph Grammar rule counts as a Mathematical Proof

I am intrigued by Triple Graph Grammars (TGG) as a potential for formal mathematical proof. Triple Graph Grammars (TGGs) are a technique for defining the correspondence between two different ...
2
votes
1answer
121 views

Correctness of lower bound proof

I am working on this exercise with the purpose of learning how to provide proper proofs and I would like to know if my proof for the following problem is correct. Given a sorted array $A$ (of $n$ ...
1
vote
2answers
106 views

Is IEEE 754 float arithmetic associative, commutative, distributive, etc? Why?

Does the associative/commutative/distributive/etc property hold for arithmetic performed with IEEE 754 floats? Obviously the answer is no to most of those questions, but do any of the properties of ...
0
votes
1answer
50 views

Show that C(n) = {a^k | k is a multiple of n} is a regular language

I came across this question in an exam book and was unable to find a solution: Prove that C(n) = {a^k | k is a multiple of n} is a regular language for every natural number n ≥ 1. I wasn't able to ...
0
votes
2answers
42 views

Definition of InLeft and InRight

So in reading I have come across the terms "InLeft" and "InRight" and I am unable to find a concrete definition for it. I have found it used in the specification for COQ, and in some notes on ...
2
votes
1answer
69 views

Find the loop invariant of the given while loop

I don't know how to find a loop invariant. I'm not sure where to start. Can anyone find the loop invariant of the given program and explain your method please. ...
4
votes
1answer
95 views

Can't Understand this Subset Construction Proof

This proof is from Introduction to Automata Theory Languages and Computation by Hopcroft & Ullman and is regarding a 'bad case' for subset construction. The NFA which is being converted is as ...
0
votes
0answers
83 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
1answer
40 views

Prove that the number of full nodes plus one is qual to the number of leaves in a nonempty binary tree

I'm trying to write an induction statement to prove a full node in a tree but I have no idea how to do that. I've always been terrible when it comes to logic. Where do I even start with this? I know ...
2
votes
1answer
184 views

Proving correctness of an iterative Fibonacci algorithm

One of the questions in the problem sets that I'm struggling in is this specific number that asks me to prove an iterative Fibonacci algorithm. The algorithm is written below: ...
0
votes
1answer
276 views

Prove that Big-O is transitive by relation. What does it mean by 'by relation'?

Prove $f(n) = O(g(n))$ and $g(n) = O(h(n))$, then $f(n) = O(h(n))$. The question is Prove that Big-O is transitive by relation. What does it mean by ...
5
votes
1answer
186 views

Analogy between Gödel's incompleteness proof and Richard's argument

If we take a look at Gödel's paper “On formally undecidable propositions”, the first self referential proof given in the paper, with the following formula: $$n \in K \equiv \overline{\textit{Bew}}[R(...