• DocumentCode
    2345163
  • Title

    Proving inductive theorems using witnessed test sets

  • Author

    Shao, Zhiqing ; Sun, Yongqiang ; Song, Guoxin ; Yu, Huiqun

  • Author_Institution
    East China Univ. of Sci. & Technol., Shanghai, China
  • fYear
    1998
  • fDate
    9-11 Dec 1998
  • Firstpage
    158
  • Lastpage
    164
  • Abstract
    Based on a new approach to deciding ground reducibility 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 (1991), our method generates test sets of smaller size and is more efficient to prove inductive theorems
  • Keywords
    algorithm theory; rewriting systems; theorem proving; algorithm; ground reducibility; inductive theorem proving; left-linear rewrite systems; witnessed test sets; Algorithm design and analysis; Application software; Character generation; Computer science; Ear; Educational institutions; Sun; System testing; Time measurement;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Formal Engineering Methods, 1998. Proceedings. Second International Conference on
  • Conference_Location
    Brisbane, Qld.
  • Print_ISBN
    0-8186-9198-0
  • Type

    conf

  • DOI
    10.1109/ICFEM.1998.730579
  • Filename
    730579