Multi-lingual handwriting means the script written with more than one language. In this paper, a hierarchical hidden Markov model network-based approach is proposed for on-line recognition of multi-lingual cursive handwritings. Basic characters of language, language network, and intermixed use of language are modeled with hierarchical relations. Since recognition corresponds to finding an optimal path in such a network, recognition candidates of each language are combined with probability without special treatment. Character labels of handwriting, language modes, and segmentation are obtained simultaneously. However, several difficulties caused by multiple language occurred during recognition. Applied heuristic methods are Markov chain for language mode transitions, pairwise discrimination for confusing pairs, and constrained routines for side effects by language related preprocessing methods. In spite of the addition of other language, recognition accuracy of each language drops negligibly on experimental results of multi-lingual with Hangul, English, and Digit case.

Huet and Levy showed that index reduction is a normalizing strategy for every orthogonal strongly sequential term rewriting system. Toyama extended this result to root balanced joinable strongly sequential systems. In this paper, we present a class including all root balanced joinable strongly sequential systems and show that index reduction is normalizing for this class. We also propose a class of left-linear (possibly overlapping) NV-sequential systems having a normalizing strategy.

A computational model for security verification of cryptographic protocols is proposed. Until most recently, security verification of cryptographic protocols was left to the protocol designers' experience and heuristics. Though some formal verification methods have been proposed for this purpose, they are still insufficient for the verification of practical real-time cryptographic protocols. In this paper we propose a new formalism based on a term rewriting system approach that we have developed. In this model, what and when the saboteur can obtain is expressed by a first-order term of a special form, and time-related concepts such as the passage of time and the causality relation are specified by conditional term rewriting systems. By using our model, a cryptographic protocol which was shown to be secure by the BAN-logic is shown to be insecure.

This paper extends left-incompatible term rewriting systems defined by Toyama et al. It is also shown that the functional strategy is normalizing in the class, where the functional strategy is the reduction strategy that finds index by some rule selection method and top-down and left-to-right lazy pattern matching method.

Many rewriting systems, including those of terms, strings, graphs, and conjunction of atoms, are used throughout computer science and artificial intelligence. While the concepts of "substitutions," "places" in objects and the "replacement" of "subobjects" by other objects seems to be common to all rewriting systems, there does not exist a common foundation for such systems. At the present time, many of the theories are constructed independently, one for each kind of rewritten object. In the conventional approach, abstract rewriting systems are used to discuss common properties of all rewriting systems. However, they are too abstract to capture properties relating to substructures of objects. This paper aims to provide a first step towards a unified formalization of rewriting systems. The major problem in their formulation may be the formalization of the concept of "places". This has been solved here by employment of the concept of contexts rather than by formalization of places. Places determine subobjects from objects, while, conversely, contexts determine objects from subobjects. A class of rewriting systems, called β rewriting systems, is proposed. It is defined on axiomatically formulated base structures, called β structures, which are used to formalize the concepts of "contexts" and "replacement" common to many rewritten objects. The class of β rewriting systems includes very important systems such as semi-Thue systems and Petri Nets. Abstract rewriting systems are also a subclass of β rewriting systems.

We propose an on-line writer verification method to improve the reliability of verifying a specific system user. Most of the recent research focus on signature verification especially in the field of on-line writer verification. However, signature verification has a serious problem in that it will accept forged handwriting. To overcome this problem, we have introduced a text-indicated writer verification method. In this method, a different text including ordinary characters is used on every occasion of verification. This text can be selected automatically by the verification system so as to reflect the specific writer's personal features. A specific writer is accepted only when the same text as indicated by the verification system is inputted, and the system can verify the writer's personal features from the inputted text. Moreover, the characters used in the verification process can be different from those in the enrolment process. This method makes it more difficult to get away with forged handwriting than the previous methods using only signatures. We also discuss the reliability of the proposed method with some simulation results using handwriting data. From these simulation results, it is clear that this method keeps high reliability without the use of signatures.

