[3G1-ES-1] Knowledge engineering (1)

[3G1-ES-1-03] Towards United Reasoning for Automatic Induction in Isabelle/HOL

〇Yutaka Nagashima^1,2 (1. Czech Technical University in Prague, 2. University of Innsbruck)

Keywords:interactive theorem prover, reasoning, domain-specific language, Isabelle/HOL, proof by induction

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.