General Form of Alpha-Linear Resolution Method Based on Lattice-Valued First-Order Logic System

Author

Weitao Xu ; Wenqiang Zhang ; Yang Xu

Author_Institution

Coll. of Inf. Sci. & Eng., Henan Univ. of Technol., Zhengzhou, China

Volume

2

fYear

2012

fDate

28-29 Oct. 2012

Firstpage

286

Lastpage

289

Abstract

In this paper we propose a new resolution approach for automated reasoning in artificial intelligence. the general form a-linear resolution method is established in lattice-valued first-order logic system LF(X) based on lattice implication algebra. the soundness theorem is given in LF(X). by using lift lemma, the weak completeness theorem is also investigated in LF(X). This method is to provide a scientific and efficient reasoning tool for theorem proving based on lattice-valued logic system.

Keywords

inference mechanisms; process algebra; theorem proving; α-linear resolution method; artificial intelligence; automated reasoning; lattice implication algebra; lattice-valued first-order logic system; lift lemma; reasoning tool; soundness theorem; theorem proving; weak completeness theorem; Algebra; Cognition; Computational intelligence; Educational institutions; Lattices; Presses; Uncertainty; automated reasoning; general form of a-linear resolution; generalized clause; generalized literal; lattice-valued first-order logic;

fLanguage

English

Publisher

ieee

Conference_Titel

Computational Intelligence and Design (ISCID), 2012 Fifth International Symposium on

Conference_Location

Hangzhou

Print_ISBN

978-1-4673-2646-9

Type

conf

DOI

10.1109/ISCID.2012.223

Filename

6405996