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.

Filter by
Sorted by
Tagged with
1
vote
0answers
21 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
148 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" ...
2
votes
0answers
102 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. ...
6
votes
2answers
2k 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
71 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
210 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 ...
0
votes
1answer
410 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
77 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
72 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
109 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
223 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
75 views

How to apply Operational Semantics to this function

Say I have a function like this: ...
1
vote
1answer
120 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
388 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$ ...
2
votes
2answers
1k 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
609 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 ...
1
vote
2answers
120 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
270 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
441 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 ...
1
vote
0answers
646 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
90 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
867 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
2k 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
215 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(...
1
vote
0answers
50 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 ...
0
votes
0answers
36 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
3k 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 ...
1
vote
0answers
155 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 ...
0
votes
2answers
323 views

Why and how geometric series are used for proofs?

I often see that someone uses geometric series for proofs related to time complexity, but also I can't understand why they are used. Are they making proving easier? And how can I use this 'tool' for ...
0
votes
1answer
288 views

Lower bound of complexity of simple problem

Consider the simple problem: Given a list of objects L of length n, and an object O, determine if O is in L. It is intuitive that there cannot exist an algorithm a with worst-case time complexity ...
2
votes
1answer
576 views

Proving worst-case running time is in $\Omega(n^2)$

I was given the following method to argue that an algorithm $A$ has a worst-case running time of $\Omega(n^2)$: We need to argue that there exists an input $x$ of size $n$, the running time of $A$...
1
vote
2answers
395 views

Naive argument that P ≠ NP

Consider the following naïve argument that any algorithm solving SAT must take $\Omega(2^n)$ time in the worst-case scenario. Let $f(x_1,x_2,\dots,x_n)$ be a Boolean function in conjunctive normal ...
1
vote
1answer
56 views

Proof that if a function is computable with standard programs it is computable with Turing Machines

Where can i find a proof related to the subject mentioned?
0
votes
1answer
57 views

On clarification of intersection of classes definition

How do you define $\oplus P\cap PP$? $L\in\oplus P$ iff $\exists\mbox{ NTM }M:\forall x,\#acc_M(x)\mod2\equiv0$. $L\in PP$ iff $\exists\mbox{ NTM }M:\forall x,\#acc_M(x)>\#rej_M(x)$. Consider ...
5
votes
1answer
543 views

Mathematical proofs implemented purely by Lambda Calculus

I've seen often stated that Lambda Calculus can be used for mathematical proofing but I haven't yet seen any example how it is actually used for the task. Is there a simple example, lambda ...
0
votes
0answers
76 views

How to prove QUADPROG is NP-hard using 3COLOR? [duplicate]

I am given a task to prove using 3COLOR that Quadratic Programming is NP-hard. Does anyone have a clue on how this is meant to be done?
0
votes
2answers
171 views

Computational Complexity and P vs. NP, A New Insight [closed]

There is a preprint on arXiv that states (in my own words). If there are three numbers (digits) and task is to add all three numbers. First we well take two number to add, set aside third number. ...
2
votes
1answer
92 views

Proving or disproving a set of total functions is countable

Let S be the set of total functions from $N \rightarrow M$, such that for each $f \in S$, there is $i > 1$ such that for all $j < i$, $f(i)$ and $f(j)$ are not equivalent Turing machines. ...
-1
votes
1answer
366 views

Must algorithm for comparing numbers investigate all bits?

Suppose algorithm $A$ on a digital computer takes as input integers $x$ and $y$ in binary. The algorithm outputs one if $x=y$, and zero if $x \neq y$. Is there a proof that for any input $x$ and $y$ ...
4
votes
2answers
93 views

Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?

Recently I was reading again this propositions as types paper by Philip Wadler: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf It gives an impression, ...
0
votes
0answers
325 views

Need Help Understanding Proof by Contradiction for Halting Problem

I understand what the halting problem describes, but I do not understand how the proof by contradiction associated with it proves that it is impossible to solve. The proof by contradiction can be ...
0
votes
0answers
147 views

Inductive proof that $n^2 + bn + d$ is $O(n^2)$ using definition of big O

Given that $T(n) = n^2 + bn + d$ then it's $O(n^2)$ if I can prove that: $O(n^2) = \{T(n): \text{there exist positive constants } c, n_0 \text{ such that } \forall n \geq n_0, 0 \leq T(n) \leq cn^2 \}$...
1
vote
2answers
413 views

Element wise product sum of two arrays

I have two arrays, namely $a$ and $b$. Both have the same length $n$. I have to find the maximum value of $\sum a_i b_j$, in which every element can be used at most one time. My algorithm for solving ...
0
votes
0answers
1k views

Expectation for the number of comparisons in a randomized Quicksort

I found this link: http://theory.stanford.edu/~tim/w11/l/qsort.pdf and it kind of theoretically describes how to approach finding expectation for the number of comparisons in a Quicksort. Using ...
2
votes
3answers
120 views

When is the empty word part of $A^+$?

My professor mentioned the below statement in class but without a proof. I am trying to prove it for myself as I don't understand 100% why this is always the case. Given is A, a subset of {0,1}$^*$. ...
0
votes
1answer
107 views

Could the execution of a Haskell program be considered as a proof using equational reasoning

Could the execution of a Haskell program be considered as a proof in equational reasoning. This follows on from my earlier question on Haskell and inductive proof. Currently I am stuck between morally ...
3
votes
1answer
541 views

Does a Haskell program count as an inductive proof?

Is the following statement from [1] true? "Since recursion is the main computational technique, a terminating pure Haskell program counts as an inductive proof of a theorem." My intuition is that ...
2
votes
1answer
103 views

How do you prove that the set of decimal representation of the 4 divisble natural numbers is regular?

This is from an old exam, the last Task no one could solve correctly and I'm curious how it's done :p Show that the set of decimal representation (without leading zeroes) of the divisible numbers by <...
0
votes
1answer
982 views

Proof of correctness of algorithm

Can someone help me prove the correctness of this algorithm: ...
1
vote
2answers
120 views

Is $2^n$ steps enough to tell if DTM will run forever?

In the space hierarchy theorem proof for PSPACE from Wikipedia, we reject the input after $2^{|f(x)|}$ steps on the machine $M$, reportedly to avoid infinite running time. My question is: how is it ...

1
3 4
5
6 7
13