Towards United Reasoning for Automatic Induction in Isabelle/HOL
This addresses the long-standing problem of automating inductive theorem proving for theorem provers and formal verification researchers, though it appears incremental as it builds on recent developments.
The paper tackles the challenge of automating inductive theorem proving in Isabelle/HOL by proposing a novel approach called united reasoning, which combines deductive and inductive reasoning methods to automatically prove difficult inductive problems.
Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a novel approach to further automating inductive theorem proving. Upon success, united reasoning takes the best of three schools of reasoning: deductive reasoning, inductive reasoning, and inductive reasoning, to prove difficult inductive problems automatically.