Skip to Main content Skip to Navigation
Conference papers

Algebraically Closed Fields in Isabelle/HOL

Abstract : A fundamental theorem states that every field admits an algebraically closed extension. Despite its central importance, this theorem has never before been formalised in a proof assistant. We fill this gap by documenting its formalisation in Isabelle/HOL, describing the difficulties that impeded this development and their solutions.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-03083589
Contributor : Paulo Emílio de Vilhena <>
Submitted on : Monday, December 21, 2020 - 11:08:29 AM
Last modification on : Thursday, January 7, 2021 - 3:37:13 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Paulo Emílio de Vilhena, Lawrence Paulson. Algebraically Closed Fields in Isabelle/HOL. IJCAR 2020 - International Joint Conference on Automated Reasoning, Jul 2020, Paris, France. pp.204-220, ⟨10.1007/978-3-030-51054-1_12⟩. ⟨hal-03083589⟩

Share

Metrics

Record views

42

Files downloads

155


Données de recherche

doi: web.