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

Traditional automated theorem provers for first-order logic depend onspeed-optimized search and many handcrafted heuristics that are designed towork best over a wide range of domains. Machine learning approaches inliterature either depend on these traditional provers to bootstrap themselvesor fall short on reaching comparable performance. In this paper, we propose ageneral incremental learning algorithm for training domain specific provers forfirst-order logic without equality, based only on a basic given-clausealgorithm, but using a learned clause-scoring function. Clauses are representedas graphs and presented to transformer networks with spectral features. Toaddress the sparsity and the initial lack of training data as well as the lackof a natural curriculum, we adapt hindsight experience replay to theoremproving, so as to be able to learn even when no proof can be found. We showthat provers trained this way can match and sometimes surpass state-of-the-arttraditional provers on the TPTP dataset in terms of both quantity and qualityof the proofs.

Proving Theorems using Incremental Learning and Hindsight Experience Replay