Published July 2, 2003
| Submitted
Report
Open
Formalizing Abstract Algebra in Constructive Set Theory
- Creators
- Yu, Xin
- Hickey, Jason
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.
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.Attached Files
Submitted - formalaa.pdf
Files
formalaa.pdf
Files
(230.3 kB)
| Name | Size | Download all |
|---|---|---|
|
md5:1413785f9ae1c02ab5f8b8a8e1a7d656
|
230.3 kB | Preview Download |
Additional details
- Eprint ID
- 27065
- Resolver ID
- CaltechCSTR:2003.004
- Created
-
2003-07-02Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
- Caltech groups
- Computer Science Technical Reports