Resolution-based automated reasoning theory is an important and active research field in artificial intelligence. It is not only used to judge the satisfiability of logic formula, but also widely applied to areas such as artificial intelligence, logic programming, problem solving and question answering systems, database theory and so on. With the development of classical and non-classical logic, resolution theory and method based on different logic system has been discussed widely and deeply. In this paper, resolution-based automated reasoning method in a six lattice-valued first-order logic on lattice implication algebra is focused. It is based on resolution principle on Six Lattice-valued First-order Logic L6F(X). In the presented paper, some necessary preliminaries including some necessary definition, resolution principle on L6F(X) and related soundness and completeness are given first. Then resolution method on L6F(X) is given. Because L6F(X) is a non-chain, non-boolean and non-well-ordered algebra structure, the research of resolution method will be helpful support for the application of intelligent reasoning system based on lattice-valued logic which includes incomparable information.

In this paper, an intelligent adjustive method for WfMS is proposed for the workflow process. Firstly, the intelligent adjustive principle is introduced and the operation frame of the adjustive system is shown. Then the activity information table is designed in detail. Subsequently, the modification operations and the running control method are discussed respectively. These researches play an important role in the modification of the workflow process in WfMS.

In daily life, one usually judges a proposition using some linguistic hedges. It strengthens or weakens the degree of the truth value of the proposition. We consider the hedge operators using a qualitative method. Three kinds of qualitative values of the hedge variable with their qualitative operations are presented in this paper. Linguistic hedge of six lattice-valued first-order logic system is introduced and its soft-resolution is also presented. In the process of resolution, the hedge operators will be operated and the result with hedge operators are discussed.

In the present paper, resolution-based automated reasoning theory and algorithm in a finite chain lattice-valued proposition logic are focused. Concretely, the resolution principle, which is based on a finite chain lattice-valued propositional logic FCLP(X) is investigated. And soundness theorem and completeness theorem of this resolution principle are also proved. In order to realize resolution, the concrete algorithm of resolution is discussed. It is hoped that this research will make forward theoretical research of automated reasoning based on lattice-valued logic.

In this paper, graded consequence relations in lattice-valued propositional logic LP(X) are studied. First, valuation sets in LP(X) are defined and their properties are discussed. Based on these, a graded semantic consequence relation between an L-fuzzy set of formulae and a formula is specified. Accordingly, graded syntactic consequence relation is also given. It is demonstrated that these two classes of graded consequence relations are generalizations of counterparts in classical logic and even in LP(X). Furthermore, graded soundness problem, graded completeness theorem and graded deduction theorem for them are given and proven.

Resolution-based automated reasoning theory is an important and active research field in artificial intelligence. It is used to judge the satisfiability of any logic formula. With the development of classical and non-classical logic, the resolution theory and method based on different logic system has been discussed widely and deeply. In the present paper, a new resolution principle by using ultrafilter in LP6(X) is put forward. Different from existed method of resolution, this resolution in this paper is based on ultrafilter of lattice implication algebra. Because of LP6(X) is a non-chain, non-boolean and non-well-ordered algebra structure, resolution based on LP6(X) will be the theoretical foundation of resolution on lattice-valued truth-field. Accordingly, the research in this paper will be helpful supported for the application of intelligent reasoning system based on lattice-valued logic.

In the present paper, as a continuous work about a-resolution principle based on an intermediate element lattice-valued propositional logic IELP(X) whose algebra of truth-value is a relative general lattice-lattice implication algebra(LIA), the resolution principle for the corresponding lattice-valued first-order resolution principle for IELF(X) is focused. Firstly, some concepts about lattice-valued resolution principle for IELF(X) are introduced and the Herbrand theorem for IELF(X) is proved. Then, the a-resolution principle, which can be used to judge if an intermediate element lattice-valued first-order logical formula is always false at a truth-valued level alpha (i.e. alpha-false) is established. And, the completeness theorem and soundness theorom of this alpha-resolution principle are also proved. It is hoped that the current work will serve as a foundation for constructing resolution-based automated reasoning methods for lattice-valued logic capable of dealing with both comparable and incomparable uncertain information.

In the present paper the algorithm of transforming any formula in LP(X) to a pure-generalized conjunction normal form is focused. Concretely, some important concepts and results about lattice implication algebra (LIA), lattice-valued prepositional logic LP(X) and resolution principle based on LP(X) are introduced firstly. Then algorithm of transforming any implication term to a reducible form is considered. Finally, the method of transforming any formula F in LP(X) to a pure-generalized conjunction normal form is given.