JEFL: joint embedding of formal proof libraries

DOI10.1007/978-3-030-86205-3_9MaRDI QIDQ831932zbMATH OpenOpenAlexWikidataFDO

Authors Qingxiang Wang, Cezary Kaliszyk

Publication date 24 March 2022

Full work available at URL https://arxiv.org/abs/2107.10188

zbMATH Keywords

concept alignmentsproof formalizationsystem integrationunsupervised embedding

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Cites work

• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• 30 years of research and development around Coq
• Aligning concepts across proof assistant libraries
• Classification of alignments between concepts of formal mathematical systems
• HOL Light: An Overview
• HOL(y)Hammer: online ATP service for HOL Light
• Importing HOL Light into Coq
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Lemma Mining over HOL Light
• MPTP 0.2: Design, implementation, and initial experiments
• Matching concepts across HOL libraries
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Recycling proof patterns in Coq: case studies
• Scalable LCF-style proof translation
• Sharing HOL4 and HOL Light proof knowledge
• Structured formal development with quotient types in Isabelle/HOL
• The MMT API: a generic MKM system
• The TPTP World -- infrastructure for automated reasoning

Describes a project that uses

Uses Software

• DeepWalk
• OpenTheory
• node2vec
• GloVe
• word2vec
• HOLyHammer
• Flyspeck
• Coq/SSReflect
• QMT
• MMT
• HOL Light
• Mizar
• MoMM
• TPTP
• gensim
• MPTP 0.2
• Isabelle/HOL

This page was built for publication: JEFL: joint embedding of formal proof libraries

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