一种新型逻辑函数化简方法——立体化简法

文章在卡诺图化简法的思想基础上设计了一种新型的逻辑函数化简方法——“立体化简法”。用逻辑函数立方体代替卡诺图来表示逻辑函数,在三维立体空间进行逻辑函数的化简,既保持了卡诺图化简法方便、直观、容易掌握的优点,又使得可以方便化简的逻辑函数变量增加至六个;如果采用达到卡诺图化简法五、六变量逻辑函数化简的难易程度的方法,可使化简的逻辑函数变量增加至九个。这种新型的逻辑化简方法使得五、六变量逻辑函数的化简变得非常简单、方便,也使得九变量以内的逻辑函数的化简变得直观、可行。     

A general technique for proving lock-freedom

Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction.     

Bisimulations for a calculus of broadcasting systems

We develop a theory of bisimulation equivalence for the broadcast calculus CBS. Both the strong and weak versions of bisimulation congruence we study are justified in terms of a characterisation as the largest CBS congruences contained in an appropriate version of barbed bisimulation. We then present sound and complete proof systems for both the strong and weak congruences over finite terms. The first system we give contains an infinitary proof rule to accommodate input prefixes. We improve on this by presenting a unitary proof system where judgements are relative to properties of the data domain.     

布尔型模糊系统逼近的充分条件

为了保证布尔模糊系统逼近定义在紧集上任意实值连续函数的逼近精度．给出一个估计布尔模糊系统的输入变量与输出变量各自需要构造的模糊集个数的公式,讨论如何设计布尔模糊系统．以便实现逼近任给的实值连续函数到需要的逼近精度．最后通过一个例子展示了如何设计布尔模糊系统来逼近所给的连续函数的具体方法．     

粗糙集概念与运算的布尔矩阵表示

建立了属性集与布尔矩阵以及逻辑方程组的解之间的关系;在此基础上给出了粗糙集理论中概念与运算的布尔矩阵表示;最后证明了属性约简在布尔矩阵和代数两种不同表示下是等价的。     

Model-order reduction for differential-algebraic equation systems with higher index

In this paper, a new model-order reduction (MOR) approach is presented for reducing large-scale differential-algebraic equation (DAE) systems with higher index. This approach is based upon the balanced truncation, single-point, and multi-point MOR methods. We decompose the DAE system into an ordinary differential equation (ODE) subsystem and a DAE subsystem. The DAE subsystem has the same index as the original DAE system. Then, the balanced truncation method is applied to the ODE subsystem. Both single-point and multi-point methods are used to reduce the DAE subsystem. In generally, the multi-point method can perform better than the single-point method across a wide-range of frequencies. Some numerical examples demonstrate the effectiveness of our approach.     

A logical duality for underspecified probabilistic systems

This paper establishes a Stone-type duality between specifications and infLMPs. An infLMP is a probabilistic process whose transitions satisfy super-additivity instead of additivity. Interestingly, its simple structure can encode a mix of probabilistic and non-deterministic behavior, which, as we show, is strongly related to another well-known such model: probabilistic automata. Our duality puts in relation the category of infLMPs and a category of abstract representations of them based on properties only. We exhibit a Galois connection between these categories and show that we have an adjunct pair of functors when restricted to LMPs only. Our duality also shows that an infLMP can be considered as a demonic representative of a system’s information. Moreover, it carries forward a view where states are less important, and events, or properties, become the main characters, as it should be in probability theory. Along the way, we show that bisimulation and simulation are naturally interpreted in this setting, and we exhibit the interesting relationship between infLMPs and the usual probabilistic modal logics. This paper is an extended version of a Concur ’09 paper [13]; in particular, the comparison of infLMPs with probabilistic automata and the Galois connection are new.     

Specification and refinement of mobile systems in MTLA and mobile UML

We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics.     

Joint decomposition of Boolean functions on the basis of a solution of logic equations

It is proposed that the apparatus of logic equations be used to achieve an exact solution of the problem of joint decomposition of a system of Boolean functions with respect to a two-block partitioning of the set of arguments.     

A graphical user interface for Boolean query specification

Online information repositories commonly provide keyword search facilities through textual query languages based on Boolean logic. However, there is evidence to suggest that the syntactic demands of such languages can lead to user errors and adversely affect the time that it takes users to form queries. Users also face difficulties because of the conflict in semantics between AND and OR when used in Boolean logic and English language. Analysis of usage logs for the New Zealand Digital Library (NZDL) show that few Boolean queries contain more than three terms, use of the intersection operator dominates and that query refinement is common. We suggest that graphical query languages, in particular Venn-like diagrams, can alleviate the problems that users experience when forming Boolean expressions with textual languages. A study of the utility of Venn diagrams for query specification indicates that with little or no training users can interpret and form Venn-like diagrams in a consistent manner which accurately correspond to Boolean expressions. We describe VQuery, a Venn-diagram based user interface to the New Zealand Digital Library (NZDL). In a study which compared VQuery with a standard textual Boolean interface, users took significantly longer to form queries and produced more erroneous queries when using VQuery. We discuss the implications of these results and suggest directions for future work. Received: 15 December 1997 / Revised: June 1999     

