Automated Reasoning with Extended Linking and Left Merging

Proceedings of the Fourth Bar-Ilan Symposium on Foundations of Artificial Intelligence

Volume

Proceedings of the Fourth Bar-Ilan Symposium on Foundations of Artificial Intelligence

Contents

Eztended Linking Strategy(ELS) is a hyper-style strategy whose underlying principle is to control and perform (extend) a series of standard resolution clauses. However it may be treated as a unique inference rule that serially links several resolution steps into one. We have defined the clause chain, introduced the ideas of ELS with left merging (LELS). We also presented the soundness and completeness proofs for ground LELS and used a fundamental theorem of logic (Herbrand’s theorem) and facts about the unification algorithm to show that LELS is in fact complete for the first-order predicate calculus. We also touched on some consequences and benefits of a strategic nature that are present when employing LELS. Employment of LELS enables an automated reasoning program to draw conclusions in fewer steps that typically require many steps when unlinked inference rules are used.