JEFL: joint embedding of formal proof libraries

DOI10.1007/978-3-030-86205-3_9OpenAlexW3200624497WikidataQ108482099 ScholiaQ108482099MaRDI QIDQ831932

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)

Uses Software

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

Cites Work

• Unnamed Item
• Recycling proof patterns in Coq: case studies
• MPTP 0.2: Design, implementation, and initial experiments
• Aligning concepts across proof assistant libraries
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Classification of alignments between concepts of formal mathematical systems
• The MMT API: A Generic MKM System
• Lemma Mining over HOL Light
• The TPTP World – Infrastructure for Automated Reasoning
• HOL Light: An Overview
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Sharing HOL4 and HOL Light Proof Knowledge
• Structured Formal Development with Quotient Types in Isabelle/HOL
• Scalable LCF-Style Proof Translation
• 30 years of research and development around Coq
• Matching Concepts across HOL Libraries
• Importing HOL Light into Coq

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