English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present the problem of selecting relevant premises for a proof of a givenstatement. When stated as a binary classification task for pairs (conjecture,axiom), it can be efficiently solved using artificial neural networks. The keydifference between our advance to solve this problem and previous approaches isthe use of just functional signatures of premises. To further improve theperformance of the model, we use dimensionality reduction technique, to replacelong and sparse signature vectors with their compact and dense embeddedversions. These are obtained by firstly defining the concept of a context foreach functor symbol, and then training a simple neural network to predict thedistribution of other functor symbols in the context of this functor. Aftertraining the network, the output of its hidden layer is used to construct alower dimensional embedding of a functional signature (for each premise) with adistributed representation of features. This allows us to use 512-dimensionalembeddings for conjecture-axiom pairs, containing enough information about theoriginal statements to reach the accuracy of 76.45% in premise selection task,only with simple two-layer densely connected neural networks.

Premise selection with neural networks and distributed representation of features