On the structure of generalized rough sets

In this paper we consider some fundamental properties of generalized rough sets induced by binary relations on algebras and show that

1.

Any reflexive binary relation determines a topology.

2.

If θ is a reflexive and symmetric relation on a set X, then O={A⊆X|θ_-(A)=A} is a topology such that A is open if and only if it is closed.

3.

Conversely, for every topological space (X,O) satisfying the condition that A is open if and only if it is closed, there exists a reflexive and symmetric relation R such that O={A⊆X|R_-(A)=A}.

4.

Let θ be an equivalence relation on X. For any pseudo ω-closed subset A of X, θ₋(A) is an ω-closed set if and only if ω(x, x, … , x) ∈ θ₋(A) for any x ∈ X.

Moreover we consider properties of generalized rough sets.     

Relations and functions in multiset context

A multiset is a collection of objects in which repetition of elements is significant. In this paper an attempt is made to generalize the concepts of relation, function, composition and equivalence in the multiset context. As a pre-requisite a brief survey of the axiomatic approach to the multiset theory is also presented.     

Formal Proofs About Rewriting Using ACL2

We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization and representation aspects of our work using the first-order, quantifier-free logic of ACL2 and we sketch some of the main points of the proof effort. First, we present a formalization of abstract reduction systems and then we show how this abstraction can be instantiated to establish results about term rewriting. The main theorems we mechanically proved are Newman's lemma (for abstract reductions) and Knuth–Bendix critical pair theorem (for term rewriting).     

Addressed Term Rewriting Systems: Syntax, Semantics, and Pragmatics: Extended Abstract

We present a formalism called Addressed Term Rewriting Systems, which can be used to define the operational semantics of programming languages, especially those involving sharing, recursive computations and cyclic data structures. Addressed Term Rewriting Systems are therefore well suited for describing object-based languages, as for instance the family of languages called , involving both functional and object-based features.     

Logical Semantics for the Rewriting Calculus

The Rewriting Calculus has been proposed as a language for defining term rewriting strategies. Rules are explicitly represented as terms, and are applied explicitly to other terms to transform them. Sets of rules may be applied to (sets of) terms non-deterministically to obtain sets of results. Strategies are implemented as rules which accept other rules as arguments and apply them in certain ways. This paper describes work in progress to strengthen the Rewriting Calculus by giving it a logical semantics. Such a semantics can provide crucial guidance for studying the language and increasing its expressive power. The latter is demonstrated by adding support to the Rewriting Calculus for what we call higher-form rewriting, where rules rewrite other rules. The logical semantics used is based on ordered linear logic. The paper develops the ideas through several examples.     

Deduction, Strategies, and Rewriting

Automated deduction methods should be specified not procedurally, but declaratively, as inference systems which are proved correct regardless of implementation details. Then, different algorithms to implement a given inference system should be specified as strategies to apply the inference rules. The inference rules themselves can be naturally specified as (possibly conditional) rewrite rules. Using a high-performance rewriting language implementation and a strategy language to guide rewriting computations, we can obtain in a modular way implementations of both the inference rules of automated deduction procedures and of algorithms controling their application. This paper presents the design of a strategy language for the Maude rewriting language that supports this modular decomposition: inference systems are specified in system modules, and strategies in strategy modules. We give a set-theoretic semantics for this strategy language, present its different combinators, illustrate its main ideas with several examples, and describe both a reflective prototype in Maude and an ongoing C++ implementation.     

基于视图的正则路径查询重写

正则路径查询的重写是实现XML查询重写优化的基础。通过比较正则路径视图和正则路径查询的结构信息,分析了两者之间进行映射应满足的条件,描述了正则路径视图到正则路径查询的映射和基于有穷自动机的映射过滤算法,并从理论上阐明了两个算法的重写等价性。借助于此两个算法,能够极大地减少需要求解的映射数目和提高正则路径查询处理的效率。     

基于PI演算的反XML重写攻击安全模型验证

设计出一个安全模型后,要严格验证其是否满足安全需求是非常重要和必要的。利用形式化方法来检验模型是否满足了安全协议是一种有效的手段。本文针对XML重写攻击,设计出了一个反XML重写攻击的安全模型,然后运用Pi演算形式化方法验证了其有效性、真实性和安全性。     

利用等价类构造有限状态自动机

