Towards United Reasoning for Automatic Induction in Isabelle/HOL
Artificial Intelligence
2020-05-27 v1 Logic in Computer Science
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.
Cite
@article{arxiv.2005.12737,
title = {Towards United Reasoning for Automatic Induction in Isabelle/HOL},
author = {Yutaka Nagashima},
journal= {arXiv preprint arXiv:2005.12737},
year = {2020}
}
Comments
This is the pre-print of our short-paper accepted at the 34th Annual Conference of the Japanese Society for Artificial Intelligence, 2020 (https://www.ai-gakkai.or.jp/jsai2020/en)