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

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 (**199901_10.pdf** : 55,111 bytes)

Received January 23, 1996; accepted May 12, 1998.

Communicated by Jieh Hiang.