DSpace Kolekcja:
http://hdl.handle.net/11320/4800
2022-05-23T10:44:25ZAlgebra of Polynomially Bounded Sequences and Negligible Functions
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:00ZPropositional Linear Temporal Logic with Initial Validity Semantics
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:00ZConstruction of Measure from Semialgebra of Sets
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:00ZExponential Objects
http://hdl.handle.net/11320/4908
Tytuł: Exponential Objects
Autorzy: Riccardi, Marco
Abstrakt: In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a free-object category [1]. In particular, we show that this definition of natural transformation is equivalent to the standard definition [13]. Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category [12].2015-01-01T00:00:00Z