Backward Reasoning: Difference between revisions
Jump to navigation
Jump to search
m (See also format) |
(Expanded beginning) |
||
| Line 1: | Line 1: | ||
{{Stub}} | {{Stub}} | ||
Backward Reasoning is a [[decider]] which simulates [[Turing machines]] backwards from all possible halting configurations until a contradiction (or an impossible step) is reached. If | Backward Reasoning is a [[decider]] which simulates [[Turing machines]] backwards from all possible halting configurations, creating a tree of possible previous configurations, until a contradiction (or an impossible step) is reached. If, for all possible halting configurations, all leaves of a Backward Reasoning tree of depth <math>D</math> reach a contradiction, it is known that, if the machine halts, it must do so in less than <math>D</math> steps. If the machine runs for <math>D</math> steps from an empty tape, it cannot reach any halting configurations and thus cannot halt. The amount of backward steps which are simulated can also be called the depth with which Backward Reasoning was applied. | ||
==See also== | ==See also== | ||
* [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 4] of bbchallenge's deciders write-up. | * [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 4] of bbchallenge's deciders write-up. | ||
[[Category:Deciders]] | [[Category:Deciders]] | ||
Revision as of 22:59, 27 August 2025
Backward Reasoning is a decider which simulates Turing machines backwards from all possible halting configurations, creating a tree of possible previous configurations, until a contradiction (or an impossible step) is reached. If, for all possible halting configurations, all leaves of a Backward Reasoning tree of depth reach a contradiction, it is known that, if the machine halts, it must do so in less than steps. If the machine runs for steps from an empty tape, it cannot reach any halting configurations and thus cannot halt. The amount of backward steps which are simulated can also be called the depth with which Backward Reasoning was applied.
See also
- Section 4 of bbchallenge's deciders write-up.