The aim of mathematics mechanization is to develop symbolic algorithms for manipulating mathematical objects, proving and discovering theorems in a mechanical way. This paper gives a brief review of the major advances in the field over the past thirty years. The characteristic set method for symbolic solution of algebraic, differential, and difference equation systems are first introduced. Methods for automated proving and discovering geometry theorems are then reviewed. Finally, applications in computer-aided geometric design, computer vision, intelligent computer-aided design, and robotics are surveyed.

Web service is increasingly being applied in solving many universal interoperability problems. Business Process Execution Language (BPEL) is a de facto standard for specifying the behavior of business processes. It contains several interesting features, including scope-based compensation, fault handling and shared-labels for synchronization. In this paper we explore an observation-oriented model for BPEL-like languages, which can be used to study program equivalence. The execution states of a program are divided into five types: completed state, waiting state and divergent state, as well as error state and undo state. The last two states are especially for dealing with compensation and fault handling. Based on the formalized model, a set of algebraic laws is investigated, including traditional laws and BPEL featured laws. The concept of guarded choice is also introduced in this model, which can be used to support the transformation of a parallel program into the form of guarded choice. Two special scopes are introduced: canonical structure and compensation structure, which are used to eliminate undo and compensation construct from finite processes.

Dawning4000A is an AMD Opteron-based Linux Cluster with 11.2Tflops peak performance and 8.06Tflops Linpack performance. It was developed for the Shanghai Supercomputer Center (SSC) as one of the computing power stations of the China National Grid (CNGrid) project. The Massively Cluster Computer (MCC) architecture is proposed to put added-value on the industry standard system. Several grid-enabling components are developed to support the running environment of the CNGrid. It is an achievement for a high performance computer with the low-cost approach.

Plan recognition, the inverse problem of plan synthesis, is important wherever a system is expected to produce a kind of cooperative or competitive behavior. Most plan recognizers, however, suffer the problem of acquisition and hand-coding a larger plan library. This paper is aims to show that modern planning techniques can help build plan recognition systems without suffering such problems. Specifically, we show that the planning graph, which is an important component of the classical planning system Graphplan, can be used as an implicit, dynamic planning library to represent actions, plans and goals. We also show that modern plan generating technology can be used to find valid plans in this framework. In this sense, this method can be regarded as a bridge that connects these two research fields. Empirical and theoretical results also show that the method is efficient and scalable.

We briefly present the basic elements of membrane computing, a branch of natural computing inspired by the structure and functioning of living cells, then we give some details about spiking neural P systems, a class of membrane systems recently introduced, with motivations related to the way neurons communicate by means of spikes. In both cases, of general P systems and of spiking neural P systems, we introduce the fundamental concepts, give a few examples, then recall the types of results and of applications. A series of bibliographical references are provided.

Crosscutting concerns such as logging, security, and transaction, are well supported in the programming level by aspect-oriented programming technologies. However, addressing these issues in the high-level architecture design still remains open. This paper presents a novel approach to supporting crosscutting concern modelling in the software architecture design of component-based systems. We introduce a new element named Aspect  into our architecture description language, ABC/ADL, to clearly model the behavior of crosscutting concerns. Aspect is the first class entity as Component and Connector in ABC/ADL. ABC/ADL Connectors provide the weaving points where the component and aspect crosscut. This approach effectively enables separation of concerns  in high-level architecture design, and facilitates black-box reuse of COTS components.

From 1991 to 2005, China s High Technology Research and Development Program (HTRDP) sponsored a series of technology evaluations on Chinese information processing and intelligent human-machine interface, which is called HTRDP evaluations, or 863  evaluations in brief. This paper introduces the HTRDP evaluations in detail. The general information of the HTRDP evaluation is presented first, including the history, the concerned technology categories, the organizer, the participants, and the procedure, etc. Then the evaluations on each technology are described in detail respectively, covering Chinese word segmentation, machine translation, acoustic speech recognition, text to speech, text summarization, text categorization, information retrieval, character recognition, and face detection and recognition. For the evaluations on each technology categories, the history, the evaluation tasks, the data, the evaluation method, etc., are given. The last section concludes the paper and discusses possible future work.

Energy consumption of parallel computers has been becoming the obstruction to higher-performance systems. In this paper, we focus on power optimization of high-performance interconnection networks for MPI applications in high-performance parallel computers. Compared with the past history-based work, we propose the idea of compiler-directed power-aware on/off network links. There are some idle intervals for network links during the execution of parallel applications, at which the links still consume large amounts of energy. Using on/off network links, compiler first divides load-balancing MPI applications into the communication intervals and the computation intervals, and then inserts the on/off instruction into the applications to switch the link state. To avoid the time overhead of state switching, we use a time estimation technique to analyze the computation time, and insert the on instruction before reaching the communication intervals. Results from simulations and experiments show that the proposed compiler-directed method can reduce energy consumption of interconnection networks by 20~70%, at a loss of less than 1% network latency and performance degradation.

In the context of the Kinematic Theory of Rapid Human Movement, handwriting strokes are considered to be primitives that reflect the intrinsic properties of the neuromuscular system of a writer as well as the basic control strategies that the writer uses to produce such strokes. The study of these strokes relies on the extraction of the different parameters that characterize a stroke velocity profile. In this paper, we present a new method for stroke parameter extraction. The algorithm is described and evaluated under various testing conditions.

P2P worm exploits common vulnerabilities and spreads through peer-to-peer networks. Despite being recognized as a potential and deadly threat to the Internet recently, few relevant countermeasures are found in extant literature. Once it breaks out, a P2P worm could result in unpredictable losses. Based on propagation characteristics of the worm, this paper presents a detection method called PWD (P2P Worm Detection), which is designed based on application identification and unknown worm detection. Simulation result and LAN-environment experiment result both indicate that PWD is an effective method to detect and block P2P worms.