# 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), ...

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

### Boolean Logic for Floats

I recommend that you look up 'Fuzzy Logic'.

### 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. ...
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 ...
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 &...
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,...
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. ...

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