Towards United Reasoning for Automatic Induction in Isabelle/HOL

TL;DR

This paper introduces united reasoning, a new approach that combines deductive and inductive methods to enhance the automation of inductive theorem proving in Isabelle/HOL.

Contribution

It proposes a novel unified reasoning framework that integrates multiple reasoning styles to improve automatic inductive theorem proving capabilities.

Findings

Successfully combines deductive and inductive reasoning methods.

Enhances automation in inductive theorem proving.

Shows promising results in Isabelle/HOL environment.

Abstract

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.