Inductive Proof System: Difference between revisions
Jump to navigation
Jump to search
(Stub) |
No edit summary |
||
| Line 1: | Line 1: | ||
An '''Inductive Proof System''' is an [[Accelerated Simulator]] and [[Decider]] which operates by automatically detecting and proving [[Transition rule|transition rules]] using Mathematical Induction. | An '''Inductive Proof System''' is an [[Accelerated Simulator]] and [[Decider]] which operates by automatically detecting and proving [[Transition rule|transition rules]] using Mathematical Induction. | ||
TODO(Shawn): | == 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 | |||
Revision as of 20:03, 14 June 2024
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