一种基于布尔矩阵的新的属性约简完备算法

属性约简是粗糙集理论研究的核心问题之一。现已有学者证明属性约简在布尔矩阵和代数两种不同表示下是等价的,且布尔矩阵表示更加直观。基于此理论本文提出了一种基于布尔矩阵的新的属性约简完备算法,并在此基础上加了一个反向删除过程,直到不能再删为止,保证了算法的完备性。最后通过实例分析证实了其有效性。     

基于布尔矩阵的初等行变换的知识约简算法

给出了布尔矩阵的初等行变换定义，建立了线性逻辑方程组形式的属性约简模型，用布尔矩阵的初等行变换把系数矩阵化为最简矩阵，给出了用系数矩阵和最简矩阵判定绝对必要属性、相对必要属性和绝对不必要属性的三个充分必要条件，并由此提出了一种知识约简的快速算法。     

A user-friendly interface to specify temporal properties of concurrent systems

In model checking environments, system requirements are usually expressed by means of temporal logic formulas. We propose a user-friendly interface (UFI) with the aim of simplifying the writing of concurrent system properties. The tool is endowed with a graphical interface that supplies a set of patterns from the natural language; the defined patterns constitute a logic (UFL) that is adequate to express the classes of properties usually checked on actual systems. Moreover, UFI is integrated with the CWB-NC tool-kit which is a verification environment based on process algebras and the mu-calculus temporal logic; UFI supports the automatic translation of UFL formulas into mu-calculus formulas and save the translation in the format required by the CWB-NC. Nevertheless, UFI is a flexible tool that can be easily integrated with other environments.     

基于布尔推理的极大相容块构造方法

极大相容块是非完备信息系统中的最小知识单元,在非完备信息系统的知识表示、属性约简、粒度分析及知识获取方面有重要的应用价值。提出了一种获取非完备信息系统中极大相容块的方法。通过定义的区分关系,构造了新的布尔函数,证明了极大相容块与构造的布尔公式的素蕴含之间存在一一对应的关系。因此,这种新的布尔函数可以被用来获得系统的所有极大相容块,这将有助于非完备信息系统中的知识获取。     

The vmf90 program for the numerical resolution of the Vlasov equation for mean-field systems

The numerical resolution of the Vlasov equation provides complementary information with respect to analytical studies and forms an important research tool in domains such as plasma physics. The study of mean-field models for systems with long-range interactions is another field in which the Vlasov equation plays an important role. We present the vmf90 program that performs numerical simulations of the Vlasov equation for this class of mean-field models with the semi-Lagrangian method.     

基于布尔剪枝的多值广义量词Tableau推理规则简化方法

Tableau作为自动推理的有效方法之一在许多领域中有重要的应用．该文作者在已提出的布尔剪枝方法基础上,对含广义量词（交和并）规则的简化方法进行研究,建立了一套含广义量词的一阶多值逻辑公式的简化Tableau推理方法．通过实例分析,对简化前后结果对比表明,改进后的Tableau方法,在推理效率上有很大的提高．     

A Shortest 2-Basis for Boolean Algebra in Terms of the Sheffer Stroke

In this article, we present a short 2-basis for Boolean algebra in terms of the Sheffer stroke and prove that no such 2-basis can be shorter. We also prove that the new 2-basis is unique (for its length) up to applications of commutativity. Our proof of the 2-basis was found by using the method of proof sketches and relied on the use of an automated reasoning program. This revised version was published online in August 2006 with corrections to the Cover Date.     

Rule effectiveness in rule-based systems: A credit scoring case study

Rule-based systems may sometimes grow very large, making their acceptance by users and their maintenance quite problematic. One therefore needs to make rule-bases as compact as possible. The classical definition of rule redundancy in the literature is based upon logic and graph theory. Another, complementary, view of redundancy is proposed here. The suggested approach is based on the contribution of individual rules to the overall system’s accuracy.

It is shown here, though an analysis of a real-world credit scoring rule-based system, that by taking into account system’s accuracy, one can sometimes significantly reduce the size of a rule-base; even one which is already free from logic-related abnormalities. The approach taken here is not proposed as a substitution to classical logic and graph-based methods. Rather, it complements them.