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].
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...
Grzegorz Bancerek (2012)
Formalized Mathematics
Similarity:
In the paper the semantics of MML Query queries is given. The formalization is done according to [4]
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...
Kazuhisa Ishida, Yasunari Shidama (2008)
Formalized Mathematics
Similarity:
This text includes verification of the basic algorithm in Simple On-the-fly Automatic Verification of Linear Temporal Logic (LTL). LTL formula can be transformed to Buchi automaton, and this transforming algorithm is mainly used at Simple On-the-fly Automatic Verification. In this article, we verified the transforming algorithm itself. At first, we prepared some definitions and operations for transforming. And then, we defined the Buchi automaton and verified the transforming algorithm.MML...
Qi, Feng, Debnath, Lokenath (2000)
International Journal of Mathematics and Mathematical Sciences
Similarity:
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/. ...
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.
Ciesielski, Krzysztof (2003)
Zeszyty Naukowe Uniwersytetu Jagiellońskiego. Universitatis Iagellonicae Acta Mathematica
Similarity:
Saharon Shelah (2000)
Fundamenta Mathematicae
Similarity:
The Kalikow problem for a pair (λ,κ) of cardinal numbers,λ > κ (in particular κ = 2) is whether we can map the family of ω-sequences from λ to the family of ω-sequences from κ in a very continuous manner. Namely, we demand that for η,ν ∈ ω we have: η, ν are almost equal if and only if their images are. We show consistency of the negative answer, e.g., for but we prove it for smaller cardinals. We indicate a close connection with the free subset property and its variants. ...
Grulović, Milan Z. (2002)
Novi Sad Journal of Mathematics
Similarity:
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].