Discovering inductive theorems using rewriting induction
Haruhiko Sato, Masahito Kurihara · 2016
Theory exploration has been investigated as the lemma generation methods which play important role in automation of theorem provers. In order to enlarge the scope of provable theorems in the exploration, in this paper we propose an approach of applying the rewriting induction technique in exploration of inductive theorems. Especially, we propose some heuristics for proof search in the rewriting induction. In the experimentation using two examples, the proposed heuristics improve the efficiency without sacrificing the number of successes in the proof search.