The Coq library as a theory graph

DOI10.1007/978-3-030-23250-4_12zbMath1428.68344OpenAlexW2956143085MaRDI QIDQ2287907

Dennis Müller, Claudio Sacerdoti Coen, Florian Rabe

Publication date: 22 January 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-23250-4_12

Mathematics Subject Classification ID

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

Related Items

Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Unnamed Item ⋮ Experiences from exporting major proof assistant libraries

Uses Software

• Coq
• Isabelle/HOL
• PVS
• Mizar
• Matita
• HOL Light
• CoqHammer
• CoqInE