Hot answers tagged

31 votes
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), ...
user avatar
  • 714
5 votes

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 ...
user avatar
  • 201
3 votes
Accepted

Boolean Logic for Floats

I recommend that you look up 'Fuzzy Logic'.
user avatar
  • 46
3 votes

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. ...
user avatar
  • 3,910
2 votes
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 ...
user avatar
  • 11.3k
2 votes
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 &...
user avatar
  • 34.1k
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,...
user avatar
  • 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. ...
user avatar
  • 25.2k

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