Dynamic Term Rewriting Calculus is a new computation model proposed by the authors for the purpose of formal description and verification of algorithms treating Term Rewriting Systems. The computation of DTRC is basically term rewriting. The characteristic features of DTRC are dynamic change of rewriting rules during computation and hierarchical declaration of not only function symbols and variables but also rewriting rules. These features allow us to program metacomputation of TRSs in DTRC, that is , we can implement in DTRC in a natural way those algorithms which manipulate term rewriting systems as well as those procedures which verify such algorithms. In this paper, we give a formal description of DTRC. We then show some results on confluence property of DTRC.

Term Rewriting System (TRS) is a model of computation and it is used in various application such as algebraic specification. TRS has an inherent concurrency and it is suitable for parallel computing. We have already proposed BOB (Bundle Of Branches), which is a mechanism of data management for parallel rewriting. We have proposed a model of parallel rewriting using BOB and implemented a TRS simulator based on this model on a shared memory parallel computer. Because it fully depends on the feature of a shared memory architecture, that is, a process can access any memory element, it is hard to transport it on a distributed memory parallel computer. In this paper, we propose autonomous BOB model. This model is suitable for a distributed memory architecture since a process uses message passing protocol and the method of load balancing is provided. We implement a TRS simulator using this model on a distributed memory architecture and it runs about 30 times faster on 64 processors than on a single processor.

The currying of term rewriting systems (TRSs) is a transformation of TRSs from a functional form to an applicative form. We have already introduced an order-sorted version of currying and proved that the compatibility and confluence of order-sorted TRSs were preserved by currying. In this paper, we focus on a key property of TRSs, completeness. We first show some proofs omitted in Ref. [3]. Then, we prove that the SN (strongly normalizing) property, which corresponds to termination of a program, is preserved by currying. Finally, we prove that the completeness of compatible order-sorted TRSs is preserved by currying.

We developed the computer calligraphy, that is, a computer formation of brush-written Kanji characters using calligraphic knowledge. The style of brush handwriting depends mainly on the way of using a writing brush. Brush writing skills include the direction of brush at the beginning, curvature and turning the brush, the brush-up at the termination point in a stroke. We make up the calligraphic knowledge base according to the above mentioned brush writing skills. For simulating real brush movement, we represent the brush contact form that is the brush shape on the writing plane as a brush-touch. The system can control the size and direction of this brush-touch during the brush simulation. The system simulates the real brush writing to move the brush-touch along the skeleton letter shape in the standard database. We get the brush written Kanji from the locus of the brush-touch movement. We can extend this system to the new on line training system for brush writing using the simulation of brushtouch movement modified by the pressure, speed and rotation of the writing brush, and the skeleton letters written by a learner from the tablet. This system is also useful for students learning how to write Japanese letters beautifully with brush.

This paper describes an on-line Kanji character recognition method that solves the one-to-one stroke correspondence problem with both the stroke-number and stroke-order variations common in cursive Japanese handwriting. We propose two kinds of complementary algorithms: one dissolves excessive mapping and the other dissolves deficient mapping. Their joint use realizes stable optimal stroke correspondence without combinatorial explosion. Also, three kinds of inter-stroke distances are devised to deal with stroke concatenation or splitting and heavy shape distortion. These new ideas greatly improve the stroke matching ability of the selective stroke linkage method reported earlier by the authors. In experiments, only a single reference pattern for each of 2,980 Kanji character categories is generated by using training data composed of 120 patterns written carefully with the correct stroke-number and stroke-order. Recognition tests are made using the training data and two kinds of test data in the square style and in the cursive style written by 36 different people; recognition rates of 99.5%, 97.6%, and 94.1% are obtained, respectively. Moreover, comparative results obtained by the current OCR technique as applied to bitmap patterns of on-line character data are presented. Finally, future work for enhancing the stroke matching approach to cursive Kanji character recognition is discussed.

In this paper we describa a system for Off-line Recognition of Arabic characters and Numerals. This is based on expressing the machine printed Arabic alpha-numerical text in terms of strokes obtained by MCR (Minimum Covering Run) expression. The strokes are rendered meaningful by a labeling process. They are used to detect the baseline and to provide necessary features for recognition. The features selected proved to be effective to the extent that with simple right to left analysis we could achieve interesting results. The recognition is achieved by matching to reference prototypes designed for the 28 Arabic characters and 10 numerals. The recognition rate is 97%.

