文献类型：会议论文

英文题名：Proving inductive theorems using witnessed test sets

作者：Shao, Zhiqing[1]; Sun, Yongqiang[2]; Song, Guoxin[1]; Yu, Huiqun[1]

机构：[1]E China Univ Sci & Technol, Dept Comp Sci, Shanghai 200237, Peoples R China

会议论文集：2nd International Conference on Formal Engineering Methods (ICFEM98)

会议日期：DEC 09-11, 1998

会议地点：BRISBANE, AUSTRALIA

语种：英文

摘要：Based on a new approach to deciding ground reducibility we proposed by introducing witnesses, we design an algorithm for proving inductive theorems using witnessed test sets for left-linear rewrite systems. Experimental results show that: compared with the standard test set approach presented by Kapur, Narendran and Zhang, our method generates test sets of smaller size and is more efficient to prove inductive theorems.