A channel coding problem with cost constraint for general channels is considered. Verdú and Han derived ϵ-capacity for general channels. Following the same lines of its proof, we can also derive ϵ-capacity with cost constraint. In this paper, we derive a formula for ϵ-capacity with cost constraint allowing overrun. In order to prove this theorem, a new variation of Feinstein's lemma is applied to select codewords satisfying cost constraint and codewords not satisfying cost constraint.

The achievability part of the rate-distortion theorem is proved by showing existence of good codes. For i.i.d. sources, two methods showing existence are known; random coding and non-random coding. For general sources, however, no proof in which good codes are constructed with non-random coding is found. In this paper, with a non-random method of code construction, we prove the achievability part of the rate-distortion theorem for general sources. Moreover, we also prove a stochastic variation of the rate-distortion theorem with the same method.

Vectorial Boolean functions play an important role in cryptography, sequences and coding theory. Both affine equivalence and EA-equivalence are well known equivalence relations between vectorial Boolean functions. In this paper, we give an exact formula for the number of affine equivalence classes, and an asymptotic formula for the number of EA-equivalence classes of vectorial Boolean functions.

Register automaton (RA), register context-free grammar (RCFG) and register tree automaton (RTA) are computational models with registers which deal with data values. This paper shows pumping lemmas for the classes of languages expressed by RA, RCFG and RTA. Among them, the first lemma was already proved in terms of nominal automata, which is an abstraction of RA. We define RTA in a deterministic and bottom-up manner. For these languages, the notion of ‘pumped word’ must be relaxed in such a way that a pumped subword is not always the same as the original subword, but is any word equivalent to the original subword in terms of data type defined in this paper. By using the lemmas, we give examples of languages that do not belong to the above-mentioned classes of languages.

We present an automated lemma generation method for equational, inductive theorem proving based on the term rewriting induction of Reddy and Aoto as well as the divergence critic framework of Walsh. The method effectively works by using the divergence-detection technique to locate differences in diverging sequences, and generates potential lemmas automatically by analyzing these differences. We have incorporated this method in the multi-context inductive theorem prover of Sato and Kurihara to overcome the strategic problems resulting from the unsoundness of the method. The experimental results show that our method is effective especially for some problems diverging with complex differences (i.e., parallel and nested differences).

In this letter, we show the recursive representation of the optimum projection matrix. The recursive representation of the orthogonal projection and oblique projection have been done in past references. These projections are optimum when the noise is only characterized by the white noise or the structured noise. However, in some practical applications, a desired signal is deteriorated by both the white noise and structured noise. In this situation, the optimum projection matrix has been given by Behrens. For this projection matrix, the recursive representation has not been done. Therefore, in this letter, we propose the recursive representation of this projection matrix.

This paper deals with a design problem of an observer-based robust stabilizing controller for a class of polytopic uncertain systems. The proposed controller synthesis differs from the conventional quadratic stabilization based on Lyapunov criterion and is based on the computation of the system's trajectory. In this paper, we show a LMI-based design method of the observer-based robust controller. The effectiveness of the proposed controller design approach is presented through a simple numerical example.

Let G(s)=C(sI - A)-1B+D be a given system where entries of A,B,C,D are polynomials in a parameter k. Then H∞ norm || G(s) ||∞ of G(s) is a function of k, and [9] presents an algorithm to express 1/(||G(s) ||∞)2 as a root of a bivariate polynomial, assuming feedthrough term D to be zero. This paper extends the algorithm in two ways: The first extension is the form of the function to be expressed. The extended algorithm can treat, not only H∞ norm, but also functions that appear in the celebrated KYP Lemma. The other extension is the range of the frequency. While H∞ norm considers the supremum of the maximum singular value of G(i ω) for the infinite range 0 ≤ω ≤ ∞ of ω, the extended algorithm treats the norm for the finite frequency range ω ≤ ω ≤ ω- (ω, ω- ∈ R ∪ ∞). Those two extensions allow the algorithm to be applied to wider area of control problems. We give illustrative numerical examples where we apply the extended algorithm to the computation of the frequency-restricted norm, i.e., the supremum of the maximum singular value of G(i ω) (ω- ≤ ω ≤ ω-).

This paper discusses the behavior of the second-order modes (Hankel singular values) of linear discrete-time systems under bounded-real transformations, where the transformations are given by arbitrary transfer functions with magnitude bounded by unity. Our main result reveals that the values of the second-order modes are decreased under any of the above-mentioned transformations. This result is the generalization of the theory of Mullis and Roberts, who proved that the second-order modes are invariant under any allpass transformation, i.e. any lossless bounded-real transformation. We derive our main result by describing the controllability/observability Gramians of transformed systems with the help of the discrete-time bounded-real lemma.

In our former paper, we formalized a Logic of Multiple-valued Argumentation (LMA) on an expressive knowledge representation language, Extended Annotated Logic Programming (EALP), in order to make it possible to construct arguments under uncertain information. In this paper, We confirm expressivity and applicability by applying LMA to arguments reflecting Easterners' preference over argumentation as well as Eastern thought and philosophy. In doing so, we exploit a wide variety of complete lattices as truth-values, showing the flexibility and adaptability of LMA to various multiple-valuedness required in argumentation under uncertain information. In particular, we consider a significant specialization of LMA to Tetralemma with an Eastern mind. Through various argument examples, it is shown that LMA allows for a kind of pluralistic argumentation, or a fusion of Eastern and Western argumentation.

This paper discusses real-time language recognition by 1-dimensional one-way cellular automata (OCAs) and two-way cellular automata (CAs), focusing on limitations of the parallel computation power. To clarify the limitations, we investigate real-time recognition of cyclic strings of the form uk with u {0,1}+ and k 2. We show a version of pumping lemma for recognizing cyclic strings by OCAs, which can be used for proving that several languages are not recognizable by OCAs in real time. The paper also discusses the real-time language recognition of CAs by prefix and postfix computation, in which every prefix or postfix of an input string is also accepted, if the prefix or postfix is in the language. It is shown that there are languages L Σ+ such that L is not recognizable by OCA in real-time and the reversal of L and the concatenation LΣ* are recognizable by CA in real-time.

In this paper, we propose a new lemma facility, called the strong contraction rule, for model elimination calculus, and we study some implementation issues of strong contraction in a PTTP-based theorem prover. Strong contraction has the ability to shorten possible proofs and prevent some irrelevant computation to a target goal. Strong contraction never broadens the search space, in principle, and thus, has a stable effect on the acceleration of top-down proof search. However, it is difficult to embed the strong contraction into a PTTP-based theorem prover, because strong contraction imposes a truncation operation of center chains in model elimination calculus. We show a self-truncation-style Prolog code, which makes it possible to retain the high performance of a PTTP-based prover with strong contraction. Finally, we evaluate the performance and effect of strong contraction by performing some experiments.

We propose a new type of Graph Rewriting Systems (GRS) that provide a theoretical foundation for using the reduction method which plays an important role on analyze network reliability. By introducing this GRS, several facts were obtained as follows: (1) We clarified the reduction methods of network reliability analysis in the theoretical framework of GRS. (2) In the framework of GRS, we clarified the significance of the completeness in the reduction methods. (3) A procedure of recognizing complete systems from only given rewriting rules was shown. Specially the procedure (3) is given by introducing a boundary graph (B-Graph). Finally an application of GRS to network reliability analysis is shown.