Backward Reasoning - Revision history

Polygon: linked Turing machine

2026-04-01T10:54:36Z

linked Turing machine

← Older revision		Revision as of 10:54, 1 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Backward Reasoning''' or '''backtracking''' is a [[decider]] which simulates Turing ~~Machines~~ backwards from all halting configurations, proving the TM as non-halting if a contradiction is met in all possible paths to these halting configurations.		'''Backward Reasoning''' or '''backtracking''' is a [[decider]] which simulates [[Turing machines]] backwards from all halting configurations, proving the TM as non-halting if a contradiction is met in all possible paths to these halting configurations.

	== Method ==		== Method ==

Polygon: Separated the method section from the lead

2026-04-01T10:53:57Z

Separated the method section from the lead

← Older revision		Revision as of 10:53, 1 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Backward Reasoning''' or '''backtracking''' 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.		'''Backward Reasoning''' or '''backtracking''' is a [[decider]] which simulates Turing Machines backwards from all halting configurations, proving the TM as non-halting if a contradiction is met in all possible paths to these halting configurations.

	==History==		== Method ==
			The decider 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.

			== History ==
	* A version of Backward Reasoning is described by [[Shen Lin]] in his 1963 proof of [[BB(3)]], where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>		* A version of Backward Reasoning is described by [[Shen Lin]] in his 1963 proof of [[BB(3)]], where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>
	* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>		* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>
Line 12:		Line 15:
	* In November 2023, the decider is reproduced by int-y1.<ref name=":0"/>		* In November 2023, the decider is reproduced by int-y1.<ref name=":0"/>

	==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.
	* [[Halting Segment]]		* [[Halting Segment]]

	==References==		== References ==
	[[Category:Deciders]]		[[Category:Deciders]]

Sligocki: Link Shen Lin

2025-12-04T17:39:28Z

Link Shen Lin

← Older revision		Revision as of 17:39, 4 December 2025
Line 3:		Line 3:

	==History==		==History==
	* A version of Backward Reasoning is described by Shen Lin in his 1963 proof of [[BB(3)]], where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>		* A version of Backward Reasoning is described by [[Shen Lin]] in his 1963 proof of [[BB(3)]], where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>
	* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>		* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>
	* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>		* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>

Sligocki at 16:30, 3 September 2025

2025-09-03T16:30:38Z

← Older revision		Revision as of 16:30, 3 September 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	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.		'''Backward Reasoning''' or '''backtracking''' 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.

	==History==		==History==
	* A version of Backward Reasoning is described by Shen Lin in his 1963 proof of BB(3), where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>		* A version of Backward Reasoning is described by Shen Lin in his 1963 proof of [[BB(3)]], where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>
	* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>		* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>
	* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>		* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>

Polygon: /* History */ made time consistent

2025-08-30T14:19:51Z

History: made time consistent

← Older revision		Revision as of 14:19, 30 August 2025
Line 3:		Line 3:

	==History==		==History==
	* A version of Backward Reasoning ~~was already used~~ by Shen Lin in his 1963 proof of BB(3), where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>		* A version of Backward Reasoning is described by Shen Lin in his 1963 proof of BB(3), where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>
	* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>		* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>
	* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>		* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>

Polygon: /* See also */ Added Halting Segment

2025-08-30T12:14:51Z

Polygon: Added use in proof of BB(3)

2025-08-30T11:58:30Z

Added use in proof of BB(3)

← Older revision		Revision as of 11:58, 30 August 2025
Line 3:		Line 3:

	==History==		==History==
	* The idea of Backward Reasoning ~~was already~~ used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>		* A version of Backward Reasoning was already used by Shen Lin in his 1963 proof of BB(3), where he calls it back-tracking.<ref>Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614</ref>
			* The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>
	* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>		* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>
	* In May 2022, Backward Reasoning is added to the deciders write-up, becoming section 4. The decider is also applied to the remaining [[BB(5)]] holdouts.<ref name=":0"/>		* In May 2022, Backward Reasoning is added to the deciders write-up, becoming section 4. The decider is also applied to the remaining [[BB(5)]] holdouts.<ref name=":0"/>

Polygon: /* History */ Added reproduction by int-y1 (migrated from Cosearch)

2025-08-29T20:16:10Z

History: Added reproduction by int-y1 (migrated from Cosearch)

← Older revision		Revision as of 20:16, 29 August 2025
Line 9:		Line 9:
	* In October 2022, another bug is found and fixed, leading to the decider briefly being unapplied.<ref name=":0"/>		* In October 2022, another bug is found and fixed, leading to the decider briefly being unapplied.<ref name=":0"/>
	* In August 2023, Backward Reasoning is verified in Coq (now Rocq) by meithecatte.<ref>https://github.com/meithecatte/busycoq</ref>		* In August 2023, Backward Reasoning is verified in Coq (now Rocq) by meithecatte.<ref>https://github.com/meithecatte/busycoq</ref>
			* In November 2023, the decider is reproduced by int-y1.<ref name=":0"/>

	==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.

Polygon: Added history section

2025-08-29T11:46:16Z

Added history section

← Older revision		Revision as of 11:46, 29 August 2025
Line 2:		Line 2:
	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.		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.

			==History==
			* The idea of Backward Reasoning was already used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref>
			* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/>
			* In May 2022, Backward Reasoning is added to the deciders write-up, becoming section 4. The decider is also applied to the remaining [[BB(5)]] holdouts.<ref name=":0"/>
			* In June 2022, a bug in the decider is found and fixed, leading to some less machines being marked as decided.<ref name=":0"/>
			* In October 2022, another bug is found and fixed, leading to the decider briefly being unapplied.<ref name=":0"/>
			* In August 2023, Backward Reasoning is verified in Coq (now Rocq) by meithecatte.<ref>https://github.com/meithecatte/busycoq</ref>
	==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.

			==References==
	[[Category:Deciders]]		[[Category:Deciders]]

Polygon: Expanded beginning

2025-08-27T22:59:04Z

Expanded beginning

← Older revision		Revision as of 22:59, 27 August 2025
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 ~~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.		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]]

← Older revision		Revision as of 12:14, 30 August 2025
Line 14:		Line 14:
	==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.
			* [[Halting Segment]]

	==References==		==References==
	[[Category:Deciders]]		[[Category:Deciders]]