Forcing when there are large cardinals: An introduction
Forcing with ideals generated by closed sets
Consider the poset where is an arbitrary -ideal -generated by a projective collection of closed sets. Then the extension is given by a single real of an almost minimal degree: every real is Cohen-generic over or .
Forcing with proper classes
Forcing with propositional Lindenbaum algebras.
Forcings which preserve large cardinals
Formal Specifications in Software Development: an Overview
Formalization of Generalized Almost Distributive Lattices
Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative...
Formalization of the Advanced Encryption Standard. Part I
In this article, we formalize the Advanced Encryption Standard (AES). AES, which is the most widely used symmetric cryptosystem in the world, is a block cipher that was selected by the National Institute of Standards and Technology (NIST) as an official Federal Information Processing Standard for the United States in 2001 [12]. AES is the successor to DES [13], which was formerly the most widely used symmetric cryptosystem in the world. We formalize the AES algorithm according to [12]. We then verify...
Formalized models of ontological systems
Formalizing a non-linear Henkin quantifier
Formally self-referential propositions for cut free classical analysis and related systems [Book]
Formes combinatoires du théorème d'incomplétude
Formulas and ultraproducts in categories
Formulas of the general solutions of Boolean equations.
Formulation of Cell Petri Nets
Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended...
Foundations for stepwise refinement of program specifications via cylindric algebra theory
Fractal construction of an atomic Archimedean effect algebra with non-atomic subalgebra of sharp elements
Does there exist an atomic Archimedean lattice effect algebra with non-atomic subalgebra of sharp elements? An affirmative answer to this question is given.
Fractions continues limitées et théorie des langages
Fragments of complete extensions of PA and McDowell-Specker's theorem.
Fragments of strong compactness, families of partitions and ideal extensions
We investigate some natural combinatorial principles related to the notion of mild ineffability, and use them to obtain new characterizations of mild ineffable and weakly compact cardinals. We also show that one of these principles may be satisfied by a successor cardinal. Finally, we establish a version for of the canonical Ramsey theorem for pairs.