Consistency Property of Finite FC-Normal Logic Programs

Marek＇s forward-chaining construction is one of the important techniques for investigating the non-monotonic reasoning. By introduction of consistency property over a logic program, they proposed a class of logic programs, FC-normal programs, each of which has at least one stable model. However, it is not clear how to choose one appropriate consistency property for deciding whether or not a logic program is FC-normal. In this paper, we firstly discover that, for any finite logic programⅡ, there exists the least consistency property LCon（Ⅱ） overⅡ, which just depends onⅡitself, such that, Ⅱ is FC-normal if and only ifⅡ is FC-normal with respect to （w.r.t.） LCon（Ⅱ）. Actually, in order to determine the FC-normality of a logic program, it is sufficient to check the monotonic closed sets in LCon（Ⅱ） for all non-monotonic rules, that is LFC（Ⅱ）. Secondly, we present an algorithm for computing LFC（Ⅱ）. Finally, we reveal that the brave reasoning task and cautious reasoning task for FC-normal logic programs are of the same difficulty as that of normal logic programs.     

Notes on automata theory based on quantum logic

The main results are as follows: (1) it deals with a number of basic operations (concatenation, Kleene closure, homomorphism, complement); (2) due to a condition imposed on the implication operator for discussing some basic issues in orthomodular lattice-valued automata, this condition is investigated in detail, and it is discovered that all the relatively reasonable five implication operators in quantum logic do not satisfy this condition, and that one of the five implications satisfies such a condition iff the truth-value lattice is indeed a Boolean algebra; (3) it deals further with orthomodular lattice-valued successor and source operators; (4) an example is provided, implying that some negative results obtained in the literature may still hold in some typical orthomodular lattice-valued automata.     

Chattering free adaptive fuzzy terminal sliding mode control for second order nonlinear system

A novel fuzzy terminal sliding mode control （FTSMC） scheme is proposed for position tracking of a class of second-order nonlinear uncertain system. In the proposed scheme, we integrate input-output linearization technique to cancel the nonlinearities. By using a function-augmented sliding hyperplane, it is guaranteed that the output tracking error converges to zero in finite time which can be set arbitrarily. The proposed scheme eliminates reaching phase problem, so that the closed-loop system always shows invariance property to parameter uncertainties. Fuzzy logic systems are used to approximate the unknown system functions and switch item. Robust adaptive law is proposed to reduce approximation errors between true nonlinear functions and fuzzy systems, thus chattering phenomenon can be eliminated. Stability of the proposed control scheme is proved and the scheme is applied to an inverted pendulum system. Simulation studies are provided to confirm performance and effectiveness of the proposed control approach.     

Formal Reduction of Interfaces to Large-scale Process Control Systems

A formal methodology is proposed to reduce the amount of information displayed to remote human operators at interfaces to large-scale process control plants of a certain type.The reduction proceeds in two stages.In the first stage,minimal reduced subsets of components,which give full information about the state of the whole system,are generated by determining functional dependencies between components.This is achieved by using a temporal logic proof obligation to check whether the state of all components can be inferred from the state of components in a subset in specified situations that the human operator needs to detect,with respect to a finite state machine model of the system and other human operator behavior.Generation of reduced subsets is automated with the help of a temporal logic model checker.The second stage determines the interconnections between components to be displayed in the reduced system so that the natural overall graphical structure of the system is maintained.A formal definition of an aesthetic for the required subgraph of a graph representation of the full system,containing the reduced subset of components,is given for this purpose. The methodology is demonstrated by a case study.     

Low power DCVSL circuits employing AC power supply

In view of changing the type of energy conversion in CMOS circuits, this paper investigates low power CMOS circuit design, which adopts a gradually changing power clock. First, we discuss the algebraic expressions and the corresponding properties of clocked power signals. Then the design procedure is summed up for converting complementary CMOS logic gates employing DC power to the power-clocked CMOS gates employing AC power. On this basis, the design of differential cas-code voltage switch logic (DCVSL) circuits employing AC power clocks is proposed. The PSPICE simulations using a sinusoidal power-clock demonstrate that the designed power-clocked DCVSL circuit has a correct logic function and low power characteristics. Finally, an interface circuit to convert clocked signals into the standard logic levels of a CMOS circuit is proposed, and its validity is verified by computer simulations.     

Maximal contractions in Boolean algebras

