A Combined Method Based on Extension Rule and Resolution

Author

Wu, Xia ; Yu, Haihong ; Li, Ying

Author_Institution

Coll. of Comput. Sci. & Technol., Jilin Univ., Changchun, China

Volume

3

fYear

2009

fDate

7-8 Nov. 2009

Firstpage

265

Lastpage

269

Abstract

Theorem proving based on the extension rule is a new reasoning method. It is, in a sense, potentially a complementary method to resolution based method. HRIER is a very fast extension rule algorithm with reduction rules and heuristic function. DR is a fast ordering-based restricted resolution method in proposition logic. In order to make best use of the respective characteristic of the extension rule method and resolution method, this paper proposes a combined algorithm CDE based on HRIER and DR. And then the soundness and completeness of it are proved. The experiment results show CDE is a fast SAT solver.

Keywords

formal logic; inference mechanisms; theorem proving; SAT problem; automated theorem proving; combined DR-ER algorithm; extension rule method; heuristic function; proposition logic; reasoning method; resolution method; Artificial intelligence; Computational intelligence; Computer science; Educational institutions; Educational technology; Erbium; Knowledge engineering; Laboratories; Logic; Mathematics; extension rule method; propositional logic; resolution method; theorem proving;

fLanguage

English

Publisher

ieee

Conference_Titel

Artificial Intelligence and Computational Intelligence, 2009. AICI '09. International Conference on

Conference_Location

Shanghai

Print_ISBN

978-1-4244-3835-8

Electronic_ISBN

978-0-7695-3816-7

Type

conf

DOI

10.1109/AICI.2009.308

Filename

5376644