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.
為了持續優化網站功能與使用者體驗,本網站將Cookies分析技術用於網站營運、分析和個人化服務之目的。
若您繼續瀏覽本網站,即表示您同意本網站使用Cookies。