Non-decidability
- Are there non-decidable languages?
- Are there non-acceptable languages?
Software verification
Let there be a decision problem, does a program
ATM is acceptable lemma
ATM is not decidable theorem
This means that there is no general solution for the software verification problem! But there are many methods that do solve the software verification problem under extra assumptions.
Complement of ATM is non-acceptable lemma
Termination problem theorem
Similarly to
The structure of each of the proofs above is very similar - building an impossible program based on a given black-box that we assume to exist. This technique is called Reduction