Displaying similar documents to “How to improve efficiency of analysis of sequential data?”

Basic Properties and Concept of Selected Subsequence of Zero Based Finite Sequences

Yatsuka Nakamura, Hisashi Ito (2008)

Formalized Mathematics

Similarity:

Here, we develop the theory of zero based finite sequences, which are sometimes, more useful in applications than normal one based finite sequences. The fundamental function Sgm is introduced as well as in case of normal finite sequences and other notions are also introduced. However, many theorems are a modification of old theorems of normal finite sequences, they are basically important and are necessary for applications. A new concept of selected subsequence is introduced. This concept...

Formalization of Integral Linear Space

Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2011)

Formalized Mathematics

Similarity:

In this article, we formalize integral linear spaces, that is a linear space with integer coefficients. Integral linear spaces are necessary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm that outputs short lattice base and cryptographic systems with lattice [8].

The Sum and Product of Finite Sequences of Complex Numbers

Keiichi Miyajima, Takahiro Kato (2010)

Formalized Mathematics

Similarity:

This article extends the [10]. We define the sum and the product of the sequence of complex numbers, and formalize these theorems. Our method refers to the [11].

Arithmetical transfinite induction and hierarchies of functions

Z. Ratajczyk (1992)

Fundamenta Mathematicae

Similarity:

We generalize to the case of arithmetical transfinite induction the following three theorems for PA: the Wainer Theorem, the Paris-Harrington Theorem, and a version of the Solovay-Ketonen Theorem. We give uniform proofs using combinatorial constructions.

Real-valued GCS classifier system

Łukasz Cielecki, Olgierd Unold (2007)

International Journal of Applied Mathematics and Computer Science

Similarity:

Learning Classifier Systems (LCSs) have gained increasing interest in the genetic and evolutionary computation literature. Many real-world problems are not conveniently expressed using the ternary representation typically used by LCSs and for such problems an interval-based representation is preferable. A new model of LCSs is introduced to classify real-valued data. The approach applies the continous-valued context-free grammar-based system GCS. In order to handle data effectively, the...

Model Checking. Part II

Kazuhisa Ishida (2008)

Formalized Mathematics

Similarity:

This article provides the definition of linear temporal logic (LTL) and its properties relevant to model checking based on [9]. Mizar formalization of LTL language and satisfiability is based on [2, 3].

Stability of n -Bit Generalized Full Adder Circuits (GFAs). Part II

Katsumi Wasaki (2008)

Formalized Mathematics

Similarity:

We continue to formalize the concept of the Generalized Full Addition and Subtraction circuits (GFAs), define the structures of calculation units for the Redundant Signed Digit (RSD) operations, then prove its stability of the calculations. Generally, one-bit binary full adder assumes positive weights to all of its three binary inputs and two outputs. We define the circuit structure of two-types n-bit GFAs using the recursive construction to use the RSD arithmetic logical units that...