期刊名称:Lecture Notes in Engineering and Computer Science
印刷版ISSN:2078-0958
电子版ISSN:2078-0966
出版年度:2018
卷号:2233&2234
页码:489-492
出版社:Newswood and International Association of Engineers
摘要:Theory exploration has been investigated as the
lemma generation methods which play important role in automation
of theorem provers. In our previous research on
exploration of equational inductive theorems, we have found
that in some cases it is important to find syntactically complex
theorems for deriving other theorems which is hard to directly
prove by induction. In this paper we discuss on the details of
such cases through an example.
关键词:inductive theorem proving; term rewriting;
systems; theory exploration