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 metadata

https://hal.inria.fr/hal-03083589
Contributor : Paulo de Vilhena Connect in order to contact the contributor
Submitted on : Monday, December 21, 2020 - 11:08:29 AM
Last modification on : Friday, January 21, 2022 - 3:18:48 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

INSMI | X | IP_PARIS | INRIA | CDF | PSL

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

Les métriques sont temporairement indisponibles