Inductive Proof System

From BusyBeaverWiki
Revision as of 04:34, 24 June 2024 by Sligocki (talk | contribs)
Jump to navigation Jump to search

An Inductive Proof System is an Accelerated Simulator and Decider which operates by automatically detecting and proving transition rules using Mathematical Induction.

Inductive Rule

An inductive rule is a general transition rule (a start and end configuration, generalized with variables for repetition counts) along with a proof. The proof generally has two pieces: the base case and the inductive case. Each is a list of steps where each step is (A) a specific TM transition, (B) an application of the inductive hypothesis, (C) an application of a previously defined rule.

TODO(Shawn): Give examples