In this paper, an interactive learning algorithm of context-free language is presented. This algorithm is designed especially for system SAQ, which is a system for formal specification acquisition and verification. As the kernel of concept acquisition subsystem (SAQ/CL) of SAQ, the algorithm has been implemented on SUN SPARC workstation. The grammar to be obtained can represent sentence structure naturally.

From the SAT physical model, a physical hypothesis named PHHY is proposed. By PHHY, it is proved that there is a universally efficient algorithm for solving SAT problem. Then, by square packing problem, the authors show that there are interesting industrial NP-complete problems which can be solved through SAT algorithms, but each way of solving like this will be much worse than that of a certain direct solving.

The process of understanding natural language can be viewed as the process of model construction. This paper? employing Kripke frame for intuitionistic logic semantics as the implement of model construction for natural language, introduces a method of incremental model construction.

In this paper a class of cycle unification problems called type Cpg+r is studied, and an intuitive representation method, called the position supergraph, is presented to analyze or reduce the cycle problem. A typical case of Cpg+r problems is considered and an algorithm is given, which transforms the original problem of Cpg+r that is of the exponential complexity into a new one that is of the linear complexity when using SLD resolution method. These results are of importance for practice and theory.

The accumulation calculus (AC for short) is an interval based temporal logic to specify and reason about hybrid real-time systems. This paper presents a formal proof system for AC, and proves that the system is complete relative to that of Interval Temporal Logic (ITL for short) on real domain.

In this paper a new feature called crosscount for document analysis is introduced.The feature crosscount is a function of white line segment with its start on the edgeof document images. It reflects not only the contour of image, but also the periodicity of white lines(background) and text lines in the document images. In complexprinted-page layouts, there are different blocks such as textual, graphical, tabular, andso on. of these blocks, textual ones have the most obvious periodicity with their homogeneou…

Motion perception is one of the most important aspects of the biological visual system, from which people get a lot of information of the natural world. In this paper, trying to simulate the neurons in MT (motion area in visual cortex) which respond selectively both in direction and speed, the authors propose a novel multiplicative inhibitory velocity detector (MIVD) model, whose spatiotemporal joint parameter K determines its optimal velocity. Based on the Response Amplitude Disparity (RAD) property of MIV…

A new stick text segmentation method based on the sub connected area analysis is introduced in this paper. The foundation of this method is the sub connected area representation of text image that can represent all connected areas in an image efficiently. This method consists mainly of four steps: sub connected area classification, finding initial boundary following point, finding optimal segmentation point by boundary tracing, and text segmentation. This method is similar to boundary analysis method but …

A new type of bivariate generalized Ball basis function on a triangle is presented for free-form surface design. Some properties of the basis function are given, then degree elevation, recursive evaluation and some other properties of the generalized Ball surfaces are also derived. It is shown that the proposed recursive evaluation algorithm is more efficient than those of the old surfaces.

In this paper, the authors describe the principles of Straight Line Strokes illustration, present the mathematical model of the principles, and show how a great number of lines can be implemented as main part of an automated drawing system named Line-Art. Different from traditional drawing art, Line-Art generates pictures without curves, colors, ink marks, brushes, and oil paint, but only with Straight Line Strokes. Generated pictures are composed, clipped, and plotted. The paper also introduces how to use…

Protocol Interoperability testing is an important means to ensure the interconnection and interoperation between protocol products. In this paper, we proposed a formal approach to protocol interoperability testing based on the operational semantics of Concurrent TTCN. We define Concurrent TTCN's operational semantics by using Labeled transition System, and describe the interoperability test execution and test verdict based on Concurrent TTCN. This approach is very helpful for the formation of formal intero…

In this paper, some problems on the topology design of network are discussed. An exact formula to calculate the delay of a line will be provided. In the design, the key problem is how to find some efficient heuristic algorithms. To solve this problem, a nonliner- discrete-capacity assignment heuristic and a hybrid perturbation heuristic are suggested. Then, a practical CAD system which helps design the topology of network will be introduced.