scientific article; zbMATH DE number 7699425

DOI10.4230/LIPICS.ITP.2021.8MaRDI QIDQ6157249zbMATH OpenFDO

Authors Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub

Publication date 20 June 2023

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2021.8

zbMATH Keywords

Abel-RuffiniCoqdependent type theoryGalois theorygeneral quinticmathematical components

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited in

(3)

• \(\forall \exists^{5}\)-equational theory of context unification is undecidable
• THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F
• What is the point of computers? A question for pure mathematicians

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6157249)