Formal Engineering Methods, International Conference on (1998)
Dec. 9, 1998 to Dec. 11, 1998
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.
G. Song, Z. Shao, Y. Sun and H. Yu, "Proving Inductive Theorems using Witnessed Test Sets," Formal Engineering Methods, International Conference on(ICFEM), Brisbane, Australia, 1998, pp. 158.