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

The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorffet al. in 2019, explicitly builds partial strategies inside refutations. Theoriginal motivation for this approach was to overcome the limitationsencountered in long-distance Q-Resolution proof system (LD-Q-Res), where thesyntactic side-conditions, while prohibiting all unsound resolutions, also endup prohibiting some sound resolutions. However, while the advantage of M-Resover many other resolution-based QBF proof systems was already demonstrated, acomparison with LD-Q-Res itself had remained open. In this paper, we settlethis question. We show that M-Res has an exponential advantage over not onlyLD-Q-Res, but even over LQU$^+$-Res and IRM, the most powerful among currentlyknown resolution-based QBF proof systems. Combining this with results fromBeyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Resand LQU$^+$-Res.  Our proof method reveals two additional and curious features about M-Res: (i)M-Res is not closed under restrictions, and is hence not a natural proofsystem, and (ii) weakening axiom clauses with existential variables provablyyields an exponential advantage over M-Res without weakening. We further showthat in the context of regular derivations, weakening axiom clauses withuniversal variables provably yields an exponential advantage over M-Res withoutweakening. These results suggest that M-Res is better used with weakening,though whether M-Res with weakening is closed under restrictions remains open.We note that even with weakening, M-Res continues to be simulated by eFrege $+$$\forall$red (the simulation of ordinary M-Res was shown recently by Chew andSlivovsky).

QBF Merge Resolution is powerful but unnatural