http://hdl.handle.net/11320/3666 Mon, 01 Jun 2026 09:10:07 GMT 2026-06-01T09:10:07Z http://hdl.handle.net/11320/3721 Tytuł: Algebraic Approach to Algorithmic Logic Autorzy: Bancerek, Grzegorz Abstrakt: We introduce algorithmic logic - an algebraic approach according to [25]. It is done in three stages: propositional calculus, quantifier calculus with equality, and finally proper algorithmic logic. For each stage appropriate signature and theory are defined. Propositional calculus and quantifier calculus with equality are explored according to [24]. A language is introduced with language signature including free variables, substitution, and equality. Algorithmic logic requires a bialgebra structure which is an extension of language signature and program algebra. While-if algebra of generator set and algebraic signature is bialgebra with appropriate properties and is used as basic type of algebraic logic. Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3721 2014-01-01T00:00:00Z http://hdl.handle.net/11320/3722 Tytuł: Formalization of Generalized Almost Distributive Lattices Autorzy: Grabowski, Adam Abstrakt: 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 nor Λ-commutative (resp., Λ-commutative); consequently not all forms of absorption identities hold. We characterized some necessary and sufficient conditions for commutativity and distributivity, we also defined the class of GADLs with zero element. We tried to use as much attributes and cluster registrations as possible, hence many identities are expressed in terms of adjectives; also some generalizations of wellknown notions from lattice theory [11] formalized within the Mizar Mathematical Library were proposed. Finally, some important examples from Rao’s paper were introduced. We construct the example of GADL which is not an ADL. Mechanization of proofs in this specific area could be a good starting point towards further generalization of lattice theory [10] with the help of automated theorem provers [8]. Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3722 2014-01-01T00:00:00Z http://hdl.handle.net/11320/3723 Tytuł: Difference of Function on Vector Space over F Autorzy: Arai, Kenichi; Wakabayashi, Ken; Okazaki, Hiroyuki Abstrakt: In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against block ciphers [13] can be formalized using these definitions. In this article, we formalize the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F. Moreover, we formalize some facts about these definitions. Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3723 2014-01-01T00:00:00Z http://hdl.handle.net/11320/3720 Tytuł: Topological Properties of Real Normed Space Autorzy: Nakasho, Kazuhisa; Futa, Yuichi; Shidama, Yasunari Abstrakt: In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67). Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3720 2014-01-01T00:00:00Z