Displaying similar documents to “N-Dimensional Binary Vector Spaces”

Relational Formal Characterization of Rough Sets

Adam Grabowski (2013)

Formalized Mathematics

Similarity:

The notion of a rough set, developed by Pawlak [10], is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of [6], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library). Here we drop the classical equivalence- and tolerance-based...

Morphology for Image Processing. Part I

Hiroshi Yamazaki, Czesław Byliński, Katsumi Wasaki (2012)

Formalized Mathematics

Similarity:

In this article we defined mathematical morphology image processing with set operations. First, we defined Minkowski set operations and proved their properties. Next, we defined basic image processing, dilation and erosion proving basic fact about them [5], [8].

Inner Products, Group, Ring of Quaternion Numbers

Fuguo Ge (2008)

Formalized Mathematics

Similarity:

In this article, we define the division of the quaternion numbers, we also give the definition of inner products, group, ring of the quaternion numbers, and we prove some of their properties.MML identifier: QUATERN2, version: 7.8.10 4.100.1011

Some Operations on Quaternion Numbers

Bo Li, Xiquan Liang, Pan Wang, Yanping Zhuang (2009)

Formalized Mathematics

Similarity:

In this article, we give some equality and basic theorems about quaternion numbers, and some special operations.

Stability of the 4-2 Binary Addition Circuit Cells. Part I

Katsumi Wasaki (2008)

Formalized Mathematics

Similarity:

To evaluate our formal verification method on a real-size calculation circuit, in this article, we continue to formalize the concept of the 4-2 Binary Addition Cell primitives (FTAs) to define the structures of calculation units for a very fast multiplication algorithm for VLSI implementation [11]. We define the circuit structure of four-types FTAs, TYPE-0 to TYPE-3, using the series constructions of the Generalized Full Adder Circuits (GFAs) that generalized adder to have for each positive...

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...

Upper bounds for the degrees of decomposable forms of given discriminant

K. Győry (1994)

Acta Arithmetica

Similarity:

1. Introduction. In our paper [5] a sharp upper bound was given for the degree of an arbitrary squarefree binary form F ∈ ℤ[X,Y] in terms of the absolute value of the discriminant of F. Further, all the binary forms were listed for which this bound cannot be improved. This upper estimate has been extended by Evertse and the author [3] to decomposable forms in n ≥ 2 variables. The bound obtained in [3] depends also on n and is best possible only for n = 2. The purpose of the present paper...

Semantics of MML Query

Grzegorz Bancerek (2012)

Formalized Mathematics

Similarity:

In the paper the semantics of MML Query queries is given. The formalization is done according to [4]