Displaying similar documents to “Formalization of Integral Linear Space”

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

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

Bertrand’s Ballot Theorem

Karol Pąk (2014)

Formalized Mathematics

Similarity:

In this article we formalize the Bertrand’s Ballot Theorem based on [17]. Suppose that in an election we have two candidates: A that receives n votes and B that receives k votes, and additionally n ≥ k. Then this theorem states that the probability of the situation where A maintains more votes than B throughout the counting of the ballots is equal to (n − k)/(n + k). This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. ...

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

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.

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]