New answers tagged

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
3 votes
Accepted

Boolean Logic for Floats

I recommend that you look up 'Fuzzy Logic'.
user avatar
  • 46
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
0 votes

Elemination of duplicate premise

You can try these slides for proof search in natural deduction-https://fiorentini.di.unimi.it/download/slidesTableaux2015.pdf
user avatar
0 votes

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,...
user avatar
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
-3 votes

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 ...
user avatar
  • 25.2k
0 votes

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 ...
user avatar
  • 304
-2 votes

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 ...
user avatar
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

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$.
user avatar
  • 3,912
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
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,912

Top 50 recent answers are included