# Tag Info

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.3k
Accepted

### Boolean Logic for Floats

I recommend that you look up 'Fuzzy Logic'.
• 46
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 &...
• 34.1k

### Elemination of duplicate premise

"All $A$ are $B$" and "All $B$ are $C$" then "All $A$ are $C$", it is called deductive reasoning. If two premises are identical then you don't get actually the deduction,...
• 468
1 vote
Accepted

### How can I prove that LTL formula is valid?

There are two main technique in order to prove validity (or more in general, to solve the problem of satisfiability over a definite model) for a LTL formula. The first one is based on semantic tableau,...
• 800
1 vote

### 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. ...
• 25.2k

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

This is basically the Church-Turing hypothesis. We know there are programs P such that no program X can prove that P halts, or that P doesn't halt. That's not what you asked. You asked "can we ...
• 25.2k

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

When you make an informal statement like "Is it provably true/false that for a program, there exists a proof whether it halts or not?", the "a" article is interpreted as a ...
• 304

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

If you're really asking about every program then of course not. Such proof would need to consider every possible outcome of every choice within the most complex program imaginable… which would make ...

### 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

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

Consider a program that computes the non-trivial zeroes of Riemann's $\zeta$ function by increasing imaginary parts and halts if a real part differs from $\frac12$.
• 3,912
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), ...
• 714