Grzegorz Bancerek (2013)
Formalized Mathematics
Similarity:
We analyse three algorithms: exponentiation by squaring, calculation of maximum, and sorting by exchanging in terms of program algebra over an algebra.
Gonda, J. (2007)
Acta Mathematica Academiae Paedagogicae Nyí regyháziensis. New Series [electronic only]
Similarity:
Saharon Shelah (2000)
Fundamenta Mathematicae
Similarity:
The aim this paper is to present an answer to Problem 1 of Monk [10], [11]. We do this by proving in particular that if μ is a strong limit singular cardinal, and then there are Boolean algebras such that . Further we improve this result, deal with the method and the necessity of the assumptions. In particular we prove that if is a ccc Boolean algebra and then satisfies the λ-Knaster condition (using the “revised GCH theorem”).
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...
A. Morawiec, B. Węglorz (1993)
Colloquium Mathematicae
Similarity:
It is well known that if a nontrivial ideal ℑ on κ is normal, its quotient Boolean algebra P(κ)/ℑ is -complete. It is also known that such completeness of the quotient does not characterize normality, since P(κ)/ℑ turns out to be -complete whenever ℑ is prenormal, i.e. whenever there exists a minimal ℑ-measurable function in . Recently, it has been established by Zrotowski (see [Z1], [CWZ] and [Z2]) that for non-Mahlo κ, not only is the above condition sufficient but also necessary...
Grzegorz Bancerek (2012)
Formalized Mathematics
Similarity:
In the paper the semantics of MML Query queries is given. The formalization is done according to [4]
Marco Caminati (2011)
Formalized Mathematics
Similarity:
Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster...
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...
Miroslav Langer, Alica Kelemenová (2012)
Kybernetika
Similarity:
In this paper we follow our previous research in the field of positioned agents in the eco-grammar systems and pure grammars. We extend model of the positioned eco-grammar systems by boundary markers and we introduce bordered positioned eco-grammar systems (BPEG systems, for short) and that way we show one of the possible answers to the question stated in [9]. Namely we compare generative power of the BPEG systems with three types of pure regulated grammars with appearance checking. ...
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/. ...