Questions tagged [proofs]

Used for questions about existing or possible proofs of a specific theorem or conjecture

Filter by
Sorted by
Tagged with
-4 votes
1 answer
107 views

If I want to end math, where should I start?

I'm a PhD in math, but I'm not good. I'm familiar with Riemannian geometry, a little partial differential equations, and a little algebraic topology. And the other undergraduate courses of math (I ...
Enhao Lan's user avatar
2 votes
0 answers
46 views

Is this variant of Facilities location problem a NP-hard problem?

Given a set of locations $P=\{p_1,p_2,\dots\}$ and a set of facilities $F=\{f_1,f_2,\dots\},|F|\ge k$ on a plane. We want to partition the facilities into $k$ disjoint subsets (each subset has at ...
Jingle's user avatar
  • 21
0 votes
0 answers
46 views

Proving the Equivalence of REGEX r^n and r^{..n} when r Is Nullable

Im seeking clarification and a rigorous proof regarding the equivalence of r^n and r^{..n} in the context of formal languages, particularly when r is nullable. To clarify the terminology: r denotes ...
J.Doe's user avatar
  • 1
1 vote
0 answers
35 views

Overlap operator for simple ( regex-like ) Patterns

( Introduction ) Some Notation lower case letters, $a, b, c$ will be used to denote single symbols Upper case letters, $P, Q, R$ will be used to denote string of symbols $a\!:\!S$ means a string ...
Sam Coutteau's user avatar
0 votes
2 answers
33 views

Combining different length epsilon-ADU hash function families

For context, an $\epsilon$-almost delta universal ($\epsilon$-ADU) hash function family $\mathcal{H} = \{h : M \to D\}$ hashes inputs from $M$ to digests in $D$ such that for any distinct $m, m' \in M$...
orlp's user avatar
  • 720
7 votes
1 answer
155 views

Conversion between NP certificates

This might be a well-known fact, but I can't convince myself of whether this is true. Suppose I have some NP language and two different verifying procedures V and V' for L. For any x in L, is it the ...
Noel Arteche's user avatar
3 votes
0 answers
66 views

What's the difference between "modular" and "compositional"?

When talking about reducing complexity in a software system, we often talk about making it "modular" by breaking it up into multiple modules that are all linked together to form the overall ...
Jonathan Schuster's user avatar
4 votes
1 answer
216 views

Halting problem proofs that do not utilise self-reference or diagonalization

Are there any proofs of the Halting problem that do not involve any self-reference, and diagonalization (or any diagonal argument) whatsoever? All the duplicate questions I have come across end up ...
Alan Whitteaker's user avatar
0 votes
1 answer
139 views

Sources that prove solving 2-SAT with DP takes linear time

Would anyone have any sources that describe/an explanation of how solving 2-SAT using dynamic programming takes a linear amount of time? Can't seem to find a text that proves it in detail/formality. ...
wtfamidoing's user avatar
0 votes
0 answers
41 views

Proof that Sufficiency and Caliberation by group are equivalent notions

I am currently reading through the Fairness and Machine Learning book and I have a problem understanding the proof of Proposition 1 in Chapter 3 (titled Classification) (https://fairmlbook.org/...
Segun Ojo's user avatar
0 votes
1 answer
116 views

On the proof of $PP = P \iff \#P = FP$ in Arora & Barak (Lemma 17.7)

Introduction I am currently studying chapter 17 (of the famous textbook by Arora & Barak [1]) on the complexity of counting and got stuck on the proof of Lemma 17.7, which states $\mathrm{PP} = \...
sebastian's user avatar
  • 173
5 votes
1 answer
168 views

Establishing competing memory limits for pushdown automata

Let $L$ be the language of all even-length strings whose first half is a palindrome. Let $L$ be the language of all even length strings whose first half is imbalanced—with an unequal number of $\...
user326210's user avatar
0 votes
0 answers
64 views

A fundamental question about the proof by induction in session types

I have a question about proof by induction in the domain of session types. Let's assume we have the following lemma: $$ \text{Let}~ \Gamma \vdash P : T. ~~\text{If } P = \mu X. Q ~~\text{then}~~ \...
Coder's user avatar
  • 109
8 votes
1 answer
138 views

Construction of arbitrary functions with exponential-size $MODp \circ MODq$ circuits

It is mentioned in multiple papers [1], [2] that $MODp \circ MODq$ circuits for two distinct primes $p, q$ can compute arbitrary functions in exponential size. However, [1] provides no citation for ...
Jake's user avatar
  • 1,204
4 votes
0 answers
180 views

Any problems for which we know the complexity, but no algorithms with the same time?

I suddenly found myself wondering if there are any problems for which the complexity (time or space or anything else) is proven, say to be O(n^2), but for which the best known algorithms are worse ...
MinusPi's user avatar
  • 59
4 votes
2 answers
109 views

Proving that a given formula in LTL is the smallest way to express it

I am looking for a way to prove that a given LTL formula is expressed with the fewest number of temporal operators possible. I would like to do this to compare the expressive length with other ...
Gokul's user avatar
  • 43
3 votes
1 answer
366 views

How hard is this combinatorial optimisation problem?

Suppose we have multiple intervals $R_1,R_2,...,R_i$ of non-negative integers. These intervals may overlap and we use $R_h(\mathrm{median})$ to denote the median integer in the $h$-th interval $R_h$, ...
user avatar
4 votes
3 answers
415 views

Proving proof system properties within the proof system itself?

While reading about Frege proof systems in [1], I came across the completeness theorem and its proof, which involves a few lemmas introduced first. Here are the first two of those lemmas: $$\begin{...
user avatar
19 votes
3 answers
988 views

Examples of the value of proofs for algorithms

In teaching Intro. Algorithms to undergrads, one of the most difficult tasks is to motivate why they need to know how to prove things about algorithms. (For many students, at least in many US ...
Joshua Grochow's user avatar
7 votes
1 answer
203 views

Document references describing weaknesses for cutting planes and algebraic proof system?

Here, Fortnow says (section 4.3): Since then complexity theorists have shown similar weaknesses in a number of other proof systems including cutting planes, algebraic proof systems based on ...
Jérôme Verstrynge's user avatar
1 vote
1 answer
207 views

Uniqueness of the distribution maximizing the channel capacity

Setting: We look at a discrete memoryless channel which takes an input probability distribution acting over symbols in $\mathcal{X}$ to an output probability distribution over symbols in $\mathcal{Y}$....
user1936752's user avatar
-1 votes
1 answer
70 views

Formally prove that the loops of this sorting algorithm will terminate [closed]

Given is the sorting algorithm Bubblesort ...
kathelk's user avatar
  • 117
1 vote
0 answers
325 views

EXPSPACE proof and its implications

I'm dealing with the min-max regret 0-1 Integer Linear Programming problem (MMR-ILP, for short), which is formulated as below. \begin{equation} \label{eq:nip_obj} \min_{x \in \Phi} \sum_{i = 1}^n ...
Iago Carvalho's user avatar
3 votes
1 answer
693 views

Possible to do Complexity theory with only counting and Pigeonhole

Most of the proofs in the book Computational complexity by Barak and Arora seem to be Pigeonhole in disguise. What are some places in Complexity theory where counting and Pigeonhole was insufficient ...
Turbo's user avatar
  • 12.8k
10 votes
0 answers
260 views

How would proof of the Lindelöf hypothesis improve our understanding of computational complexity classes?

A recent press release from the Viterbi School of Engineering at USC discussed the proof of the Lindelöf hypothesis by Athanassios Fokas, a visiting professor from the Department of Applied ...
Greenstick's user avatar
1 vote
0 answers
140 views

Proof of Sipser-Lautmann Theorem

I have written the following answer as an attempt to prove a variation of Sispser-Lautmann theorem, but it was rejected without any comments. I would appreciate if anyone can find the flaws in this ...
s3683168's user avatar
15 votes
1 answer
1k views

Examples of algorithms and proofs that seem correct, but aren't

In my intro to programming course, we're learning about the Initialization-Maintenance-Termination method of proving an algorithm does what we expect it to. But we've only had to prove that an ...
Marin's user avatar
  • 153
29 votes
1 answer
4k views

What's the status of Babai's Graph isomorphism result?

It's been over a year since his January 2017 retraction and correction. Is there news? If not is this normal for validation to take this long? I would expect it would get plenty of attention. Has ...
Meir Maor's user avatar
  • 434
3 votes
2 answers
704 views

Formally proving no algorithm exists [closed]

Are there standard techniques to show that no algorithms exist for given complexity constraints? For example, consider the following problem. The input is a list of items with exactly one duplicate, ...
user890123818239's user avatar
2 votes
0 answers
216 views

Graph optimization problem with multiple objectives/constraints

Let's assume that we have a directed acyclic graph $G = (V, E)$, non-negative vertex weight functions $w_a(v)$ and $w_b(v)$, and a non-negative edge weight function $t(u,v)$. We can divide vertices in ...
marszall87's user avatar
4 votes
1 answer
491 views

Proof that the graph optimization problem is NP-hard

I'm trying to prove that the following optimization problem is NP-hard: Given a graph $G=(V,E)$, non-negative vertex weight functions $w(v)$ and $s(v)$, and a non-negative edge weight function $t(u,v)...
marszall87's user avatar
8 votes
1 answer
141 views

How to prove relations between "classes" of types?

After reading Effects as Sessions, Sessions as Effects, I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System. In ...
cyberglot's user avatar
  • 181
7 votes
1 answer
407 views

Where is the quote "Informal proofs are algorithms, formal proofs are code" from?

Does anyone know the origin of the quote, Informal proofs are algorithms; formal proofs are code. Its made in Benjamin C. Pierce et al.'s Software Foundations.
Steven Shaw's user avatar
1 vote
2 answers
228 views

Are equalizers of regular functions always regular languages? (My guess is no because PCP, but...)

Edit: I originally defined a regular function as a function computable by a Mealy machine, but Denis pointed out that that was a weaker model than what I was thinking of. So to be more precise, by a "...
BenW's user avatar
  • 113
3 votes
0 answers
235 views

New proofs from "The Book" [closed]

The book "Proofs from The Book", referencing Erdős' notion of God's book, which contains the most beautiful proofs, was published in 1998. Are there any new proofs that should be considered for "...
Shaull's user avatar
  • 5,531
2 votes
1 answer
462 views

Paxos made simple, invariant P2c

I am reading Leslie Lamport's Paxos Made Simple paper. Can someone explain why $P2^c$ implies $P2^b$? $P2^b$ If a proposal with value $v$ is chosen, then every higher-numbered proposal issued ...
PNT's user avatar
  • 21
14 votes
1 answer
648 views

How is the MA version of SETH proven to be false?

According to this paper, which discusses a nondeterministic extension of the Strong Exponential Time Hypothesis (SETH), "[…] Williams has recently shown related hypotheses about Merlin-Arthur ...
user avatar
1 vote
0 answers
71 views

Looking for reference proving polynomial-time bounds for A* search under specific conditions

In the textbook "Artificial Intelligence - A Modern Approach" (Russel, Norvig), it mentions that a sufficient criteria for the A* search algorithm to complete in polynomial time is for the heuristic ...
Bill Province's user avatar
8 votes
3 answers
583 views

Would a proof assuming a physical law be considered sufficient?

I've always wondered if proofs in computer science would be considered sufficient proofs of the proposition if they needed to assume physical laws? For example, I'm wondering what would happen if ...
user541686's user avatar
8 votes
1 answer
606 views

Humanifying computer-generated or computer assisted proofs

I remember reading a blog post displaying two versions of the same proof, one written by a human and the other by a machine, and asked the readers to tell which is which. Trying to google the post ...
SorcererofDM's user avatar
-1 votes
1 answer
167 views

Undecidable Single Programs [closed]

So the halting problem basically states that there cannot exist any finite length algorithm for automatically verifying if other finite length algorithms terminate. But suppose I start listing out ...
Sidharth Ghoshal's user avatar
1 vote
0 answers
123 views

Minimum size counter-example in a 2-machine scheduling problem proof

I'm confused about something in the main proof in this paper (sorry that it's behind a paywall, but I assume many people on here have access to such things through their university and my posting the ...
user124384's user avatar
13 votes
1 answer
1k views

Correctness proofs of classic Paxos and Fast Paxos

I am reading the "Fast Paxos" paper by Leslie Lamport and get stuck with the correctness proofs of both classic Paxos and Fast Paxos. For consistency, the value $v$ picked by the coordinator in phase ...
hengxin's user avatar
  • 2,329
0 votes
0 answers
223 views

Correctness proof of recursive-descent recognizer

Let G be a grammar that contains no left-recursive rules, and we use a recursive-descent recognizer that uses full backtracking, using list of results for example, to recognize strings of G. How ...
Wickoo's user avatar
  • 386
1 vote
0 answers
70 views

Proof of convergence of alternative minimization/maximization [duplicate]

Given a problem \begin{equation} \max_{x\in X} \min_{y \in Y} f(x,y) \end{equation} where $f$ is strongly convex in $Y$ and strongly concave in $X$ How to show that the following iterative ...
user25492's user avatar
6 votes
1 answer
402 views

Would an optimal sorting network ever have to swap two numbers the "wrong" way

Intuitively it seems like an optimal (either minimum depth or minimum gates) sorting network should never have to compare-swap two numbers the "wrong" way (such that the larger one goes into the ...
dspyz's user avatar
  • 916
0 votes
0 answers
288 views

Famous computer science results which correctness is uncertain?

I am asking the following: which of the 'famous' computer science results have been thoroughly checked, and for which ones is the correctness still uncertain? I understand that some proofs are hard ...
Stephan Krilow's user avatar
0 votes
1 answer
91 views

The random densification technique-JL lemma

In Ailon's paper (p.3): How $1/(20nd)$ is obtained?
hoom's user avatar
  • 101
1 vote
0 answers
375 views

Equational Logic and First Order Predicate Logic

I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as CafeOBJ . I wish to use ET+EL to represent and prove sentences ...
Pat's user avatar
  • 179
0 votes
0 answers
93 views

A self-contained proof that OrdHorn relations are tractable?

I'm currently investigating a family of temporal relations called 'Ordered Horn' ($OH$ for short). This class was introduced in 'Reasoning about Temporal Relations: A Maximal Tractable Subclass of ...
NisaiVloot's user avatar
  • 1,292