3 ms·
Either your decision/deduction procedure terminates on all inputs. Then the property you're going after is trivial. Or it doesn't and then the property you're g
by maweki 5y ago
Either your decision/deduction procedure terminates on all inputs. Then the property you're going after is trivial. Or it doesn't and then the property you're going after is generally undecidable.
If you can symbolically evaluate a program and this always works for all input programs, your input programs are already restricted in that they are not computationally complete.
- chriswarbo 5y agoGoing a bit further, this could absolutely be used for a denial-of-service attack; but would otherwise be 'sandboxed', similar to how exploits for a Universal Turing machine are still limited to reading/writing the machine's tape. They can't, for example, hijack an SSH session or whatever (unless there are serious vulnerabilities in the prover/turing-machine implementation)