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 show that strategies implemented in automatic theorem proving involve aninteresting tradeoff between execution speed, proving speedup/computationaltime and usefulness of information. We advance formal definitions for theseconcepts by way of a notion of normality related to an expected (optimal)theoretical speedup when adding useful information (other theorems as axioms),as compared with actual strategies that can be effectively and efficientlyimplemented. We propose the existence of an ineluctable tradeoff between thisnormality and computational time complexity. The argument quantifies theusefulness of information in terms of (positive) speed-up. The results disclosea kind of no-free-lunch scenario and a tradeoff of a fundamental nature. Themain theorem in this paper together with the numerical experiment---undertakenusing two different automatic theorem provers AProS and Prover9 on randomtheorems of propositional logic---provide strong theoretical and empiricalarguments for the fact that finding new useful information for solving aspecific problem (theorem) is, in general, as hard as the problem (theorem)itself.

Rare Speed-up in Automatic Theorem Proving Reveals Tradeoff Between Computational Time and Information Value