Backward Reasoning

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 $D$ reach a contradiction, it is known that, if the machine halts, it must do so in less than $D$ steps. If the machine runs for $D$ 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.