http://hdl.handle.net/11320/4800 2026-06-01T15:15:34Z http://hdl.handle.net/11320/4909 Tytuł: Algebra of Polynomially Bounded Sequences and Negligible Functions Autorzy: Okazaki, Hiroyuki Abstrakt: In this article we formalize negligible functions that play an essential role in cryptology [10], [2]. Generally, a cryptosystem is secure if the probability of succeeding any attacks against the cryptosystem is negligible. First, we formalize the algebra of polynomially bounded sequences [20]. Next, we formalize negligible functions and prove the set of negligible functions is a subset of the algebra of polynomially bounded sequences. Moreover, we then introduce equivalence relation between polynomially bounded sequences, using negligible functions. 2015-01-01T00:00:00Z http://hdl.handle.net/11320/4910 Tytuł: Propositional Linear Temporal Logic with Initial Validity Semantics Autorzy: Giero, Mariusz Abstrakt: In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of “until” operator in a very strict version. The very strict “until” operator enables to express all other temporal operators.In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial state of model while normal semantics means that we define the validity as satisfaction in all states of model. We prove the Deduction Theorem, and the soundness and completeness of the introduced formal system. We also prove some theorems to compare both formal systems, i.e., the one introduced in the article [10] and the one introduced in this article.Formal systems for temporal logics are applied in the verification of computer programs. In order to carry out the verification one has to derive an appropriate formula within a selected formal system. The formal systems introduced in [10] and in this article can be used to carry out such verifications in Mizar [4]. 2015-01-01T00:00:00Z http://hdl.handle.net/11320/4905 Tytuł: Construction of Measure from Semialgebra of Sets Autorzy: Endou, Noboru Abstrakt: In our previous article [22], we showed complete additivity as a condition for extension of a measure. However, this condition premised the existence of a σ-field and the measure on it. In general, the existence of the measure on σ-field is not obvious. On the other hand, the proof of existence of a measure on a semialgebra is easier than in the case of a σ-field. Therefore, in this article we define a measure (pre-measure) on a semialgebra and extend it to a measure on a σ-field. Furthermore, we give a σ-measure as an extension of the measure on a σ-field. We follow [24], [10], and [31]. 2015-01-01T00:00:00Z http://hdl.handle.net/11320/4907 Tytuł: Characteristic of Rings. Prime Fields Autorzy: Schwarzweller, Christoph; Korniłowicz, Artur Abstrakt: The notion of the characteristic of rings and its basic properties are formalized [14], [39], [20]. Classification of prime fields in terms of isomorphisms with appropriate fields (ℚ or ℤ/p) are presented. To facilitate reasonings within the field of rational numbers, values of numerators and denominators of basic operations over rationals are computed. 2015-01-01T00:00:00Z