一类语言由任意字母表上的某种进制的数字串构成，要求该语言中的所有数字串能够整除N；构造有限状态自动机识别该类语言是困难的，本文提出了根据等价类构造一类有限状态自动机的方法。该方法可以针对所有字母表和所有进制的数字串构成的语言，而且满足语言中的所有数字串能够整除任意正整数N。该方法实用、简便。     

Equivalence in template-guided recombination

Template-guided recombination (TGR) is a formal model for the DNA rearrangement which occurs in certain ciliates. In this paper, the equivalence problem for TGR is considered: given two sets of templates, is their action is the same for all operands? This question is motivated by molecular computation, as we view equivalence in TGR as a method for discerning whether modifications to the functioning of a ciliate via the set of templates has any effect on the rearrangement it defines. This motivation is also suggested by recent experiments into the role of RNA in the rearrangement of ciliate DNA. We give a language-theoretic characterization of equivalence which leads to decidability results for common language classes. In particular, we show a positive answer for regular sets of templates. For context-free sets of templates, the answer is negative. The same language-theoretic characterization also applies to intra-molecular TGR. The problem for iterated TGR remains open.     

余等价关系下的粗糙集

二元关系作为一类特殊的集合,可考虑它的余集.文中首先从等价关系的集合属性出发,给出余等价关系的定义及其内部关系刻画,构造基于余等价关系的广义粗糙集,论证其公理化基础.其次研究经典粗糙集和余等价关系下的广义粗糙集之间的相互联系,并在特定条件下借助余等价关系下的广义粗糙集,简化相应经典近似算子的相关运算,刻画基本精确集等重要知识.     

RST与SPA的广义等价

通过对粗糙集理论(RST)中的基本概念正区(Positive Region)、负区(Negative Region)和边区(Boundary Region)与集对分析(SPA)中的基本概念同一度、差异度和对立度的分析,从人类认识世界的这个广义角度探讨了RST与SPA的等价性。     

Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus

We present a call-by-need λ-calculus λ_ND with an erratic non-deterministic operator pick and a non-recursive let. A definition of a bisimulation is given, which has to be based on a further calculus named λ_≈, since the naïve bisimulation definition is useless. The main result is that bisimulation in λ_≈ is a congruence and coincides with the contextual equivalence. The proof is a non-trivial extension of Howe's method. This might be a step towards defining useful bisimulation relations and proving them to be congruences in calculi that extend the λ_ND-calculus.     

论两种改进内模控制系统的等价性

改进型内模控制有两种最常见的形式,针对这两种改进内模控制的研究一直认为它们是两种不同的控制,且其中一种比另一种更为优越.通过深入分析可以证明它们事实上是完全等价的,而且所得等价性结论具有一般性,无论采用何种设计方法、系统连续或离散、对象稳定与否都成立.     

等价闭包矩阵及其算法

1 引言在模糊聚类分析的研究与应用中,基于模糊关系等价闭包的模糊聚类算法,又称等价闭包法是一种重要的方法。等价闭包法即是利用样本间的模糊相似关系矩阵进行模糊矩阵相乘得到模糊等价矩阵进而得到等价闭包矩阵,选取适当的阈值对闭包矩阵截取得到一定的分类。该算法的关键问题就是计算出等价闭包矩阵。设R为模糊相似矩阵,其等价闭包矩阵由下式计算:     

利用FAN算法进行组合电路的等价性检验

讨论了组合电路的等价性检验方法,分析了FAN算法的关键技术。利用该算法进行了组合电路的等价性检验,实验结果表明了该方法的有效性。     

基于先验性指标的试卷等价方法

随着网络化考试这一新型考试方式的逐步流行,如何在节约成本的同时保证考试的公平合理已成为人们日益关注的重点.在研究广义向量空间模型的基础上,综合考虑试卷难度和知识点,提出了一种试卷等价性的计算方法.     

GIS中由单种细节方向关系推理拓扑关系的方法

介绍了一种用细节方向关系来处理与参照对象内部有关方向的方法,以弥补外部方向关系的不足;提出了描述两个方向关系之间的关系的九交模型,并得到了19条根据细节方向关系推理拓扑关系的规则,通过这些规则即可得到未知的拓扑关系,而不需要任何几何计算．由于规则推理比几何计算速度快、内存消耗小,因此推理能够提高基于空间关系的空间数据查询的速度和效率。