# Tag Info

Accepted

### Is it provably true/false that for a program, there exists a proof whether it halts or not?

Actually this is no different from the halting problem unsolvability. If you have any formal system T with a proof verifier program V that can reason about programs (as you desire in your question), ...
• 707

### Combinational logic check if bits is prime

There is no known regularity in the primes, and for small numbers (such as 8 bits naturals), the best is to implement them as a table. If you want an instant answer, one comparator per prime can do. ...
• 8,777

### Is it provably true/false that for a program, there exists a proof whether it halts or not?

Unlike the general halting problem, this problem does not require a mechanical procedure to generate a proof for each program which can potentially depend on the procedure itself, but instead, it ...
• 201
Accepted

### How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?

Algorithm design is known to be an art. There is no magical recipe. It all depends on the mathematical properties of the problems addressed. In the case of sorting, the designers were helped by a few ...
• 8,777

### Using hypercomputation for "impossible" problems?

Nope. Russell's paradox and the liar's paradox aren't undecidable. They aren't even decision problems. As far as we know, hypercomputers don't exist. They are an imaginary idea that don't appear ...
• 152k

### Can we accept that all axioms are equivalent?

What you have discovered is that any two true propositions are logically equivalent (you do not need them to be axioms in your argument, only that they hold). What may be confusing is that the truth ...
• 29.4k
Accepted

### Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$

What prevents me from treating the bottom part as if it was "$-\varphi \land \Gamma \implies \Delta$"? Nothing prevents you! In fact, this is exactly the right idea. You can think of the ...
• 6,757
Accepted

### Is finding a Polytime reduction from $L_1$ to $L_2$ equivalent to proving $L_2 \in P \Rightarrow L_1 \in P$

No, this only works one way. If there is a polynomial time reduction from $A$ to $B$, then $B \in P \implies A \in P$. This works irrespective of the what kind of languages $A$ and $B$ are. The ...
• 111
Accepted

### What is the difference in heap configurations? Separation logic with CVC5 SMT solver

Thanks for the question. The model construction for the separation logic heap in cvc5 was wrong in this case. This will be fixed by https://github.com/cvc5/cvc5/pull/9574.
Accepted

### What defines a byte?

A "byte", as defined by the C and C++ standard, is the accessible unit of memory, and exactly large enough to hold one char, signed char, or unsigned char. It must be at least 8 bits, but ...
• 27.4k
Accepted

### Boolean Logic for Floats

I recommend that you look up 'Fuzzy Logic'.
• 46
Accepted

### Is any 2-CNF has 2-DNF representation?

How about $\phi = (x_1 \vee x_2) \wedge (x_1 \vee x_3) \wedge (x_1 \vee x_4)$? This formula is satisfied iff $x_1$ is true, or $x_2$, $x_3$, and $x_4$ are all true. Suppose that $\phi$ had a $2$-DNF ...
• 26.4k

### Is it possible to write an AND gate using XOR gates?

No Consider W the set of the functions that maps {0, 1}×{0, 1} to {0, 1}. For example, the AND gate (denoted by ^) and the XOR gate (denoted by ⊕) are elements of W. Now, for f ∈ W, define Val(f) in ...

### If computers only work with intuitionistic/constructivist logic, so how it works with binary code?

If I were to attempt to make a computing analogue of this question, it would be this: instead of relating 0 and 1 with 'false' and 'true', suppose we called them 'diverge' and 'halt'. Now by encoding ...
• 2,319
Accepted

### Formal language rewrite rules: strange notation

Yes, I think that's basically the intent. I guess the book is trying to write grammars without grammatical symbols. For me, it's abuse of notation, but that's pretty common. Because there is no formal ...
• 11.7k
Accepted

### substitution of same variable in context-free grammars

As you suspect probably, theorem 6.1 still holds even if $A$ and $B$ are the same variable. This can be seen by following the proof of the theorem, assuming $B$ is $A$. So, it is not correct to say &...
• 38.2k

### How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?

Bubblesort to Quicksort requires some cleverness, but is a quite natural progression. First, you implement Bubblesort, and you find that for 100,000 random items it is indeed very slow. 100,000^2 ...
• 27.4k

### How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?

No matter how much one optimizes its code, a bad algorithm will always be bad. The key to great software is starting with a great algorithm. What distinguishes an algorithm is something that makes it ...
Accepted

### What is the proper way to write logic formula, say concerning graph theory?

The standard logical notation I have seen among computer scientists for saying there exists $x \in X$ such that $\varphi(x)$ holds is to write $$\exists x \in X . \varphi(x).$$ In other words, we use ...
• 152k

### Combinational logic check if bits is prime

Of course, the circuit will just grow rapidly. For 8 bits there is no problem. You check whether bit 0 is 0 or 1. If it is 0, then you check whether the input is 2. If it is 1, then you check bit 7. ...
• 27.4k
Accepted

### Why do simple Logical Gates have an Irrational amount of Bits?

An amount of information does not need to be an integer, just like the weight of an object does not need to be an integer number of grams. One might see as a source of confusion to give the same name ...
• 8,777
1 vote

### How do you write a logic function to determine if one 2s complement binary number is less than another?

This page shows you the formula for a one-bit subtractor with borrows in and out. You can use this as a building block for a three-bits subtractor: https://www.geeksforgeeks.org/full-subtractor-in-...
• 8,777
1 vote

### What is the Kripke semantic for a linear temporal logic?

tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind. Details: Let $P$ be a set of atomic proposition. Write $\Sigma$ for $P$'s powerset. Write $T$ for ...
• 479
1 vote
Accepted

### Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Since you are asking to find any inhabitant, how about $\lambda (x : A). \lambda y : B(x). A$? In other words, we take $P := \lambda (u : A) . \lambda (v : B u) . A$. It looks like part of your ...
• 29.4k
1 vote

### K in SKI combinator calculus: why doesn't it take one parameter since it ignores its second?

Maybe it would help to think about it comparing to functions: $K$ can be interpreted as the function with two arguments that returns the first. In Python, it would be ...
• 12k
1 vote
Accepted

### Proof that propositional resolution is refutation complete

There is an error in the example: $S = \{p_1 \lor p_2, p_1 \lor \lnot p_2 \}$ is actually satisfiable. Every interpretation $I$ that sends $p_1$ to $true$ actually works. With this in mind, notice ...
1 vote

### Does quantum computing imply LPO?

No, this is not possible. It is known that Turing machines can simulate quantum machines (albeit very inefficiently). If there were a quantum machine that realized LPO then we could simulate it on a ...
• 29.4k
1 vote

### "Largest set" in coinductive definitions

I think the precise definition of a final coalgebra might help. Fix a set of symbols $\Sigma$. For any set $X$ define $F(X) = \Sigma \times X$, and for any $f : X \to Y$ let $F(f) : F(X) \to F(Y)$ be ...
• 29.4k
1 vote

### "Largest set" in coinductive definitions

Here is a tentative self-answer. I think it must just be that there is an additional requirement that wasn't mentioned in the tutorials I read, namely that one of the destructors must apply to each ...
• 936
1 vote

### Boolean Logic when one component switches from 0 to 1

Designing pure functions (i.e. output depends only on input) is called combinational logic, and designing stateful logic (i.e. a finite state machine) is called sequential logic. If you're working ...
• 20.2k

Only top scored, non community-wiki answers of a minimum length are eligible