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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Smart premise selection is essential when using automated reasoning as a toolfor large-theory formal proof development. A good method for premise selectionin complex mathematical libraries is the application of machine learning tolarge corpora of proofs. This work develops learning-based premise selection intwo ways. First, a newly available minimal dependency analysis of existinghigh-level formal mathematical proofs is used to build a large knowledge baseof proof dependencies, providing precise data for ATP-based re-verification andfor training premise selection algorithms. Second, a new machine learningalgorithm for premise selection based on kernel methods is proposed andimplemented. To evaluate the impact of both techniques, a benchmark consistingof 2078 large-theory mathematical problems is constructed,extending the olderMPTP Challenge benchmark. The combined effect of the techniques results in a50% improvement on the benchmark over the Vampire/SInE state-of-the-art systemfor automated reasoning in large theories.

Premise Selection for Mathematics by Corpus Analysis and Kernel Methods