Formalizing Abstract Algebra in Constructive Set Theory

Yu, Xin and Hickey, Jason (2003) Formalizing Abstract Algebra in Constructive Set Theory. Technical Report. California Institute of Technology. [caltechCSTR2003.004]

Full text available as:

PDF - Requires Adobe Acrobat Reader or other PDF viewer.

Abstract

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.

EPrint Type:	Monograph (Technical Report)
Uncontrolled Keywords:	formal methods, theorem proving, abstract algebra
Subjects:	All Records
ID Code:	491
Deposited By:	Xin Yu
Deposited On:	02 July 2003
Record Number:	caltechCSTR2003.004
Official Persistent URL:	http://resolver.caltech.edu/caltechCSTR:2003.004
Usage Policy:	You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.

Archive Staff Only: edit this record