Title :
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
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;
Conference_Titel :
Computational Intelligence and Design (ISCID), 2012 Fifth International Symposium on
Conference_Location :
Hangzhou
Print_ISBN :
978-1-4673-2646-9
DOI :
10.1109/ISCID.2012.223
