2020/05/25 by Yutaka Nagashima, Nagashima, Yutaka
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Formal Methods in Verification
paper · pdf · doi:10.48550/arxiv.2005.12737
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.