On algebraic hierarchies in mathematical repository of Mizar

Abstract

Mathematics, especially algebra, uses plenty of structures: groups, rings, integral domains, fields, vector spaces to name a few of the most basic ones. Classes of structures are closely connected -usually by inclusion -naturally leading to hierarchies that has been reproduced in different forms in different mathematical repositories. In this paper we give a brief overview of some existing algebraic hierarchies and report on the latest developments in the Mizar computerized proof assistant system. In particular we present a detailed algebraic hierarchy that has been defined in Mizar and discuss extensions of the hierarchy towards more involved domains. Taking fully formal approach into account we meet new difficulties comparing with its informal mathematical framework.