http://hdl.handle.net/11320/8879 2026-06-01T07:20:35Z 2026-06-01T07:20:35Z Futa, Yuichi Okazaki, Hiroyuki Shidama, Yasunari http://hdl.handle.net/11320/9017 2020-04-17T09:21:50Z 2019-01-01T00:00:00Z

Tytuł: Operations of Points on Elliptic Curve in Affine Coordinates Autorzy: Futa, Yuichi; Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article, we formalize in Mizar [1], [2] a binary operation of points on an elliptic curve over GF(p) in affine coordinates. We show that the operation is unital, complementable and commutative. Elliptic curve cryptography [3], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security.

2019-01-01T00:00:00Z Koch, Sebastian http://hdl.handle.net/11320/9016 2020-04-17T09:01:53Z 2019-01-01T00:00:00Z

Tytuł: About Vertex Mappings Autorzy: Koch, Sebastian Abstrakt: In [6] partial graph mappings were formalized in the Mizar system [3]. Such mappings map some vertices and edges of a graph to another while preserving adjacency. While this general approach is appropriate for the general form of (multidi)graphs as introduced in [7], a more specialized version for graphs without parallel edges seems convenient. As such, partial vertex mappings preserving adjacency between the mapped verticed are formalized here.

2019-01-01T00:00:00Z Koch, Sebastian http://hdl.handle.net/11320/9015 2020-04-17T08:47:18Z 2019-01-01T00:00:00Z

Tytuł: About Graph Mappings Autorzy: Koch, Sebastian Abstrakt: In this articles adjacency-preserving mappings from a graph to another are formalized in the Mizar system [7], [2]. The generality of the approach seems to be largely unpreceeded in the literature to the best of the author’s knowledge. However, the most important property defined in the article is that of two graphs being isomorphic, which has been extensively studied. Another graph decorator is introduced as well.

2019-01-01T00:00:00Z Koch, Sebastian http://hdl.handle.net/11320/9014 2020-04-16T11:53:50Z 2019-01-01T00:00:00Z

Tytuł: Underlying Simple Graphs Autorzy: Koch, Sebastian Abstrakt: In this article the notion of the underlying simple graph of a graph (as defined in [8]) is formalized in the Mizar system [5], along with some convenient variants. The property of a graph to be without decorators (as introduced in [7]) is formalized as well to serve as the base of graph enumerations in the future.

2019-01-01T00:00:00Z