Backward Reasoning

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 a contradiction is reached from all possible halting configurations, the TM is shown to be non-halting. 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.