JISE


  [1] [2] [3] [4] [5] [6] [7] [8] [9] [10]


Journal of Information Science and Engineering, Vol. 15 No. 1, pp. 153-164


Completeness of the LELS Inference Rule in Automated Theorem Proving


Chuen-Hsuen Jeff Ho 
Department of Computer Science 
Chung-Cheng Institute of Technology 
Tao-Yuan, Taiwan 335, R.O.C.


    The Extended Linking Strategy (ELS) is a hyper-style strategy whose underlying principle is to control and perform (extend) a series of standard resolution on clauses. However it may be treated as a unique inference rule that serially links several resolution steps into one. We define links and clause chains, and introduce the ideas of ELS with left merging (LELS). We also presented the soundness and completeness proofs for ground LELS and use a fundamental theorem of logic (Herbrand's theorem) and facts about the unification algorithm to show that LELS is, in fact, complete for first-order predicate calculus. Some experimental results are included. Employment of LELS not only prevents an automated proving program from producing too many new clauses, but also enables it to draw in fewer steps conclusions that typically require many steps when unlinked inference rules are used.


Keywords: extended linking, left merging, clause chain, cycling, refutation completeness, induction proof

  Retrieve PDF document (JISE_199901_10.pdf)