Rewriting logic has been proposed as a unified model of parallel and concurrent computation, especially concurrent object-oriented computation and agent oriented computation. In this paper, we present a category-theoretic technique in which simulation relation between concurrent processes described by rewriting logic is analyzed. In this technique, simulation relation is represented by morphisms in the category of concurrent processes. Moreover, this technique is shown to be applicable to Petri nets by modeling them by rewriting logic. By this method, it is acknowledged that our technique is applicable to Petri nets including multi-loops whose treatment is limited in other techniques.

Flora is a functional-style language for object and relational algebra. It has been designed for efficient support of advanced database languages combining rules and objects using compilation and optimization. Flora is a strongly typed language based on an OO data model and incorporating support for collection-oriented computational capabilities. In this paper, we describe the design and architecture of the Flora optimizer which is rule-based, yet doing cost-based optimization. The optimizer uniformly captures logical, semantic and implementation knowledge regarding the execution system and the applications by means of assertions. This framework eases extensibility and enables efficient query rewriting.

This paper describes, from a system architectural viewpoint, how knowledge-based technologies have been utilized in developing EXLOG (an LSI circuit synthesis system) and SOFTEX (a software synthesis system) inside the authors' projects. Although the system architectures for EXLOG and SOFTEX started from the same production systems, consisting of transformation rules in the middle of the 1980's, both branched off in different directions in the 1990's. Based on experiences with EXLOG and SOFTEX, the differences between LSI and software design models are discussed, and the future directions are indicated for the knowledge-based design system architectures.

We extend the theorem of Gramlich on modular termination of term rewriting systems, by relaxing the disjointness condition and introducing the composability instead. More precisely, we prove that if R1, R-1 are composable, terminating term rewriting systems such that their union is nonterminating then for some a {1, -1}, Ra OR is nonterminating and R-aRa is Fa-lifting. Here, OR is defined to be the special system {or(x, y) x, or(x, y) y}, Fa is the set of function symbols associated with Ra, and an Fa-lifting system contains a rule which has either a variable or a symbol from Fa at the leftmost position of its right-hand side. The extended theorem is stronger than the original one in that it relaxed the disjointness and constructor-sharing conditions and allowed the two systems to share defined symbols in common under the restriction of composability. The corollaries of the theorem show several sufficient conditions for decomposability of termination, which are useful for proving termination of term rewriting systems defined by combination of several composable modules.

Dynamic Term Rewriting Calculus (DTRC) is a new computation model aiming at formal description and verification of algorithms treating Term Rewriting Systems (TRSs). In this paper, we show that we can use DTRC to mechanize explicit induction for proving an inductive theorem, that is, we can translate the statements of base and induction steps for proving by induction into a DTRC term. The translation reduces the proof of the statements into the evaluation of the corresponding DTRC term.

This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.

Digital neural networks are suitable for WSI implementation because their noise immunity is high, they have a fault tolerant structure, and the use of bus architecture can reduce the number of interconnections between neurons. To investigate the feasibility of WSIs, we integrated either 576 conventional neurons or 288 self-learning neurons on a 5-inch wafer, by using 0.8-µm CMOS technology and three metal layers. We also developed a new electron-beam direct-writing technology which enables easier fabrication of VLSI chips and wafer-level interconnections. We fabricated 288 self-learning neuron WSIs having as many as 230 good neurons.

This paper proposes an off-line text-independent writer identification method applicable to Japanese and Korean sentences. It is assumed that the writer of a writing in question exists in a certain group of people and that reference writings written by each person in the group can be used for identification. In the proposed method, relative frequencies of some model patterns are counted on the binary pattern of each writing and are used as the feature to measure the distance between two writings. Based on a modified Mahalanobis' distance for this feature, the person whose reference writing is nearest to the writing in question is judged as the writer. The effectiveness of the proposed method is examined through an experiment using Japanese and Korean writings. Error rates in the experiment were different depending on conditions such as volume of reference writings, dimension of adopted features, and number of people to be identified. In some cases, error rates as low as 0% were observed. Error rates tend to be lower in Korean writings probably because Hangul is composed of a smaller number of letters compared to Kanji and Hiragana in Japanese writing.