Algebraically Closed Fields in Isabelle/HOL
- Submitting institution
-
University of Cambridge
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 10549
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-030-51054-1_12
- Title of conference / published proceedings
- Automated Reasoning—10th International Joint Conference, IJCAR 2020
- First page
- 204
- Volume
- 12167 LNAI
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- January
- Year of publication
- 2020
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper reports the first-ever formalisation in a proof assistant of Steinitz's celebrated theorem that every field admits an algebraically closed extension. It also introduces new techniques for formalising algebraic constructions in simple type theory. Furthermore, the main result features an illustrative use of Zorn's lemma.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -