Formalizing Abstract Algebra In Constructive Set Theory:- Ibeabuchi, Promise I

Authors: PROMISE IGWE, IBEABUCHI | Natural & Applied Sciences Mathematics Projects 32 pages 4,006 words

Subscribe to read and download this work.

ABSTRACT

This project work present a machine-checked formalization of I • elementary abstract algebra in constructive set theory. This formalization uses an approach where I start by specifying the group axioms as a collection of inference rules, defining logic for groups. Then we can tell whether. a given set with a binary operation is a group or not and .derive all properties of groups constructively from these inference rules as well as the axioms of the set theory. The . . ' I • formalization of all other' concepts in group. This work also present an example of a formalization of a concrete group, the Klein 4 - group. 

Share this work