In the present paper,the concepts of deductive element and maximal contraction are introduced in Boolean algebras,and corresponding theories of consistency and maximal contractions are studied.An algorithm principle is proposed to compute all maximal contractions for a consistent set with respect to its refutation in Boolean algebras.It is pointed out that the quotient algebra of the first-order language with respect to its provable equivalence relation constitutes a Boolean algebra,and hence the computation of R-contractions for closed formulas in first-order languages can be converted into the one in Boolean algebras proposed in this paper.Furthermore,the concept of basic element is introduced in Boolean algebras,which contributes to the definitions of clause and Horn clause transplanted from logic to a special type of Boolean algebras generated by basic elements.It is also pointed out that the computation of R-contractions for clauses in the classical propositional logic can be converted into the one in Boolean algebras generated by basic elements proposed in this paper.     

Randomization of classical inference patterns and its application

By means of randomization, the concept of D-randomized truth degree of formulas in two-valued propositional logic is introduced, and it is proved that the set of values of D-randomized truth degree of formulas has no isolated point in [0,1]. The concepts of D-logic pseudo-metric and D-logic metric space are also introduced and it is proved that there is no isolated point in the space. The new built D-randomized concepts are extensions of the corresponding concepts in quantified logic. Moreover, it is proved that the basic logic connectives are continuous operators in D-logic metric space. Lastly, three different types of approximate reasoning patterns are proposed.     

Call for Papers The First International Conference on Rough Sets and Knowledge Technology (RSKT2006)

Overview Since the introduction of rough sets in 1982 by Professor Zdzistaw Pawlak. we have witnessed great advances in both theory and appications. There has been a rapid growth inresearch and applications of rough sets in Asia, particulary in China. Rough set theory is closely related to knowledge technology ina variety of forms such as knowledge discovery, approximate reasoning, intelligent and multiagent systems design, knowledgeintensive computations that signal the emergence of a knowledge technology age. The essence of growth in cutting-edge, state-of-the-art and promising knowledge technologies is closely related to learning, pattern recognition, machine intelligence and automation ofacquisition, transformation, communication, exploration and exploitation of knowledge. A principal thrust of such technologies is theutilization of methodologies that facilitate knowledge processing. To present state-of-the-art scientific results, encourage academicand industrial interaction, and promote collaborative reserch and developmental activities, in rough sets and knowledge technologyworldwide, a new intemational confrence named Rough Sets and Knowledge Technology (RSKT) is proposed. It will provide a newforum for researchers in rough sets and knowledge technology.     

Decidability of mean value calculus

Mean Value Calculus(MVC)^[1] is a real-time logic which can be used to specify and verify real-time systems^[2].As a conservative extension of Duration Calculus(DC)^[3],MVC increases the expressive power but keeps the properties of DC.In this paper we present decidability results of MVC.An interesting result is that propositional MVC with chop star operator is still decidable,which develops the results of [4]and [5].     

Rough implication operator based on strong topological rough algebras

The role of topological De Morgan algebra in the theory of rough sets is investigated. The rough implication operator is introduced in strong topological rough algebra that is a generalization of classical rough algebra and a topological De Morgan algebra. Several related issues are discussed. First, the two application directions of topological De Morgan algebras in rough set theory are described, a uniform algebraic depiction of various rough set models are given. Secondly, based on interior and closure operators of a strong topological rough algebra, an implication operator (called rough implication) is introduced, and its important properties are proved. Thirdly, a rough set interpretation of classical logic is analyzed, and a new semantic interpretation of ?ukasiewicz continuous-valued logic system ?uk is constructed based on rough implication. Finally, strong topological rough implication algebra (STRI-algebra for short) is introduced. The connections among STRI-algebras, regular double Stone algebras and RSL-algebras are established, and the completeness theorem of rough logic system RSL is discussed based on STRI-algebras.     

An axiomatic characterization of a fuzzy generalization of rough sets

In rough set theory, the lower and upper approximation operators defined by a fixed binary relation satisfy many interesting properties. Several authors have proposed various fuzzy generalizations of rough approximations. In this paper, we introduce the definitions for generalized fuzzy lower and upper approximation operators determined by a residual implication. Then we find the assumptions which permit a given fuzzy set-theoretic operator to represent a upper (or lower) approximation derived from a special fuzzy relation. Different classes of fuzzy rough set algebras are obtained from different types of fuzzy relations. And different sets of axioms of fuzzy set-theoretic operator guarantee the existence of different types of fuzzy relations which produce the same operator. Finally, we study the composition of two approximation spaces. It is proved that the approximation operators in the composition space are just the composition of the approximation operators in the two fuzzy approximation spaces.     

基于T模剩余蕴涵算子的直觉模糊粗糙集

构造并系统研究了直觉模糊T模的剩余蕴涵。在此基础上,推导出了直觉模糊粗糙集的一种构造模型,证明了Pawlak粗糙集、直觉模糊集、模糊粗糙集、粗糙模糊集及模糊T粗糙集都是直觉模糊粗糙集的特殊情形。最后给出并证明了直觉模糊粗糙集的一些性质。     

