New answers tagged logic
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 ...
- 11.3k
3
votes
Accepted
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 &...
- 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
- 59
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,...
- 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
-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 ...
- 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 ...
- 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 ...
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 ...
- 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$.
- 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), ...
- 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. ...
- 3,912
Top 50 recent answers are included