Inductive Proof System: Difference between revisions
Jump to navigation
Jump to search
No edit summary |
No edit summary |
||
| Line 5: | Line 5: | ||
TODO(Shawn): Give examples | TODO(Shawn): Give examples | ||
[[Category:Deciders]] | |||
Revision as of 04:34, 24 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