基于直觉模糊三角模的直觉模糊粗糙集

提出一种基于直觉模糊三角模的直觉模糊粗糙集.首先,定义了直觉模糊集上的T模及其剩余蕴涵,研究了直觉模糊T模的剩余蕴涵的性质,并推导了通用计算表达式;然后,将模糊T粗糙集扩展成直觉模糊粗糙集,证明了模糊T粗糙集、粗糙模糊集和Pawlak粗糙集都是直觉模糊粗糙集的特殊情形;最后,证明了直觉模糊粗糙集的一些性质.     

Uncertainty measures for rough formulae in rough logic: An axiomatic approach

Rough set theory, initiated by Pawlak, is a mathematical tool in dealing with inexact and incomplete information. Various types of uncertainty measure such as accuracy measure, roughness measure, etc, which aim to quantify the imprecision of a rough set caused by its boundary region, have been extensively studied in the existing literatures. However, a few of these uncertainty measures are explored from the viewpoint of formal rough set theory, which, however, help to develop a kind of graded reasoning model in the framework of rough logic. To solve such a problem, a framework of uncertainty measure for formulae in rough logic is presented in this paper. Unlike the existing literatures, we adopt an axiomatic approach to study the uncertainty measure in rough logic, concretely, we define the notion of rough truth degree by some axioms, such a notion is demonstrated to be adequate for measuring the extent to which any formula is roughly true. Then based on this fundamental notion, the notions of rough accuracy degree, roughness degree for any formula, and rough inclusion degree, rough similarity degree between any two formulae are also proposed. In addition, their properties are investigated in detail. These obtained results will be used to develop an approximate reasoning model in the framework of rough logic from the axiomatic viewpoint.     

On fuzzy rough sets based on tolerance relations

Dubois and Prade (1990) [1] introduced the notion of fuzzy rough sets as a fuzzy generalization of rough sets, which was originally proposed by Pawlak (1982) [8]. Later, Radzikowska and Kerre introduced the so-called (I,T)-fuzzy rough sets, where I is an implication and T is a triangular norm. In the present paper, by using a pair of implications (I,J), we define the so-called (I,J)-fuzzy rough sets, which generalize the concept of fuzzy rough sets in the sense of Radzikowska and Kerre, and that of Mi and Zhang. Basic properties of (I,J)-fuzzy rough sets are investigated in detail.     

粗糙集代数与蕴涵格

在粗糙集的代数刻画方面,一个重要方法是在偶序对〈R（X）,R（X）〉构成的集合中通过定义基本运算寻找刻画偶序对所成集合的代数结构。其中,最有影响的代数结构是正则双Stone代数和Nelson代数。本文从偶序对〈T（X）,R（X）〉构成的集合入手,通过定义蕴涵运算证明了偶序对〈R（X）,R（X）〉所成集合构成蕴涵格,讨论了粗蕴涵格与
正则双Stone代数的关系。本文的讨论可为粗糙逻辑和粗糙推理奠定基础。     

基于θ算子的变精度直觉模糊粗糙集*

在模糊近似空间中,结合直觉模糊集的隶属度、非隶属度与模糊蕴涵算子,提出基于θ算子和θ^算子的直觉模糊集及其隶属度和非隶属度的概念,并证明它们一系列性质.然后,结合直觉模糊集与变精度粗糙集,定义基于θ算子的变精度直觉模糊粗糙集,提出求解变精度粗糙集阈值参数β的方法,使用算例分析该方法.     

A resolution-like strategy based on a lattice-valued logic

As the use of nonclassical logics becomes increasingly important in computer science, artificial intelligence and logic programming, the development of efficient automated theorem proving based on nonclassical logic is currently an active area of research. This paper aims at the resolution principle for the Pavelka type fuzzy logic (1979). Pavelka showed that the only natural way of formalizing fuzzy logic for truth-values in the unit interval [0, 1] is by using the Lukasiewicz's implication operator a/spl rarr/b=min{1,1-a+b} or some isomorphic forms of it. Hence, we first focus on the resolution principle for the Lukasiewicz logic L/sub /spl aleph// with [0, 1] as the truth-valued set. Some limitations of classical resolution and resolution procedures for fuzzy logic with Kleene implication are analyzed. Then some preliminary ideals about combining resolution procedure with the implication connectives in L/sub /spl aleph// are given. Moreover, a resolution-like principle in L/sub /spl aleph// is proposed and the soundness theorem of this resolution procedure is also proved. Second, we use this resolution-like principle to Horn clauses with truth-values in an enriched residuated lattice and consider the L-type fuzzy Prolog.