We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: JEFL: Joint Embedding of Formal Proof Libraries

Abstract: The heterogeneous nature of the logical foundations used in different interactive proof assistant libraries has rendered discovery of similar mathematical concepts among them difficult. In this paper, we compare a previously proposed algorithm for matching concepts across libraries with our unsupervised embedding approach that can help us retrieve similar concepts. Our approach is based on the fasttext implementation of Word2Vec, on top of which a tree traversal module is added to adapt its algorithm to the representation format of our data export pipeline. We compare the explainability, customizability, and online-servability of the approaches and argue that the neural embedding approach has more potential to be integrated into an interactive proof assistant.
Comments: Submission to FroCoS 2021
Subjects: Logic in Computer Science (cs.LO); Computation and Language (cs.CL); Machine Learning (cs.LG)
Cite as: arXiv:2107.10188 [cs.LO]
  (or arXiv:2107.10188v1 [cs.LO] for this version)

Submission history

From: Qingxiang Wang [view email]
[v1] Wed, 21 Jul 2021 16:31:33 GMT (228kb)

Link back to: arXiv, form interface, contact.