A Caltech Library Service

Formalizing Abstract Algebra in Constructive Set Theory

Yu, Xin and Hickey, Jason (2003) Formalizing Abstract Algebra in Constructive Set Theory. 2003.004. California Institute of Technology , Pasadena, CA. (Unpublished)

PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


We present a machine-checked formalization of elementary abstract algebra in constructive set theory. Our formalization uses an approach where we start by specifying the group axioms as a collection of inference rules, defining a 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 formalization of all other concepts in abstract algebra is based on that of the group. We give an example of a formalization of a concrete group, the Klein 4-group.

Item Type:Report or Paper (Technical Report)
Additional Information:© 2003 California Institute of Technology. The authors would like to thank Aleksey Nogin. His valuable observations have greatly improved the contents and the presentation of the paper. We also want to thank Alexei Kopylov for discussions on the formalization.
Group:Computer Science Technical Reports
Subject Keywords:formal methods, theorem proving, abstract algebra
Issue or Number:2003.004
Record Number:CaltechCSTR:2003.004
Persistent URL:
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:27065
Deposited By: Imported from CaltechCSTR
Deposited On:02 Jul 2003
Last Modified:03 Oct 2019 03:20

Repository Staff Only: item control page